SALT - Smart Assertion Language for Temporal Logic
Goal
Do you want to specify the behavior of your program in a rigorously yet comfortable manner?
Do you see the benefits of temporal specifications but are bothered by the awkward formalisms available?
Do you want to use
- the power of a Model Checker to improve the quality of your systems or
- the powerful runtime reflection approach for bug hunting and elimination
but don't like the syntax of LTL?
If you can answer one of the above questions positively then SALT is your solution!
Try SALT click me
The Language
SALT stands for Smart Assertion Language for Temporal Logic. It is a temporal specification language that is similar in spirit to programming languages like C and Java and is therefore well suited for software engineers. Its expressiveness, on the other side, covers LTL, or, when the realtime operators of SALT are used, covers TLTL (Timed LTL).
Parts of SALT are similar in spirit to the specification lanugage Sugar, a domain specific language used in hardware industry. SALT, however, is designed mainly for software systems.
The SALT distribution comes with a manual describing the language operators both with typical examples and with the needed rigor. The SALT translator, which is available on request, takes SALT specifications and produces LTL formulas ready to use with the tools SMV or SPIN.
Documentation
- Tutorial held at NASA Formal Methods Symposium.
- Technical Report listing main features of SALT.
- SALT manual
- Jonathan Streit's master thesis
Download
Note that you need Hugs and JAVA to run the SALT compiler.
People
SALT is developed and maintained by
- Andreas Bauer
- Martin Leucker
- Jonathan Streit
For more information, please contact me.