Skip to main content

The theory and practice of SALT

Authors

Andreas Bauer and Martin Leucker

NICTA

Australian National University

Technische Universitaet Muenchen
Germany

Abstract

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.

BibTeX Entry

  @inproceedings{Bauer_Leucker_11,
    publisher        = {Springer},
    author           = {Bauer, Andreas and Leucker, Martin},
    month            = apr,
    editor           = {{M. Bobaru, K. Havelund, G. Holzmann, R. Joshi}},
    year             = {2011},
    keywords         = {temporal logic, specification, verification},
    title            = {The Theory and Practice of {SALT}},
    booktitle        = {NASA Formal Methods Symposium (NFM)},
    pages            = {28},
    address          = {Pasadena, CA, USA}
  }

Download

Served by Apache on Linux on seL4.