Software Engineering using
Formal Methods		 TDA293/DIT270, LP1, HT2011
Links, Papers, and Software

Here are some links to interesting external pages including text books.

Formal Methods in General

  • Formal Methods Humor

  • Formal Methods Education Resources

  • Formal Methods in Wikipedia

    • Promela/SPIN

  • Home page of Promela/Spin

  • Ben-Ari's Spin reference card

  • In this course we use the new text book Principles of the Spin Model Checker by Ben-Ari.

  • The definitive reference for Promela and Spin is The Spin Model Checker by Holzmann. It contains the full theoretical background.

  • The book by Clarke et al. is a standard reference of Model Checking in general.

    • First-Order Logic

  • There are many good books on first-order (aka predicate) logic. One of the best is Melvin Fitting's First-Order Logic and Automated Theorem Proving

  • 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/Java Card

    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.

  • Java Card 2.2.1 API

  • Sun's portal for Java technology

  • Sun's portal 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.

    • KeY

    The version used in this course is available here

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

    OpenJML

    OpenJML is the upcoming tool suite for the Java Modelling Language. For the course we have compiled a current svn snapshot of their code. Please note, the OpenJML developers did not yet publish an official release, and this is just a build from a snapshot. It should be stable enough to use it for checking your JML specifications.
    You can download it from here (tgz, zip).

    Unzip the file in any directory you want e.g. user/openjml/. You can then perform a syntax check with

    java -jar user/openjml/openjml.jar -check -noInternalSpecs path_to_file_to_check

    If you want to check all files in a directory use

    java -jar user/openjml/openjml.jar -check -noInternalSpecs -dir path_to_directory

    MacOSX user need to install OpenJDK6, please follow the instruction at then end of the OpenJML setup page

    Software

  • Spin download and installation

  • jSpin and SpinSpider used in the course book

  • KeY for SEFM 2011 download and installation

    Following these links, you find information on installation and usage of the respective tool. Concerning Spin and jSpin, we have compiled some additional installation notes.

    • Further Links

  • Promela mode for Emacs

  • Eclipse Plug-in for Spin


    • Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools W. Ahrendt R. Bubel W. Mostowski , Sep 21, 2011