Tempo: A Toolkit for The Timed Input/Output Automata Formalism

N. Lynch; L. Michel; A.A. Shvartsman

Industry Track to The First International Conference on Simulation Tools and Techniques for Communications, Networks and Systems

Research Article

Tempo: A Toolkit for The Timed Input/Output Automata Formalism

Cite: BibTeX Plain Text

@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

N. Lynch¹^,*, L. Michel²^,*, A.A. Shvartsman²^,*

1: CSAIL, MIT, The Stata Center, Building 32, 32 Vassar Street, Cambridge, MA 02139
2: CSE, University of Connecticut, 371 Fairfield Way, Storrs, CT 06269-2155

*Contact email: lynch@theory.csail.mit.edu, ldm@engr.uconn.edu, aas@engr.uconn.edu

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.

Keywords: Input Output Automata Timed Input Output Automata Distributed Algorithms Specification Verification

Published: 2010-05-16
Publisher: ACM

: http://dx.doi.org/10.4108/ICST.SIMUTOOLS2008.3105