Tempo: A Toolkit for the Timed Input/Output Automata Formalism
Abstract
Report developed under STTR contract for topic AFO4-T023. This Phase II project developed an integrated development environment, called Tempo, for specifying, analyzing, and verifying complex distributed system designs. This includes a modeling language, a graphical user interface, and computational support tools. This modeling and analysis framework provides an integrated suite of tools and methods. In more detail, this project developed: (a) a formal modeling language, called Tempo, based on the TIOA (Timed Input/Output Automata) formalism, for specifying timed, asynchronous, and interacting systems components, (b) the language processor for Tempo, incorporating syntax and type checking, and providing interfaces to computer-aided design tools, (c) a simulation tool allowing simulation of specifications and paired simulations of a specification and an abstract implementation, (d) an interface to model-checking tool UPAALL, and (e) theorem-proving link through an interface to PVS.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 30, 2008
- Accession Number
- ADA477189
Entities
People
- Alexander A. Shvartsman
- Nancy Lynch