Additional Literature
Tools
Web-interfaces
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 and jSpin
OpenJML
- 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.
KeY
- The version used in this course is available via
webstart here.
(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 http://www.key-project.org in the security settings in the
the Java Control Panel, reachable from
the System Preferences.)
For alternatives to webstart, see
the KeY1.6.5
download page.
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').
Other Links
|