TTM/PAT: Specifying and Verifying Timed Transition Models

Timed Transition Models (TTMs) are event-based descriptions for specifying real-time systems in a discrete setting. We propose a convenient and expressive event-based textual syntax for TTMs and a corresponding operational semantics using labelled transition systems. A system is specified as a composition of module instances. Each module has a clean interface for declaring input, output, and shared variables. Events in a module can be specified, individually, as spontaneous, fair or real-time. An event action specifies a before-after predicate by a set of (possibly non-deterministic) assignments and nested conditionals. The TTM assertion language, linear-time temporal logic (LTL), allows references to event occurrences, including clock ticks (thus allowing for a check that the behaviour is non-Zeno). We implemented a model checker for the TTM notation (using the PAT framework) that includes an editor with static type checking, a graphical simulator, and a LTL verifier. The tool automatically derives the tick transition and implicit event clocks, removing the burden of manual encoding them. The TTM tool performs significantly better on a nuclear shutdown system than the manually encoded versions analyzed in [6].