The Tempo Project

Tempo is a simple formal language for modeling distributed systems with (or without) timing constraints as collections of interacting state machines, called timed input/output automata(TIOA). Tempo provides natural mathematical notations for describing systems, their intended properties, and intended relationships between their descriptions at varying levels of abstraction. The Tempo Toolkit is an implementation of the Tempo language and a suite of tools that supports a range of validation methods for descriptions of systems and their properties, including static analysis, simulation, and machine-checked proofs.