Formal Methods for Software Development TDA294/DIT271, LP1, HT2018

Literature, Tools and Links

Course Literature

For the first part we partly use the book Principles of the Spin Model Checker, mostly Chapters 1-5. The book is available as E-book from within the Chalmers network. Some additional material for that book, in particular the examples, can be found online. In particular, you find there a few pages "Supplementary material on version 6 of Spin", which corrects some outdated information from the main book.

For the second part, there is highly relevant material in the book Deductive Software Verification - The KeY Book, co-edited by the course teacher (accessible from within the Chalmers network). Chapter 1 in the book introduces general principles of deductive software verification in general, and of the KeY approach in particular. Chapter 7, co-authored by the course teacher, is a tutorial on formal specification of Java applications using the Java Modeling Language. Chapter 16 is a tutorial for the overall verification process using the KeY approach and tool. Chapter 15, co-authored by the course teacher, is a tutorial on using the the KeY prover.

Additional Literature

Model checking





We provide an online interface to some of the tools used in the course, 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.
  • OpenJML (Open Web-Interface)
    • In the top-left corner you find a collection of example Java files and those used in the course.
    • You can create a file by either choosing one from the collection of examples, or by clicking the (+) button above the editor.
    • By clicking the 'Syntax' button OpenJML is run to check that your JML annotations use correct syntax.
    • By clicking the 'ESC' button OpenJML runs an Extended Static Check, using Yices 2 as its back-end, to statically find violations of your JML specification.
    • You can hover over the warning / error markers on the left-hand side to see the output of OpenJML.

Promela, Spin, jSpin, LTL


  • We have created an online interface to OpenJML (including static checking with Yices2) to avoid installation problems.
  • The latest version of OpenJML can be found on their website (direct link here).
  • Within the directory where you extracted openjml.jar, run the command
    java -Xbootclasspath/p:openjml.jar -jar openjml.jar -noInternalSpecs path_to_file
  • If you cannot run java 1.7, we have a local copy of an older release that still supported 1.6 here.
  • OpenJML allows you to compile to a bytecode (.class) file with inlined run-time assertion checks on your invariants, pre- and post-conditions. Try this for example with this file. Compile using:
    java -Xbootclasspath/p:openjml.jar -jar openjml.jar -rac -noInternalSpecs path_to_file
    (note the extra -rac flag). For Java 1.6, use instead:
    java -Xbootclasspath/p:openjml.jar -jar openjml.jar -rac -source 1.6 -target 1.6 -noInternalSpecs path_to_file
    Then run the program with:
    java -classpath ':*' JMLTest 12
    Where 12 is the input to the program. You can try different inputs and see how the assertions can be triggered.


  • The KeY project website.
  • In particular, the KeY system is available via the KeY download pages, in the following ways:
    • The KeY system is available via webstart.
      (You need Java Runtime installed on your machine. When using Ubuntu, you may in addition need IcedTea-Web, available through the ubuntu package icedtea-netx. On all systems, you will need to confirm that you trust apps from the KeY download page. On Mac, you may in addition need to add in the security settings in the the Java Control Panel, reachable from the System Preferences.) If your browser does not recognise webstart files, you can download the webstart file KeY.jnlp and run it with javaws KeY.jnlp.
    • Here are alternatives to webstart:
      • Download and unpack these binaries, and run KeY.jar, by double click (possibly after making it executable) or via java -jar KeY.jar
      • Install the Eclipse plugin, from Eclipse via Install New Software, and then providing the Eclipse link from the KeY doload page.
  • 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)

Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools W. Ahrendt, Oct 4, 2018