Tempo Front-end

Tempo Front-end is not a plugin, rather a platform for other plugins, each with its own functionality. Function of the Front-end is to ensure proper typing of the model (syntactic and semantic check). Errors in the model specification will be reported to the user. Documentation on the Tempo language and the Timed I/O Automata model can be found on the Welcome page.


LaTeX translator

As the name suggest this tool allows translation of models expressed in the Tempo toolkit to the LaTeX format. Hance saving much valuable time during documentation of the project.


Simulator

Formal correctness proofs for distributed systems can be long, hard or tedious to construct. Simulation can be used as a way of testing automata before development of correctness proofs begins. The execution of a Tempo automaton either reveals bugs or increases the confidence that the automaton works as expected.

The Simulator can assist users in constructing correctness proofs. By describing a system or an algorithm as a Tempo program and simulating it, a user gains a better understanding of how it works. This can guide the strategy to be followed in proving correctness. Moreover, the invariants which are observed to be true for the simulated executions constitute candidates for useful lemmas in a full correctness proof.

Simulation in general is an efficient method for exposing possible deficiencies in the design of systems and algorithms which can lead to the correction of discovered errors, revision of proofs or tuning for better performance.

Tempo automata are nondeterministic (even ones with time constraints), hence in order to simulate the model all sources of nondeterminism must be resolved. The mechanism for doing this is the schedule block that must be provided. Note that the Tempo toolset does not make any attempt at verification of the schedule (checking liveness or correctness).

Documentation: The Tempo Simulator Manual


UPPAAL translator (Beta)

Model checking, the problem of deciding whether a correctness property specified in temporal logic holds of a system specification, is a well-established system and software verification technique. The Tempo Toolkit tookit supports model checking indirectly. Meaning, this plugin translates the Tempo automata to form (XTA notation) suitable for input of UPPAAL tool, which itself performs the task of model checking.

However, there is also a mismatch between Tempo and UPPAAL concerning the kinds of data structures the two languages support. Readying a Tempo specification for translation into XTA therefore requires providing a standard, UPPAAL-based implementation of those data structures supported by Tempo but not by Uppaal.

For example, we provide a standard implementation of Tempo (finite) sets as finite arrays in UPPAAL. The translation scheme is based on the version (4.1.0) of UPPAAL, which includes extended support for array variables (quantification and nondeterministic choice over array indices), structures, external functions, and the use of logical implication within state invariants. Consequently, the resulting XTA code is essentially in a 1-to-1 relationship with the original Tempo (Tempaal) specification, resulting in very short learning curves for experienced Tempo users.

This plugin generates code that serves as an imput to the UPPAAL tool. Follow the listed links for UPPAAL documentation and tool:

Documentation: The Tempo Model Checker User Guide and Reference Manual


PVS translator

Verification of timed I/O automata properties typically involves proving invariants of individual automata or proving simulation relations between pairs of automata. The key technique for proving both invariants and simulation relations for state-machine models like the timed I/O automata is induction. The timed I/O automata framework provides a means for constructing very stylized proofs, which take the form of induction over the length of the executions of an automaton or a pair of automata, and a systematic case analysis of the actions and the trajectories. Therefore, it is possible to partially automate such proofs by using an interactive theorem prover, such as PVS.

To use a theorem prover like PVS for verification, one has to write the description of the timed I/O automaton model of the system in the language of PVS, which is based on classical, typed higher-order logic. One could write this automaton specification directly in PVS, but using the TIOA language has the following advantages:

  • TIOA preserves the state-transition structure of a timed I/O automaton,
  • TIOA allows the user to write programs to describe the transitions using operational semantics, whereas in PVS, transition definitions have to be functions or relations,
  • TIOA provides a natural way for describing trajectories using differential equations, and also,
  • TIOA allows one to use other tools in the TIOA toolkit.
Therefore, it is desirable to be able to write the description of a timed I/O automaton in the TIOA language, and then use an automated tool to translate this description to the language of PVS.

This plugin generates code that serves as an imput to the PVS Specification and Verification System. The PVS tool and documentation can be found at pvs.csl.sri.com

Documentation: Translating Timed I/O Automata Specifications for Theorem Proving in PVS. (H. Lim)


Java translator (Alpha)

This work is very much in progress and the detailed documentation is forthcoming.

As the name suggest, function of this plugin is to generate executable Java codes from models specified in Tempo. Motivation for this tool is derivation of executable code that is verified to be correct, meaning, code that preserves the safety and liveness properties of its source specification. Timed Input/Output Automata framework enable specification of complex concurrent systems, timed or asynchronous, and to reason about their correctness. Additionally, this formal framework allows specifications to be developed incrementally by successively adding new levels of details, and verifying that each successive refinement generates a subset of its predecessor’s behaviors (hence solving the same system). The benefits of using formal methods are jeopardized during the process of manual translation into executable code, when high level constructs and component relationships are left up to the programmer’s personal interpretation. This process opens the possibility of undesirable and errors behaviors being introduced into the final executable system. Hence the contribution of this work is the design and implementation of an automated translator for the Timed Input/Output Automata model for various deployment platforms; with some restrictions on the properties of the source specifications.

Documentation: Using Timed Input/Output Automata for Implementing Distributed Systems. (P. M. Musial)