Salt is a general purpose specification and assertion language developed for creating concise temporal specifications to be used in industrial verification environments. It incorporates ideas of existing approaches, such as PSL or Specification Patterns, in that it provides operators to express scopes and exceptions, as well as support for a subset of regular expressions. On the one hand side, Salt exceeds specific features of these approaches, for example, in that it allows the nesting of scopes and supports the specification of real-time properties. On the other hand, Salt is fully translatable to LTL, if no real-time operators are used, and to TLTL (also known as state-clock logic), if real-time operators appear in a specification. The latter is needed in particular for verification tasks to do with reactive systems imposing strict execution times and deadlines. Salt's semantics is defined in terms of a translation to temporal (real-time) logic, and a compiler is freely available from the project web site, including an interactive web interface to test drive the compiler. This tutorial paper details on the theoretical foundations of Salt as well as its practical use in applications such as model checking and runtime verification.

Original languageEnglish
Title of host publication NASA Formal Methods
EditorsM. Bobaru, K. Havelund, G. Holzmann, R. Joshi
Number of pages28
Volume6617 LNCS
Place of PublicationBerlin
PublisherSpringer Verlag
Publication date26.04.2011
ISBN (Print)978-3-642-20397-8
ISBN (Electronic)978-3-642-20398-5
Publication statusPublished - 26.04.2011
Event3rd NASA Formal Methods Symposium - Pasadena, United States
Duration: 18.04.201120.04.2011
Conference number: 84589


Dive into the research topics of 'The Theory and Practice of SALT'. Together they form a unique fingerprint.

Cite this