Formal Methods for Software Development TDA294/DIT272, LP1, HT2023

Tools

SPIN web-interface

We provide an online interface to SPIN, to avoid installation problems.

  • Notes on saving
    • The web-interface does not save your files. To save your progress, copy the content of the editor into a file local on your machine (or save it by pressing Ctrl+S)!
  • Spin (Open Web-Interface)
    • In the top-left corner you find a collection of examples and Promela files used in the course, as well as a cheat sheet to the most used Promela syntax.
    • You can create a file by either choosing one from the collection of examples, or by clicking the (+) button above the editor.
    • You can press Ctrl+S in an opened tab to save that tab to your local machine.
    • The control panel on the right allows you to run simulations and verifications on the file that is in the currently opened tab (programs with multiple files are not supported).
    • The first group of options displays events that are printed during simulations and guided runs. Note that if 'Statements' is not selected almost no information will be printed. These options apply to both the simulation as well as running the generated trail of verification.
    • It is recommended to use the 'Stop after ...' option when running simulations that print all statements, otherwise your browser might take a long time for displaying the output.
    • For verification, select the right mode (Safety, Acceptance / Liveness, Non-progress) and specify the name of the named LTL formula in the currently opened Promela file that you want to verify. If a counter-example is found and 'Run generated trail' is selected the trail of the counter-example is printed at the bottom of the output.
    • The timeout for simulations is set to 1 second; for verification it is set to 30 seconds.

Promela, Spin, jSpin, LTL

KeY

  • We recommend to use a special built of the KeY system which was compiled for this course. It is the "fat JAR" file, which you can download here. There are various ways to execute the JAR file, which depend on your browser configuration and operating system. In any case, you need Java RE (runtime environment) on your machine. We recommend Java 11 or higher, but it may also work with lower versions.
    • Download the file and execute it (possibly after making it executable), by double click or via the command line: java -jar <pathToFile>
    • Depending on your browser set-up, you might be able to run the JAR directly from the browser, by double clicking the link.
  • The KeY project website.
  • There is a book on the KeY approach and system called Deductive Software Verification - The KeY Book. See Course Literature. In particular, the book features:
    • "Formal Verification with KeY: A Totorial" (chapter 16)
    • "Using the KeY Prover" (chapter 15)
  • Note that the KeY version recommended above is not 100% compliant with the KeY book, as many improvements were made after the book was written. For more compliant versions, we refer to download pages of the KeY project website.

OpenJML

  • OpenJML allows, among other things, to compile to a bytecode (.class) file with inlined run-time assertion checks on your invariants, pre- and post-conditions. The latest version can be found on the OpenJML website, together with usage instructions.



W. Ahrendt