TTM / PAT : A Tool for Modelling and Verifying Timed Transition Models

Timed Transition Models (TTMs) are event based descriptions for specifying and verifying real-time systems in a discrete setting. While the verification of TTMs has been supported in tools such as Uppaal and SAL, the manual encoding requires substantial effort before a TTM can be checked. We propose a convenient and expressive textual syntax for TTMs and a corresponding one-step operational semantics. Modules allow for compositional reasoning and include an interface in which monitored and controlled variables are declared. 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 (possibly nested) conditionals. The TTM assertion language, LTL, allows references to event occurrences, including clock ticks (thus allowing for a check that the behaviour is non-zeno). We describe a tool that includes an editor with static type checking, a graphical simulator and a LTL verifier (as a plug-in for the PAT toolset). The tool automatically derives the tick transition and implicit event clocks so that the burden of manual encoding is removed. The TTM tool performs significantly better on a nuclear shutdown system than the manually encoded version