As described in Ost99, Timed Transitions Models (TTMs) are used to describe reactive systems with timing constraints. The graphical model-checking tool, described in Ost99, is no longer supported. In the paper by Lawford et. al., Fundamenta Informaticae, 2006, a nuclear reactor shutdown system is described in terms of TTMs. The TTMs were manually encoded into Uppaal and SAL model-checkers in order to check their safety and liveness properties. The manual encoding into Uppaal or SAL requires substantial effort before a TTM can be checked.

This site makes available a TTM plug-in for the PAT toolset for model-checking TTMs. Encodings to labelled transitions systems are done automatically, so that TTMs can be simulated and checked using the efficient algorithms of the PAT tool. PAT is a self-contained framework that supports composing, simulating and reasoning about concurrent, real-time systems and other possible domains. It comes with support for user friendly interfaces, model editors and animated simulators. PAT provides various model checking algorithms for checking deadlock-freeness, divergence-freeness, reachability, LTL properties with fairness assumptions, refinement checking and probabilistic model checking. Partial order reduction, symmetry reduction, process counter abstraction, and parallel model checking algorithms are supported.

For the TTM plug-in, 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.

Acknowledgements: The TTM/PAT plug-in was developed by a team in the Software Engineering Laboratory, at York University (Jonathan S. Ostroff, Chen-Wei Wang and Simon Hudon). Our sincere thanks to Prof. Yang Liu (School of Computer Engineering, Nanyang Technological University) and to Prof. Jun Sun (Singapore University of Technology and Design) for their development of the PAT toolset and for their help in developing the plug-in.

Jonathan S. Ostroff, Chen-Wei Wang, and Simon Hudon. TTM/PAT: A Tool for Modelling and Verifying Timed Transition Models. Tech Report CSE-2013-05, York University, 2013. [PDF]

Jonathan S. Ostroff, Chen-Wei Wang, Simon Hudon, Yang Liu, and Jun Sun. TTM/PAT: Specifying and Verifying Timed Transition Models. In Formal Techniques for Safety-Critical Systems (FTSCS), volume 419 of Communications in Computer and Information Science (CCIS), pages 107–124. Springer, 2013. [PDF]

• The PAT toolset runs under the Windows operating system.

• The TTM/PAT plug-in currently runs under PAT 3.44

• Download ttm-plugin.zip and unzip. There are 4 files in this folder:
  1. PAT3.Setup.344.64.msi
  2. PAT.Common.dll
  3. PAT.Module.TTM.dll
  4. Syntax.xshd

• Invoke the first file to install the PAT toolkit. The installation folder should be something like: C:\Program Files\Process Analysis Toolkit\Process Analysis Toolkit 3.4.4\. We refer to this directory as $PAT.

• Place the second file PAT.common.dll in $PAT.

• In directory $PAT/Modules, create a folder called TTM. Place the last two files PAT.Module.TTM.dll and Syntax.xshd in the TTM folder.

• Invoke the PAT tool. File –> New will allow the designer to describe a new TTM. The designer can edit and statically type check TTMs (F5), simulate the behaviour (F6) and verify the properties (F7). See below.

• To see the list of distributed examples of TTM, select from Examples:
  • Train Gate v1 - multiple controller events
  • Train Gate v2 - single controller event using guarded commands
  • Fischer's Mutual Exclusion Algorithm - using indexed parallel operator
  • Dinning Philosopher v1 - symmetric ring structure that causes deadlock
  • Dinning Philosopher v2 - asymmetric ring structure that avoids deadlock
  • Bridge System v1 - untimed version
  • Bridge System v2 - timed version
  • Alarm System
  • Pacemaker - decomposition of heart and controller, use of shared variables

• The current version of PAT/TTM works with a specialized version of PAT.Common.dll.
  This means: before running RTS/PAT, if TTM/PAT has already been installed, resotre PAT.Common.dll to the original version that is shipped with the executable of PAT 3.4.4.

• Tutorial on using TTM/PAT to specify, simulate, and verify TTMs. [YouTube].

• Recording of the presentation (by Chen-Wei Wang)on FTSCS'13. [YouTube]. [slides]

Notations:

• Keywords are in boldface (e.g. define, ARRAY, etc).
• Symbols are in single quotes (e.g. '[', '(', etc).
• Terminals are in all capitals (e.g. ID).
• Non-Terminals are capitalized and in italics (e.g. TimedEvent, InterfaceVar), possibly followed by:
  • + to denote one or more occurrences
  • ? to denote zero or one occurrence
  • * to denote zero or more occurrences
• Comments are enclosed within \* and */
• LTLFormula may use the temporal connective [] (henceforth), <> (eventually), X (next), U (until), and/or R (release).
• Each state formula cannot be directly written in an assertion; instead, a macro should be defined.
  For example,
  #define x_gt_zero (x >= 0);
  #assert System |= []<>x_gt_zero;
  where System is a declared module composition.

Download the above grammar of textual TTM.

• To see an example of how the static type checking works, add a new shared variable to the share initialization … end section: x : 0 .. 1 = 0.

• Then, in the instances … end section, replace H = HEART(share pace, …) by H = HEART(share x, …).

• Then click on Check Grammar and see the generated error message.

* Click on Simulate to enter the simulation mode.

* Click on Verify to enter the simulation mode.

Results of comparing TTM/PAT and other real-time model checking tools are available here.

• Concurrent Deque (using user-defined C# library classes)

• Indexed and Synchronous Events