Links, Papers, and Software

Here are some links to interesting external pages including text books, software and further background material.

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 second part of the course is described in depth in Chapter 2 of inVerification of Object-Oriented Software: The KeY Approach.
    •

    KeY

  • You can download the KeY system from the KeY Project website: http://www.key-project.org/download/#key The best and easiest way is to use Key via WebStart.
  • The main reference to KeY system is the book Verification of Object-Oriented Software: The KeY Approach. From the TU-BS Domain, you have full text access. 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.
  • The KeY Quicktour is available at the KeY download page.
  • A tutorial introduction to Key is available from here: Verifying Object-Orient Programs with KeY: A Tutorial. See also the corresponding source files (click 'updated version').
    •

    JML

    Please follow the instructions at JML Installation Notes on how to install a syntax checker for JML in Eclipse.

    Software

  • Spin download and installation; MacOSX: if you get the following message sh: /lib/cpp: No such file or directory when running 'spin' you can do the following: Find out where your cpp is installed via which cpp (using theTerminal application) (you might need to install XCode from Apple's MacOSX DVDs first). Then enter the following in the Terminal (press enter after each line)
    sudo mkdir /lib 
    ln -s path_to_cpp/cpp /lib/cpp 
    alternatively you can patch spins sourcecode and change the line in main.c from /lib/cpp to cpp.
  • jSpin and SpinSpider used in the course book
  • Eclipse PlugIn EpiSpin
  • KeY download and installation, the best and easiest option is the Key Webstart. 

    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.

    •

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

    Further Links

  • Promela mode for Emacs
  • Eclipse Plug-in for Spin
    •