×

Translation templates to support strategy development in PVS. (English) Zbl 1277.68243

Archer, Myler (ed.) et al., Proceedings of the 6th international workshop on strategies in automated deduction (STRATEGIES 2006), Seattle, WA, USA, August 16, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 11, 59-79 (2007).
Summary: In presenting specifications and specification properties to a theorem prover, there is a tension between convenience for the user and convenience for the theorem prover. A choice of specification formulation that is most natural to a user may not be the ideal formulation for reasoning about that specification in a theorem prover. However, when the theorem prover is being integrated into a system development framework, a desirable goal of the integration is to make use of the theorem prover as easy as possible for the user. In such a context, it is possible to have the best of both worlds: specifications that are natural for a system developer to write in the language of the development framework, and representations of these specifications that are well matched to the reasoning techniques provided in the prover. In a tactic-based prover, these reasoning techniques include the use of tactics (or strategies) that can rely on certain structural elements in the theorem prover’s representation of specifications. This paper illustrates how translation techniques used in integrating PVS into the TIOA (timed input/output automata) system development framework produce PVS specifications structured to support development of PVS strategies that implement reasoning steps appropriate for proving TIOA specification properties.
For the entire collection see [Zbl 1273.68013].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

TAME; Uppaal; LARCH
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Archer, M.; Heitmeyer, C.; Riccobene, E., Proving invariants of I/O automata with TAME, Automated Software Engineering, 9, 3, 201-232 (2002) · Zbl 1034.68572
[2] Archer, Myla, TAME: Using PVS strategies for special-purpose theorem proving, Annals of Mathematics and Artificial Intelligence, 29, 1-4, 139-181 (2000), Published Feb. 2001 · Zbl 1001.68127
[3] Myla Archer. Basing a modeling environment on a general purpose theorem prover. Technical Report NRL/MR/5546-06-8952, NRL, Wash., DC, Dec. 2006; Myla Archer. Basing a modeling environment on a general purpose theorem prover. Technical Report NRL/MR/5546-06-8952, NRL, Wash., DC, Dec. 2006
[4] Myla Archer, HongPing Lim, Nancy Lynch, Sayan Mitra, and Shinya Umeno. Specifying and proving properties of Timed I/O Automata in the TIOA Toolkit. In Formal Methods and Models for Codesign (MEMOCODE 2006); Myla Archer, HongPing Lim, Nancy Lynch, Sayan Mitra, and Shinya Umeno. Specifying and proving properties of Timed I/O Automata in the TIOA Toolkit. In Formal Methods and Models for Codesign (MEMOCODE 2006)
[5] James Arvo. Computer aided serendipity: The role of autonomous assistants in problem solving. In Proc. of Graphics Interface ’99; James Arvo. Computer aided serendipity: The role of autonomous assistants in problem solving. In Proc. of Graphics Interface ’99
[6] Andrej Bogdanov, Stephen Garland, and Nancy Lynch. Mechanical translation of I/O automaton specifications into first-order logic. In Formal Techniques for Networked and Distributed Systems - FORTE 2002 : 22nd IFIP WG 6.1 Intern. Conf.; Andrej Bogdanov, Stephen Garland, and Nancy Lynch. Mechanical translation of I/O automaton specifications into first-order logic. In Formal Techniques for Networked and Distributed Systems - FORTE 2002 : 22nd IFIP WG 6.1 Intern. Conf. · Zbl 1037.68552
[7] Marco Devillers. Translating IOA automata to PVS. Technical Report CSI-R9903, Computing Science Institute, University of Nijmegen, February 1999; Marco Devillers. Translating IOA automata to PVS. Technical Report CSI-R9903, Computing Science Institute, University of Nijmegen, February 1999
[8] S.J. Garland and N.A. Lynch. The IOA Language and Toolset: Support for Designing, Analyzing, and Building Distributed Systems. Technical Report MIT/LCS/TR-762, MIT Laboratory for Computer Science, August 1998; S.J. Garland and N.A. Lynch. The IOA Language and Toolset: Support for Designing, Analyzing, and Building Distributed Systems. Technical Report MIT/LCS/TR-762, MIT Laboratory for Computer Science, August 1998
[9] Garland, Stephen, TIOA User Guide and Reference Manual (2006), Technical report, MIT CSAIL, Cambridge, MA, URL
[10] Stephen Garland, Nancy Lynch, Joshua Tauber, and Mandana Viziri. IOA User Guide and Reference Manual. Technical Report MIT-LCS-TR-961, MIT CSAIL, Cambridge, MA, 2004; Stephen Garland, Nancy Lynch, Joshua Tauber, and Mandana Viziri. IOA User Guide and Reference Manual. Technical Report MIT-LCS-TR-961, MIT CSAIL, Cambridge, MA, 2004
[11] Guttag, J. V.; Horning, J. J., Larch: Languages and Tools for Formal Specification (1993), Springer-Verlag · Zbl 0794.68103
[12] C. Heitmeyer and N. Lynch. The Generalized Railroad Crossing: A case study in formal verification of real-time systems. In Proc., Real-Time Systems Symp.; C. Heitmeyer and N. Lynch. The Generalized Railroad Crossing: A case study in formal verification of real-time systems. In Proc., Real-Time Systems Symp.
[13] Kaynar, D.; Lynch, N. A.; Segala, R.; Vaandrager, F., The Theory of Timed I/O automata, Synthesis Lectures on Computer Science (2005), Morgan Claypool Publishers
[14] Dilsun Kaynar, Nancy Lynch, and Sayan Mitra. Specifying and proving timing properties with TIOA tools. In Work-In-Progress Proc. 2004 IEEE Real-Time Systems Symp. (RTSS’04); Dilsun Kaynar, Nancy Lynch, and Sayan Mitra. Specifying and proving timing properties with TIOA tools. In Work-In-Progress Proc. 2004 IEEE Real-Time Systems Symp. (RTSS’04) · Zbl 1175.68259
[15] Manfred Kerber. How to prove higher order theorems in first order logic. Seki Report SR-90-19, Fachbereich Informatik, Universität Kaiserslautern, Germany, 1990; Manfred Kerber. How to prove higher order theorems in first order logic. Seki Report SR-90-19, Fachbereich Informatik, Universität Kaiserslautern, Germany, 1990 · Zbl 0746.68081
[16] Manfred Kerber and Axel Präcklein. Tactics for the improvement of problem formulation in resolution-based theorem proving. Seki Report SR-92-09, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany, 1992; Manfred Kerber and Axel Präcklein. Tactics for the improvement of problem formulation in resolution-based theorem proving. Seki Report SR-92-09, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany, 1992
[17] Larsen, Kim Guldstrand; Pettersson, Paul; Yi, Wang, UPPAAL in a nutshell, International Journal on Software Tools for Technology Transfer, 1, 1-2, 134-152 (1997) · Zbl 1060.68577
[18] Lim, Hongping, Translating timed I/O automata specifications for theorem proving in PVS (2006), Master’s thesis, Mass. Inst. of Tech., Cambridge, MA. URL · Zbl 1175.68259
[19] Lynch, N.; Tuttle, M., An introduction to Input/Output automata, CWI-Quarterly, 2, 3, 219-246 (Sept. 1989), Centrum voor Wiskunde en Informatica, Amsterdam, Netherlands
[20] Mavromattis, Panayiotis P., TIOA Simulator Manual (February 15, 2006), URL
[21] Mitra, Sayan; Archer, Myla, PVS strategies for proving abstraction properties of automata, Electronic Notes in Theor. Comp. Sci., 125, 2, 45-65 (2005) · Zbl 1272.68363
[22] Nipkow, Tobias; Slind, Konrad, I/O automata in Isabelle/HOL, (Dybjer, P.; Nordström, B.; Smith, J., Types for Proofs and Programs. Types for Proofs and Programs, LNCS, volume 996 (1995), Springer), 101-119
[23] Olaf Müller. A Verification Environment for I/O Automata Based on Formalized Meta-Theory; Olaf Müller. A Verification Environment for I/O Automata Based on Formalized Meta-Theory · Zbl 0914.68135
[24] Lawrence Paulson. The Isabelle reference manual. Technical Report 283, Univ. of Cambridge, 1993; Lawrence Paulson. The Isabelle reference manual. Technical Report 283, Univ. of Cambridge, 1993
[25] Deepak Ramachandran and Eyal Amir. Compact propositional encodings of first-order theories. In Proc. 20th Natl. Conf. on Artif. Intel. and 17th Innovative Appl. of Artif. Intel. Conf., July 9-13, 2005, Pittsburgh, PA; Deepak Ramachandran and Eyal Amir. Compact propositional encodings of first-order theories. In Proc. 20th Natl. Conf. on Artif. Intel. and 17th Innovative Appl. of Artif. Intel. Conf., July 9-13, 2005, Pittsburgh, PA
[26] Romijn, J., Tackling the RPC-Memory Specification Problem with I/O automata, (Broy, M.; Merz, S.; Spies, K., Formal Systems Specification — The RPC-Memory Specification Case. Formal Systems Specification — The RPC-Memory Specification Case, Lect. Notes in Comp. Sci., volume 1169 (1996), Springer-Verlag), 437-476
[27] N. Shankar, S. Owre, J.M. Rushby, and D.W.J. Stringer-Calvert. PVS Prover Guide, Version 2.4. Technical report, Comp. Sci. Lab., SRI Intl., Menlo Park, CA, Nov. 2001; N. Shankar, S. Owre, J.M. Rushby, and D.W.J. Stringer-Calvert. PVS Prover Guide, Version 2.4. Technical report, Comp. Sci. Lab., SRI Intl., Menlo Park, CA, Nov. 2001
[28] Toh Ne Win. Theorem-proving distributed algorithms with dynamic analysis. Master’s thesis, Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, May 2003; Toh Ne Win. Theorem-proving distributed algorithms with dynamic analysis. Master’s thesis, Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, May 2003
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.