Skip Navigation
York U: Redefine the PossibleHOME | Current Students | Faculty & Staff | Research | International
Search »FacultiesLibrariesCampus MapsYork U OrganizationDirectorySite Index
Future Students, Alumni & Visitors
2013 Technical Reports

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

Jonathan S. Ostroff, Chen-Wei Wang and Simon Hudon

Technical Report CSE-2013-05

York University

June 3 2013


Timed Transition Models (TTMs) are event based systems for specifying real-time and reactive 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. In the TTM syntax, a tick transition (representing a global discrete clock) and implicit event clocks are no longer a (significant) burden of the specifier but are derived automatically. 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). Tool support, including an editor with static type checking, a graphical simulator and a LTL verifier, is provided as a plug-in for the PAT toolset. The TTM tool performs significantly better on a nuclear shutdown system than the manually encoded version in Uppaal and SAL.

Download paper in PDF format.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.