TY - GEN
T1 - Specifying and proving properties of timed I/O automata in the TIOA toolkit
AU - Archer, Myla
AU - Lim, Hong Ping
AU - Lynch, Nancy
AU - Mitra, Sayan
AU - Umeno, Shinya
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=40949166046&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=40949166046&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:40949166046
SN - 1424404215
SN - 9781424404216
T3 - Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
SP - 129
EP - 138
BT - Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
T2 - 4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
Y2 - 27 July 2006 through 30 July 2006
ER -