Research Article
Tempo: A Toolkit for The Timed Input/Output Automata Formalism
@INPROCEEDINGS{10.4108/ICST.SIMUTOOLS2008.3105 , author={N. Lynch and L. Michel and A.A. Shvartsman}, title={Tempo: A Toolkit for The Timed Input/Output Automata Formalism}, proceedings={Industry Track to The First International Conference on Simulation Tools and Techniques for Communications, Networks and Systems}, publisher={ACM}, proceedings_a={SIMULATIONWORKS}, year={2010}, month={5}, keywords={Input Output Automata Timed Input Output Automata Distributed Algorithms Specification Verification}, doi={10.4108/ICST.SIMUTOOLS2008.3105 } }- N. Lynch
L. Michel
A.A. Shvartsman
Year: 2010
Tempo: A Toolkit for The Timed Input/Output Automata Formalism
SIMULATIONWORKS
ICST
DOI: 10.4108/ICST.SIMUTOOLS2008.3105
Abstract
Tempo is a simple formal language for modeling distributed, concurrent, and timed systems as collections of interacting state machines, called timed input/output automata. 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. This paper gives a brief overview of the Tempo language and illustrates its utility on selected examples of importance to distributed computing. The focus of the presentation is on the Tempo tools, and in particular, the simulator.
