Specifying and proving properties of timed I/O automata using Tempo

Myla Archer, Hongping Lim, Nancy Lynch, Sayan Mitra, Shinya Umeno

Research output: Contribution to journalArticlepeer-review

Abstract

Timed I/O automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The Tempo Toolset, currently under development, is aimed at supporting system development based on TIOA specifications. The Tempo Toolset is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on the modeling of timed systems and their properties with TIOA and on the use of TAME4TIOA, the TAME (Timed Automata Modeling Environment) based theorem proving support provided in Tempo, for proving system properties, including timing properties. Several examples are provided by way of illustration.

Original languageEnglish (US)
Pages (from-to)139-170
Number of pages32
JournalDesign Automation for Embedded Systems
Volume12
Issue number1-2
DOIs
StatePublished - Jul 2008
Externally publishedYes

Keywords

  • Automata models
  • Formal methods
  • Hybrid systems
  • Modeling environments
  • Specification
  • System development frameworks
  • Theorem proving
  • Timed automata
  • Tool suites
  • Verification

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Specifying and proving properties of timed I/O automata using Tempo'. Together they form a unique fingerprint.

Cite this