Specifying and proving properties of timed I/O automata in the TIOA toolkit

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 TIOA toolkit, currently under development, is aimed at supporting system development based on TIOA specifications. The TIOA toolkit 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 modeling of timed systems with TIOA and the TAME-based theorem proving support provided in the toolkit for proving system properties, including timing properties. Several examples are provided by way of illustration.

Original languageEnglish (US)
Title of host publicationProceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
Pages129-138
Number of pages10
StatePublished - 2006
Externally publishedYes
Event4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06 - Napa, CA, United States
Duration: Jul 27 2006Jul 30 2006

Other

Other4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
CountryUnited States
CityNapa, CA
Period7/27/067/30/06

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Hardware and Architecture
  • Software

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

  • Cite this

    Archer, M., Lim, H., Lynch, N., Mitra, S., & Umeno, S. (2006). Specifying and proving properties of timed I/O automata in the TIOA toolkit. In Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06 (pp. 129-138). [1695916]