Introduction

The timed I/O automaton (TIOA) modeling framework is a mathematical framework that supports description and analysis of timing-based systems [1]. We are developing a suite of software tools, the TIOA toolkit, that is intended to assist system designers in modeling, testing and verifying their designs within the TIOA framework. The TIOA toolkit is being developed as an extension of the IOA toolkit [2,3] . The IOA toolkit serves the same purpose as the TIOA toolkit but its capabilities are limited to system designs that do not involve any timing constraints.

The TIOA simulator is a tool that is being developed as a part of the TIOA toolkit to facilitate the execution of TIOAs and the checking of a given simulation relation between the states of a pair of automata for a specified number of steps. Our design has been influenced by our preference to preserve the architecture of the current IOA toolkit and to reuse its code to the extent it is possible.

The TIOA simulator admits a subset of the TIOA language [4] , called TIOA-sim, as its specification language. The language TIOA-sim consists of three parts: (1) a language for specifying simulatable TIOA programs, (2) a language for nondeterminism resolution (NDR), and (3) a language for asserting simulation relations and step correspondences for use in paired simulations.

Approach

Our approach is to design and implement these three parts of the TIOA-sim language in three corresponding phases. In each phase, once the design is complete, it is communicated to the developers of the front-end of the toolkit, which supports syntax and static-semantics checking of the new language constructs. The front-end development can then proceed independently of our implementation of the intermediate language that is shared by all the back-end tools in the toolkit and the simulator itself.

Progress

We have completed the first two phases of the project. Currently, the TIOA simulator can be used to execute a single TIOA at a time. We have tested our implementation on non-trivial TIOA specifications such as the two-task-race and Fischer's mutual exclusion algorithms [5] well-known in the distributed algorithms literature. We have completed the design of the paired simulator and its implementation is underway. In the process of doing our implementation work, we have reorganized the structure of the existing simulator package in the toolkit so that it can be maintained and extended more easily.

Future Work

After completing the implementation of the paired simulator, we will asses the newly introduced features of the simulator by conducting more experiments that involve checking whether an algorithm implements its specification. Another focus of future work will be on improving the user interface of the simulator and on adding interactive features.

Research Support

This project is supported by DARPA Air Force contract number FA9550-04-C-0084, DARPA Award number F33615-01-C-1896, NSF Award numbers CCR-0326277 and CCR-0121277, NSF-Texas Engineering Experiment Station grant 64961-CS, DARPA/AFOSR MURI Award F49620-02-1-0325 and MURI AFOSR Award Number SA2796PO 1-0000243658.

References

[1] Dilsun K. Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager. Timed I/O Automata: A Mathematical Framework for Modeling and Analyzing Real-Time Systems. In Proceedings of the 24th IEEE International Real-Time Systems Symposium (RTSS '03) , Cancun, Mexico, pages 166-177, December, 2003. IEEE Computer Society. (Full version available as Technical Report MIT/LCS/TR-917a.)

[2] Dilsun Kaynar, Anna Chefter, Laura Dean, Stephen J. Garland, Nancy A. Lynch, Toh Ne Win, and Antonio Ramirez-Robredo. Simulating Nondeterministic Systems at Multiple Levels of Abstraction. In Tools Day held in conjunction with CONCUR '02 , Brno, Czech Republic, August 2002.

[3] Stephen J. Garland and Nancy A. Lynch. Using I/O Automata for Developing Distributed Systems. In Gary T. Leavens and Murali Sitaraman, editors, Foundations of Component-Based Systems , pages 285-312, Cambridge University Press, 2000.

[4] The TIOA Modeling Language. Manuscript. 2005.

[5] Nancy Lynch. Distributed Algorithms Morgan Kaufmann Publishers, San Mateo, CA, 1996.