Introduction

Timed Input/Output Automata [1] 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 [2] 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 [3].

Approach

Our approach for translating TIOA to PVS is based on the methodology prescribed in the Timed Automata Modeling Environment (TAME) [4]. 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 [5]. 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.

Progress

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 [6]. 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 [2] 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]. 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.

We plan to extend the translator to support other features of the TIOA language, including user-defined types as well as nondeterminism in actions and trajectories. We are also working on the Small Aircraft Transportation System (SATS) problem [8] 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.

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. The theory of timed I/O automata, Technical Report MIT/LCS/TR-917, MIT CSAIL, Cambridge, MA, USA, April 2004. http://theory.lcs.mit.edu/~dilsun/Publications/TIOA.ps

[2] Dilsun K. Kaynar, Nancy Lynch, Sayan Mitra, and Stephen Garland. The TIOA Language, MIT CSAIL, Cambridge, MA, USA, February 2005.

[3] Sam Owre, John Rushby, and Natarajan Shankar. PVS: A Prototype Verification System, 11th International Conference on Automated Deduction (CADE), pp. 748 -- 752, Saratoga, NY, USA, June 1992.

[4] Myla Archer. TAME: Using PVS Strategies for Special-Purpose Theorem Proving, Annals of Mathematics and Artificial Intelligence, Vol 29 (1-4), pp. 139 -- 181, February 2001.

[5]Dilsun Kaynar, Nancy Lynch, and Sayan Mitra. Specifying and proving timing properties with TIOA tools, Work in Progress Session for the 25th IEEE International Real-Time Systems Symposium (RTSS 2004), Lisbon, Portugal, December 2004.

[6] Andrej Bogdanov, Stephen Garland, and Nancy Lynch. Mechanical translation of I/O automaton specifications into first-order logic. 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.

[7] Nancy Lynch. Distributed Algorithms, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1996.

[8] 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.