2006 | OriginalPaper | Buchkapitel
SALT—Structured Assertion Language for Temporal Logic
verfasst von : Andreas Bauer, Martin Leucker, Jonathan Streit
Erschienen in: Formal Methods and Software Engineering
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper presents
Salt
.
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 specification patterns, but also provides nested scopes, exceptions, support for regular expressions and real-time. The latter is needed in particular for verification tasks to do with reactive systems imposing strict execution times and deadlines. However, unlike other formalisms used for temporal specification 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 efficiency of the subsequent verification tools—rather, on the contrary.