The TIOA Language and Toolset

TIOA is a formal language for modeling distributed systems with (or without) timing constraints as collections of interacting state machines, called timed input-output automata. The language can be used to model systems at different levels of abstraction and to express properties (invariants and implementation relationships) that systems are intended to satisfy. An accompanying toolset enables users to check their specifications.

Documentation

The TIOA User Guide and Reference Manual by Stephen J. Garland (September 30, 2005) contains a tutorial on timed input/output automata and the TIOA language. (Microsoft Word)

The Theory of Timed I/O Automata by Dilsun K. Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager (March 2, 2005) describes the mathematical foundations of timed input/output automata. (PDF)

A library of sample specifications (including those in the TIOA User Guide) illustrates the use of the TIOA language. (Index)

Tools

The TIOA Checker checks the syntax and static semantics of TIOA specifications. A preliminary version is available for use via the Web. (Checker)

The TIOA Simulator simulates execution of timed input/output automata. (Simulator)

A TIOA/PVS Interface is being developed to facilitate the use of the PVS proof system for verifying properties of timed input/output automata expressed in the TIOA Language. (TIOA to PVS Translator)

Last modified September 30, 2005.
Send questions and comments to garland@csail.mit.edu