Towards Integrated Verification of Timed Transition Models

• Autorzy: Lawford M. , Pantelic V. , Zhang H.
• Języki publikacji: EN

Abstrakty

EN

This paper describes an attempt to combine theorem proving and model-checking to formally verify real-time systems in a discrete time setting. The Timed Automata Modeling Environment (TAME) has been modified to provide a formal model for Time Transition Models (TTMs) in the PVS proof checker. Strong and weak state-event observation equivalences are formalized in PVS for state-event labeled transition systems (SELTS), the underlying semantic model of TTMs. The state-event equivalences form the basis of truth value preserving abstractions for a real-time temporal logic. When appropriate restrictions are placed upon the TTMs, their PVS models can be easily translated into input for the SAL model-checker. A simple real-time control system is specified and verified using these theories. While these preliminary results indicate that the combination of PVS and SAL could provide a useful environment to perform equivalence verification, model-checking and compositional model reduction of real-time systems, the current implementation in the general purpose SAL model-checker lags well behind state of the art real-time model-checkers.

Słowa kluczowe

EN

real time; equivalence verification; theorem proving; PVS; model checking; model reduction; SAL

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 70, nr 1,2
• Strony: 75--110
• Opis fizyczny: tab., bibliogr. 32 poz.

Twórcy

autor

Lawford M.

autor

Pantelic V.

autor

Zhang H.

• Software Quality Research Lab., Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada L8S 4K1,

Bibliografia

• [1] Alur, R., Henzinger, T. A., Mang, F. Y. C., Qadeer, S., Rajamani, S. K., Tasiran, S.: MOCHA: Modularity in Model Checking, Computer Aided Verification, 1427, 1998.
• [2] Archer, M.: TAME: Using PVS Strategies for Special-Purpose Theorem Proving, Annals of Mathematics and Artificial Intelligence, 29(1-4), 2000, 201-232.
• [3] Archer, M., Heitmeyer, C., Riccobene, E.: Proving Invariants of I/O Automata with TAME, Automated Software Engg., 9(3), 2002, 201-232, ISSN 0928-8910.
• [4] Arnold, A.: Finite Transition Systems, Prentice Hall, 1994.
• [5] Behrmann, G., David, A., Larsen, K. G.: A Tutorial on UPPAAL, Formal Methods for the Design of Real-Time Systems: 4th International School on FormalMethods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004 (M. Bernardo, F. Corradini, Eds.), number 3185 in LNCS, Springer-Verlag, September 2004.
• [6] Filliâtre, J.-C., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated Canonizer and Solver., CAV (G. Berry, H. Comon, A. Finkel, Eds.), 2102, Springer, 2001, ISBN 3-540-42345-1.
• [7] Formal Methods Program: Formal Methods Roadmap: PVS, ICS, and SAL, Technical Report SRI-CSL-03-05, Computer Science Laboratory, SRI International,Menlo Park, CA, October 2003.
• [8] Graf, S., Loiseaux, C.: Property Preserving Abstraction under Parallel Composition, in: TAPSOFT'93 (M.-C. Gaudel, J.-P. Jouannaud, Eds.), number 668 in LNCS, Springer-Verlag, 1993, 644-657.
• [9] Heitmeyer, C., Archer, M.: Mechanical Verification of Timed Automata: A Case Study, Technical Report 5546-98-8180, Naval Research Laboratory, April 1998.
• [10] Heitmeyer, C., Kirby, J., Labaw, B., Bharadwaj, R.: SCR*: A Toolset for Specifying and Analyzing Software Requirements, Proc. 10th Int. Conf. Computer Aided Verification (CAV'98), Vancouver, BC, Canada, June-July 1998, 1427, Springer, 1998, ISSN 0302-9743.
• [11] Larsen, K. G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell, International Journal on Software Tools for Technology Transfer, 1(1-2), 1997, 134-152.
• [12] Lawford, M.: Transformational Equivalence of Timed Transition Models, Master Thesis, Dept. of Electrical Eng., Univ. of Toronto, Canada, January 1992.
• [13] Lawford, M.: Model Reduction of Discrete Real-Time Systems, Ph.D. Thesis, Dept. of Elec. & Comp. Eng., Univ. of Toronto, Canada, January 1997.
• [14] Lawford, M., Ostroff, J., Wonham, W.: Model reduction of modules for state-event temporal logics, in: Formal Description Techniques IX: Theory, application and tools, Proceedings of FORTE/PSTV'96 (R. Gotzhein, J. Bredereke, Eds.), Chapman & Hall, 1996, 263-278.
• [15] Lawford, M., Wonham, W.: Equivalence Preserving Transformations of Timed Transition Models, IEEE Transactions Automatic Control, 40, July 1995, 1167-1179.
• [16] Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification, Proc. of 12th ACM Symposium on Principles of Programming Languages, New Orleans, January 1985.
• [17] Lynch, N., Tuttle, M.: An Introduction to Input/Output automata, CWI-Quarterly, 2(3), September 1989, 219-246.
• [18] Lynch, N., Vaandrager, F.: Forward and backward simulations II.: timing-based systems, Inf. Comput., 128(1), 1996, 1-25, ISSN 0890-5401.
• [19] Manna, Z., Bjorner, N., Browne, A., Chang, E. Y., Colon, M., de Alfaro, L., Devarajan, H., Kapur, A., Lee, J., Sipma, H., Uribe, T. E.: STeP: The Stanford Temporal Prover, TAPSOFT, 1995.
• [20] Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag,New York, 1992.
• [21] Milner, R.: Communication and Concurrency, Prentice Hall, New York, 1989.
• [22] de Moura, L., Owre, S., Ruess, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2, Computer Aided Verification: 16th International Conference, CAV 2004 (R. Alur, D. A. Peled, Eds.), 3114, Springer-Verlag Heidelberg, Boston, MA, USA, July 2004.
• [23] Ostroff, J.: Temporal Logic for Real-Time Systems, RSP, Research Studies Press /Wiley, 1989, Taunton, UK.
• [24] Ostroff, J.: Deciding properties of timed transition models, IEEE Transactions Parallel and Distributed Systems, 1(2), April 1990, 170-183.
• [25] Ostroff, J.: A visual toolset for the design of real-time discrete-event systems, IEEE Transactions on Control Systems Technology, 5(3), 1997, 320-337.
• [26] Ostroff, J., Wonham, W.: A Framework for Real-Time Discrete Event Control, IEEE Transactions on Automatic Control, 35(4), April 1990, 386-397.
• [27] Ostroff, J. S.: Composition and refinement of discrete real-time systems, ACM Transactions on Software Engineering and Methodology, 8(1), 1999, 1-48.
• [28] Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering, 21(2), February 1995, 107-125.
• [29] Park, D.: Concurrency and automata on infinte sequences, 5th GI Conference on Theoretical Computer Science, 104, Springer-Verlag, 1981.
• [30] Sistla, A., Clarke, E.: The complexity of propositional linear temporal logic, J. ACM, 32, 1985, 733-749.
• [31] Wang, F.: Formal Verification of Timed Systems: A Survey and Perspective, Proceedings of the IEEE, 92(8), August 2004, 1283-1305.
• [32] Zhang, H.: Formal Verification of Timed Transition Models, Technical Report 17, Software Quality Research Lab, McMaster University, Hamilton, ON, Canada 2003.