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]. © Springer International Publishing Switzerland 2014.
CITATION STYLE
Ostroff, J. S., Wang, C. W., Hudon, S., Liu, Y., & Sun, J. (2014). TTM/PAT: Specifying and Verifying Timed Transition Models. In Communications in Computer and Information Science (Vol. 419 CCIS, pp. 107–124). Springer Verlag. https://doi.org/10.1007/978-3-319-05416-2_8
Mendeley helps you to discover research relevant for your work.