Using TAME to prove invariants of automata models: Two case studies

ABSTRACT

TAME is a special-purpose interface to PVS designed to support developers of software systems in proving properties of automata models. One of TAME's major goals is to allow a software developer who has basic knowledge of standard logic, and can do hand proofs, to use PVS to represent and to prove properties about an automaton model without first becoming a PVS expert. A second goal is for a human to be able to read and understand the content of saved TAME proofs without running them through the PVS proof checker. A third goal is to make proving properties of automata with TAME less costly in human time than proving such properties using PVS directly. Recent work by Romijn and Devillers et al., based on the I/O automata model, has provided the basis for two case studies on how well TAME achieves these goals. Romijn specified the RPC-Memory Problem and its solution, while Devillers et al. specified a tree identify protocol. Hand proofs of specification properties were provided by the authors. In addition, Devillers et al. used PVS directly to mechanize the specifications and proofs of the tree identify protocol. In one case study, the third author, a new TAME user with no previous PVS experience, used TAME to create PVS specifications of the I/O automata presented by Romijn and Devillers et al. and to check the hand proofs of invariant properties. The PVS specifications and proofs of Devillers et al. \hspace*{-.03in} provide the basis for the other case study, which compares the TAME approach to an alternate approach which uses PVS directly.

REFERENCES

• 1: Andrea Alborghetti , Angelo Gargantini , Angelo Morzenti, Providing automated support to deductive analysis of time critical systems, Proceedings of the 6th European conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, p.211-226, September 22-25, 1997, Zurich, Switzerland
• 2: M. Archer. Tools for simplifying proofs of properties of timed automata: The TAME template, theories, and strategies. Technical Report NRL/MR/5540-99-8359, NRL, Wash., DC, 1999.
• 3: M. Archer , C. Heitmeyer, Mechanical verification of timed automata: a case study, Proceedings of the 2nd IEEE Real-Time Technology and Applications Symposium (RTAS '96), p.192, June 10-12, 1996
• 4: Myla Archer , Constance L. Heitmeyer, Human-Style Theorem Proving Using PVS, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, p.33-48, August 19-22, 1997
• 5: Myla Archer , Constance L. Heitmeyer, Verifying Hybrid Systems Modeled as Timed Automata: A Case Study, Proceedings of the International Workshop on Hybrid and Real-Time Systems, p.171-185, March 26-28, 1997
• 6: Myla Archer, Constance Heitmeyer, and Steve Sims. TAME: A PVS interface to simplify proofs for automata models. In Proc. User Interfaces for Theorem Provers 1998 (UITP '98), Eindhoven, Netherlands, July 1998.
• 7: Butler R. W., An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot, NASA Langley Technical Report Server, 1996
• 8: Ricky W. Butler, James L. Caldwell, Victor A. Carreffo no, C. Michael Holloway, Paul S. Miner, and Ben L. Di Vito. NASA Langley's research and technology-transfer program in formal methods. In Proc. 10th Annual Conf. on Computer Assurance (COMPASS'95), pages 135-149, Gaithersburg, MD, June 1995. IEEE Computer Society Press.
• 9: Judith Crow and Ben L. Di Vito. Formalizing space shuttle software requirements. In Proc. First ACM Workshop on Formal Methods in Software Practice (FMSP'96), pages 40-48, San Diego, CA, January 1996.
• 10: Judith Crow , Ben Di Vito, Formalizing space shuttle software requirements: four case studies, ACM Transactions on Software Engineering and Methodology (TOSEM), v.7 n.3, p.296-332, July 1998 [doi>10.1145/287000.287023]
• 11: M. Devillers. Verification of a tree-identity protocol. URL http://www.cs.kun.nl/~marcod/1394.html, 1997.
• 12: Marco Devillers , David Griffioen , Judi Romijn , Frits Vaandrager, Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394, Formal Methods in System Design, v.16 n.3, p.307-320, June 2000 [doi>10.1023/A:1008764923992 ]
• 13: Marco Devillers. Private communication. January, 1999.
• 14: Alan Fekete , Nancy Lynch , Alex Shvartsman, Specifying and using a partitionable group communication service, Proceedings of the sixteenth annual ACM symposium on Principles of distributed computing, p.53-62, August 21-24, 1997, Santa Barbara, California, United States [doi>10.1145/259380.259422]
• 15: S. J. Garland and N. A. Lynch. The IOA Language and Toolset: Support for Designing, Analyzing, and Building Distributed Systems. Draft. MIT Laboratory for Computer Science, August, 1998.
• 16: Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998 [doi>10.1109/32.730543 ]
• 17: Pertti KelloMaki. Mechanical Veri~cation of Invariant Properties of DisCo Speci~cations. PhD thesis, Tampere University ofTechnology, Finland, November 1997.
• 18: L. Lamport. How to write a proof.Technical report, Digital Equipment Corp., System Research Center, February 1993. Research Report 94.
• 19: Patrick Lincoln. Private communication. July, 1998.
• 20: Victor Luchangco. Using simulation techniques to prove timing properties. Master's thesis, Massachusetts Institute of Technology, June 1995.
• 21: N. Lynch and M. Tuttle. An introduction to Input/Output automata. CWI-Quarterly, 2(3):219-246, September 1989. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands.
• 22: Nancy Lynch , Frits Vaandrager, Forward and backward simulations I.: untimed systems, Information and Computation, v.121 n.2, p.214-233, Sept. 1995 [doi>10.1006/inco.1995.1134 ]
• 23: Nancy Lynch , Frits Vaandrager, Forward and backward simulations II.: timing-based systems, Information and Computation, v.128 n.1, p.1-25, July 10, 1996 [doi>10.1006/inco.1996.0060 ]
• 24: Steven P. Miller, The Industrial Use of Formal Methods: Was Darwin Right?, Proceedings of the Second IEEE Workshop on Industrial Strength Formal Specification Techniques, p.74, October 20-23, 1998
• 25: S. P. Miller , M. Srivas, Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods, Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques, p.2, April 05-08, 1995
• 26: Olaf Mueller. A Verification Environment for I/O Automata Based on Formalized Meta-Theory. PhD thesis, Technische Universitaet Muenchen, September 1998.
• 27: J. Romijn. Tackling the RPC-Memory Specification Problem with I/O automata. Addendum. URL http://www.cwi.nl/~judi/papers/ dagstuhl proofs.ps.gz.
• 28: Judi Romijn, Tackling the RPC-Memory Specification Problem with I/O Automata, Formal Systems Specification, The RPC-Memory Specification Case Study (the book grow out of a Dagstuhl Seminar, September 1994), p.437-475, January 1996
• 29: P. Rudnicki and A. Trybulec. A note on \How to Write a Proof ". In Proc. 1992 Workshop on Types and Proofs for Programs, June 1996. Available through P. Rudnicki's web page at http://www.cs.ualberta.ca/~piotr/Mizar/.
• 30: Jens Ulrik Skakkebæk , Natarajan Shankar, Towards a Duration Calculus Proof Assistant in PVS, Proceedings of the Third International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.660-679, September 19-23, 1994

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.3 Software Management
          Subjects: Software development

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Management, Performance, Theory, Verification

Keywords:
Software engineering, formal methods, software requirements analysis, theorem proving, verification