Abstracts - 2006
Translating Timed I/O Automata Specifications for Theorem Proving in PVS
Hongping Lim, Nancy Lynch, Sayan Mitra & Shinya Umeno
Timed Input/Output Automata  is a mathematical framework for compositional specification and analysis of systems with discrete and continuous behavior and discrete communication between components. In prior work, we had designed a formal language called TIOA  to specify timed I/O automata. The key technique used for the analysis of TIOA models is deduction, so it is desirable to be able to use interactive theorem provers (TP) to verify TIOA properties. Advantages of using TPs are: (1) effective management of large proofs, and (2) automation of recurring proof patterns by using TP macros or strategies. To use a TP, however, one has to bear the cost of writing the description of the timed I/O automaton model of the system in the language of the TP (typically some variant of high order logic). The objective of this project is to eliminate this cost by providing a tool that translates automata and property specifications written in the TIOA language to the language of the Prototype Verification System (PVS). PVS is a specification system with an integrated theorem prover for high order logic .
Our approach for translating TIOA to PVS is based on the methodology prescribed in the Timed Automata Modeling Environment (TAME) . TAME provides a PVS theory template that defines the states, actions, and transitions of a generic automaton. This template is manually instantiated with the states, actions, and transitions of a particular automaton, to get a PVS theory that, together with several supporting library theories, completely specify the automaton, its transitions and its reachable states in the language of PVS. Our translator uses this approach of instantiating a theory template with the particulars of the input timed I/O automaton . However, there is an important distinction between the automaton model for which TAME was designed and the timed I/O automaton model. Elapsing of time in a TAME automaton is captured by a special time passage action which increments a special now variable, whereas in the more general timed I/O automaton model, the executions contain trajectories that map intervals of time to values of continuously changing variables. To translate these trajectory definitions to PVS, we add a set of parameterized actions that contain the trajectory map as a parameter. The precondition of these actions enforces the trajectory invariants and the stopping conditions, while the effect of these actions returns the last state of a trajectory.
Written in Java, the translator is a part of the TIOA toolkit [2, 5]. The implementation of the tool builds upon the existing IOA to Larch translator . Currently, a user can use TIOA to describe timed I/O automata and their properties. Upon running the translator, the translator first uses the TIOA front-end type checker  to parse the input TIOA, reporting any errors if necessary. The translator then generates a set of files containing PVS theories specifying the automata and their properties. The user can then invoke the PVS theorem prover to interactively prove these properties. The current implementation of the translator handles only constant differential equations and algebraic equations as a means for specifying the evolution of continuous variables. We are extending the translator to handle more complicated differential equations and differential inclusions.
We have used the translator successfully in the following three verification case studies: (1) the Fischer mutual exclusion algorithm, (2) a two-task race system, and (3) a simple failure detector [1, 7, 8]. In all these case studies, the input to the translator is a TIOA description of the system/algorithm in question and its invariant properties. For 2 and 3 we also have an abstract TIOA specification of the timing properties of the system. The output from the translator is a set of PVS theories specifying the timed I/O automata and their invariant properties. We have used the PVS theorem prover to verify the properties using inductive invariant proofs and simulation relations.
The translator also supports translation of composite automata. A composite automaton describes how various component automata are composed together to obtain a larger system. The translator generates separate definitions for each individual automaton, and then defines the states, precondition predicate and transition function of the composition in terms of the separate definitions. We have successfully translated the LCR example  and proved an invariant of the composition.
We are currently working on the integration of a newer version of the front end type checker with the translator so as to improve usability. We are also updating the existing examples and their proofs to make use of the vocabulary syntax of the TIOA language for defining custom data types, and to make use of the updated version of the TIOA and TAME strategies.
We are also working on the Small Aircraft Transportation System (SATS) problem  and the ABD atomic register algorithm. In future, the translator can also be enhanced to automatically generate partial PVS proof scripts for certain types of properties.
 Dilsun K. Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager. The theory of timed I/O automata. Technical Report MIT/LCS/TR-917, MIT CSAIL, Cambridge, MA, USA, April 2004. http://tioa.csail.mit.edu/
 Dilsun K. Kaynar, Nancy Lynch, Sayan Mitra, and Stephen Garland. The TIOA Language. MIT CSAIL, Cambridge, MA, USA, February 2005. http://tioa.csail.mit.edu/
 Sam Owre, John Rushby, and Natarajan Shankar. PVS: A Prototype Verification System. In 11th International Conference on Automated Deduction (CADE), pp. 748 -- 752, Saratoga, NY, USA, June 1992.
 Myla Archer. TAME: Using PVS Strategies for Special-Purpose Theorem Proving. In Annals of Mathematics and Artificial Intelligence, Vol 29 (1-4), pp. 139 -- 181, February 2001.
 Dilsun Kaynar, Nancy Lynch, and Sayan Mitra. Specifying and proving timing properties with TIOA tools. Work in Progress Session for the In 25th IEEE International Real-Time Systems Symposium (RTSS) Lisbon, Portugal, December 2004.
 Andrej Bogdanov, Stephen Garland, and Nancy Lynch. Mechanical translation of I/O automaton specifications into first-order logic. In Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), pp. 364 -- 368, Texas, Houston, USA, November 2002.
 Nancy Lynch. Distributed Algorithms, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1996.
 Hongping Lim, Dilsun Kaynar and Nancy Lynch. Translating timed I/O automata specifications for theorem proving in PVS. In Formal Modeling and Analysis of Timed Systems (FORMATS), pp. 17--31, Uppsala, Sweden, September 2005.
 Gilles Dowek, César Muñoz, and Victor Carreño. Abstract Model of the SATS Concept of Operations: Initial Results and Recommendations. NASA/TM-2004-213006, pp. 46 NASA, Langley Research Center, Hampton, Virginia, March 2004.