@InProceedings{ALLMU:memocode06,
  author    = {Myla Archer and Hongping Lim and Nancy Lynch and Sayan Mitra and Shinya Umeno},
  title     = {Specifying and Proving Properties of Timed {I/O} Automata in the {TIOA} Toolkit},
  booktitle = {In Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06)},
  year      = {2006},
  publisher = {IEEE},
  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, 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 TAMEbased theorem proving support provided in the TIOA toolkit for proving system properties, including timing properties. Several examples are provided by way of illustration.},
  biburl    = {http://users.crhc.illinois.edu/mitras/research.html},
  keywords  = {Automated deduction, Specification languages},
  pdfurl    = {research/2006/memocode06.pdf},
  url       = {http://ieeexplore.ieee.org/search/wrapper.jsp?arnumber=1695916},
}