You are here

Home › Research › Projects ›

SALT – Structured Assertion Language for Temporal Logic

Salt

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

You can try out SALT using this web interface.

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

Download

Note that you need Hugs and JAVA to run the SALT compiler.

People

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)

Get it

The current alpha version of SALT EO can be tried out here.

It can also be downloaded as part of LamaConv.

People

SALT EO is developed and maintained by:

For more information, please contact  Sebastian Hungerecker or Malte Schmitz.