Documentation

postscript

pdf

This is a fairly complete description of the SAL language for specifying transition systems. Note that the IMPLEMENTS operator is not implemented (!) and that the assertion language is not defined as part of SAL but by the tools that interpret the assertions. The model checkers use LTL (Linear Temporal Logic) as their assertion language (they also accept CTL syntax on the common fragment); please see the basic tutorial below for more details.

SAL and XML - SAL is intended to be language and platform independent; toward this end we defined the abstract syntax for the SAL language in XML. The SAL DTD describes valid abstract syntax.

postscript

pdf

This is a very elementary tutorial; it introduces the LTL assertion language, and use of the symbolic and bounded model checkers and some auxiliary tools

This is a more substantial example from the field of fault-tolerant algorithms; it uses both the symbolic and bounded model checkers

This is another fairly substantial example, this time from the field of cryptographic protocols; it uses both the symbolic and bounded model checkers

The best advice is to study the papers on timed systems in SAL. There are examples on the VVFCS project page too.