Temporal notations are widely accepted for formal specification of functional properties amenable to automated formal verification. The SALT temporal specification language was developed as an extension of the popular LTL notation to simplify creating temporal specifications: it provides, among others, concise operators and restricted regular expressions. SALT formulas can be translated to LTL by a freely available compiler and thereby directly used for model checking. Clearly defined semantics of the specification notation is indispensable for creating precise unambiguous descriptions of the desired behavioural properties and for making subsequent formal verification meaningful. SALT semantics has been given through translation to LTL so far, which is in parts rather sophisticated and not easily comprehensible. This report presents a clear and explicit semantics formalisation for a substantial language subset of SALT through translation to an expressive interval temporal logic with explicit time variables. The formal definition and validation is performed in the Isabelle/HOL theorem prover. In the course of the formal validation we particularly prove that the semantics resulting from translation to LTL is equivalent to the explicit semantics definition.     «

Temporal notations are widely accepted for formal specification of functional properties amenable to automated formal verification. The SALT temporal specification language was developed as an extension of the popular LTL notation to simplify creating temporal specifications: it provides, among others, concise operators and restricted regular expressions. SALT formulas can be translated to LTL by a freely available compiler and thereby directly used for model checking. Clearly defined semantics...     »