Andreas Bauer, Martin Leucker, and Jonathan Streit.
SALT - structured assertion language for temporal logic.
In Proceedings of the Eighth International Conference on Formal Engineering Methods (ICFEM), Macau, China, 2006.
Abstract
This paper presents Salt. Salt is a general purpose specication and assertion language developed for creating concise temporal speci cations to be used in industrial verifcation environments. It incorporates ideas of existing approaches, such as speci cation patterns, but also provides nested scopes, exceptions, support for regular expressions and real-time. The latter is needed in particular for verifcation tasks to do with reactive systems imposing strict execution times and deadlines. However, unlike other formalisms used for temporal specifcation of properties, Salt does not target a specific domain. The paper details on the design rationale, syntax and semantics of Salt in terms of a translation to temporal (real-time) logic, as well as on the realisation in form of a compiler. Our results will show that the higher level of abstraction introduced with Salt does not deprave the effciency of the subsequent verifcation tools - rather, on the contrary.
