Model checking

• In this course we use the text book Principles of the Spin Model Checker by Ben-Ari.
• The book by Clarke et al. is a standard reference of Model Checking in general.

Logic

• There are many good books on first-order (aka predicate) logic. We recommend, as a good introduction, Logic in Computer Science by Michael Huth and Mark Ryan.
• First-order logic with Java-style types as discussed in the last part of the course is described in depth in Chapter 2 of in Verification of Object-Oriented Software: The KeY Approach.

UML

The most basic notions of UML will suffice in this course. It is enough to understand the essentials of class and object diagrams.

• The Object Management Grup (OMG) is an industrial consortium responsible for standards development in object-oriented computing. In particular they maintain UML, where all kinds of UML/OCL documents can be found.
• If you need an introduction or refresher on UML, then Martin Fowlers's UML Distilled is strongly recommended. Still the best basic text on UML (plus a lot of general wisdom on OOP). The 3rd edition is compliant with UML 2.0.

Java Card

• The Java Card 2.2.1 API as supported by KeY can be found here
• Sun's portal for Java technology, and for Java Card technology
• If you need a refresher on Java, then Jia's Object Oriented Software Development Using Java 2/e is warmly recommended.
• Every computer professional dealing with Java needs to own the Java Language Specification and the Java Programming Language, but that goes without saying.

Promela, Spin and jSpin

• We compiled a list of instructions on installing Spin and jSpin on your own computer or using it at the remote Chalmers servers here.
• In case our instructions do not work, you should use the official instructions for Spin, jSpin and SpinSpider.
• Our own tweaked version of jSpin with syntax highlighting is here.
• The handy Ben-Ari's Spin Reference card.
• The home page of Promela/Spin.
• The definitive reference for Promela and Spin is The Spin Model Checker by Holzmann. It contains the full theoretical background.
• Promela mode for Emacs
• Eclipse Plug-in for Spin

OpenJML

• 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.

KeY

• The version used in this course is available via webstart here.

  Note on versions: the KeY system's target language for verification is not Java, but Java Card. Java Card is Sun's Java dialect intended to run on smart cards and other embedded systems. Its syntax and API are mostly a restriction of Java (the exact differences will be explained in the lectures). This means that Java programs that obey the restrictions of Java Card can be verified with KeY as well. In fact, all the programs discussed in this course are at the same time Java and Java Card programs. The latest version of Java is 1.6, and the latest version of Java Card is 2.2.2.

  The KeY system supports Java Card 2.2.1, but the differences between 2.2.1 and 2.2.2 lie only in the API. Java Card has no generic types, therefore, Java Card programs syntactically conform to Java 1.4 (up to the API, of course). In particular, from the Java Card API we will only use java.lang, which is a (very small) subset of all Java SDK2 APIs.

• There is a book on the KeY system called Verification of Object-Oriented Software: The KeY Approach. You can access the online version from a Chalmers account. Navigate to Chalmers Library, E-Books, Lecture Notes in Computer Science. Chapter 1 in the book gives a general introduction in the philosophy behind KeY. Chapter 10 is an introduction into the usage of the system. See also the KeY project website.
• KeY Quicktour is available at the KeY download page.
• Verifying Object-Orient Programs with KeY: A Tutorial,
  an article that contains an advanced example for specification in JML and verification with KeY.
  See also the corresponding source files (click 'updated version').

• Formal Methods Humor
• Formal Methods Education Resources
• Formal Methods in Wikipedia