TitleSpecifying and Proving Properties of Timed I/O Automata in the TIOA Toolkit
Publication TypeConference Proceedings
Year of Publication2006
AuthorsArcher, M., HP. Lim, N. Lynch, S. Mitra, and S. Umeno
Conference NameFourth ACM \& IEEE International Conference on Formal Methods and Models for Co-Design
Pagination129-138
Conference LocationNapa, California
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.

Full Text

Archer etal2006.pdf

NRL Publication Release Number

06-1226-1470