SALT – Structured Assertion Language for Temporal Logic
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!
You can try out SALT using this web interface.
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.
- Tutorial held at NASA Formal Methods Symposium.
- Technical Report listing main features of SALT.
- SALT manual
- Jonathan Streit's diploma thesis
Note that you need Hugs and JAVA to run the SALT compiler.
SALT was developed by
SALT EO alpha
SALT EO is the new and improved version of SALT. Its features are:
- LamaConv integration - automatically create automata from SALT specifications
- Advanced web interface with syntax highlighting, auto-completion and the above mentioned LamaConv integration
- Easier setup: available as a JAR that only requires Java to run
Planned features are:
- Improved macros
- Improved regular expressions
- RSALT (SALT for RLTL)
- Improved TSALT (SALT for TLTL)
The current alpha version of SALT EO can be tried out here.
It can also be downloaded as part of LamaConv.
SALT EO is developed and maintained by: