A Logic Framework for Verification of Timed Algorithms

• Autorzy: Slissenko A.
• Języki publikacji: EN

Abstrakty

EN

This paper is a survey of research of my colleagues and myself aimed at developing a comprehensive logical framework for the verification of real-time distributed systems. The framework is based on predicate logics with explicit time. To choose such a logic we pursue two goals: first, to make formalization of verification problems rather direct, without unjustified simplifications, and second, to have a logic which permits to describe decidable classes of the verifications problem covering the particular problems we are interested in. Notice that our intention is not to introduce new specification languages, but work directly with those of the user. In this paper we describe First Order Timed Logic (FOTL) that is sufficient to express the main part of verification of systems without uncertainty. The time is continuous (the formalism work as well for discrete time - in our context this case is less interesting and less efficient from algorithmic viewpoint). We give examples of problems that can be treated, describe how to represent runs of programs in FOTL, introduce decidable classes, discuss aspects of practical efficiency. We conclude with open questions.

Słowa kluczowe

EN

First Order Timed Logic; FOTL; verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 62, nr 1
• Strony: 29--67
• Opis fizyczny: Bibliogr. 58 poz., rys.

Twórcy

autor

Slissenko A.

• Laboratory for Algorithmics, Complexity and Logic University Paris 12. France,

Bibliografia

• [AD94] R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994.
• [AH98] M. Archer and C. Heitmeyer. Mechanical verification of timed automata: A case study. Technical Report 5546-98-8180. University Paris-12, Department of Informatics, Naval Reserach Laboratory, Washitigton, 1998. NRL Memorandum Report.
• [BB84] C. Bennett and G. Brassard. Quantum cryptography: public key distribution and coin tossing. In Proc. of IEEE Intern. Cont, on Computers. Systems and Signal processing. Bangalore, India. Dec. 79S4. pages 175-179. IEEE. 1984.
• [BBB+00] E. Biham, M. Boyer, P. Boykin. T. Mor. and V. Roychowdhury. A proof of the security of quantum key distribution. In Proc. of the ACM Annu. Symp. on Theor. Comput. Sci. (STOC'2000), pages 715-724,2000.
• [BBC+00] N. Bjømer, A. Browne, M. Colon, B. Finkbeiner, Z. Manna. H. Sipma. and T. Uribe. Verifying temporal properties of reactive systems: A STeP tutorial. Formal Methods in System Design, 2000. To appear.
• [BBF+01] B. Berard, M. Bidoit. A. Finkel, F Laroussinie, A. Petit, L. Petrucci, and P. Schnoebelen. Systems and Software Verification Model-Checking Techniques and Tools. Springer-Verlag. 2001.
• [BCP04] D. Beauquier, T. Crolard, and E. Prokofieva. Automatic parametric verification of a root contention protocol based on abstract state machines and first order timed logic. In I. Walukiewicz, editor, Proc. of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS2004). Led. Notes in Comput. Sci. vol. 2988, pages 372-387. Springer-Verlag, 2004.
• [BCS00] D. Beauquier, T. Crolard, and A. Slissenko. A predicate logic framework for mechanical verification of real-time Gurevich Abstract State Machines: A case study with PVS. Technical Report 00-25, University Paris 12. Department of Informatics, 2000. Available at http://www.univ-parisl2.fr/lacl/.
• [BG] A. Blass and Y. Gurevich. Abstract state machines capture parallel algorithms. To appear in ACM Transactions on Computational Logic.
• [BGR95] E. Börger. Y. Gurevich, and D. Rozenzweig. The bakery algorithm: Yet another specification and verification. In E. Borger, editor. Specification and Validation Methods, pages 231-243. Oxford University Press, 1995.
• [BMSU98] N. Bjørner, Z. Manna, H. Sipma, and T. Uribe. Deductive verification of real-time systems using STeP. Technical Report Technical Report STAN-CS-TR-98-1616, Computer Sci. Dept. Stanford Univ., December 1998. Submited to Elsevier Science.
• [BRS02] D. Beauquier, A. Rabinovich, and A. Slissenko. A logic of probability with decidable model-checking. In J. Bradfield. editor, Proc. of the 16th Int. Worksshop. on Comput. Sci. Logic (CSL'O2) and11lth Annual Conference of the EACSL, September 22-25, 2002, Edinburgh. UK. Lect. Notes in Comput. Sci., vol. 2471. pages 306-321. Springer-Verlag. 2002.
• [BS97] D. Beauquier and A. Slissenko. The railroad crossing problem: Towards semantics of timed algorithms and their model-checking in high-level languages. In M. Bidoit and M. Dauchel, editors, TAPSOFT'97: Theory and Practice of Software Development, pages 201-212. Springer Verlag, 1997. Lect. Notes in Comput. Sci., vol. 1214.
• [BS99] D. Beauquier and A. Slissenko. Decidable classes of the verification problem in a timed predicate logic. In Proc. of the I2th Intern. Symp. on Fundamentals of Computation Theory (FCT'99), Iasi, Rumania. August 30-September 3, 1999, Lect. Notes in Comput. Sci, vol. 1684, pages 100-111. Springer-Verlag, 1999.
• [BS02a] D. Beauquier and A. Slissenko. Decidable verification for reducible timed automata specified in a first order logic with time. Theoretical Computer Science, 275(l-2):347-388, March 2002.
• [BS02b] D. Beauquier and A. Slissenko. A first order logic for specification of timed algorithms: Basic properties and a decidable class. Annals of Pure and Applied Logic. 113(1-3): 13-52, 2002.
• [BS03] E. Borger and R. Stark. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag, 2003.
• [BS04] D. Beauquier and A. Slissenko. Periodicity based decidable classes in a first order timed logic. Technical Report 2004-04, University Paris 12, Department of Informatics, 2004. Available at http://www.unjv-parisl2.fr/lacl/.
• [CDE+99] M. Clavel, F. Durán. S. Eker, P Lincoln, N. Marti-Oliet, J. Meseguer, and J. F. Quesada. The Maude system. In P. Narendran and M. Rusinowitch. editors, Proceedings of the l0th International Conference on Rewriting Techniques and Applications (RTA'99), pages 240-243, Trento, Italy, July 1999. Springer-Verlag LNCS 1631. System Description.
• [CGP99] E. Clarke, O. Grumberg, and D. Peleg. Model Checking. MIT Press, Boston, MA., 1999.
• [CMCP+99] E. Ciapessoni, P. Mirandola, A. Coen-Porisini, D. Mandrioli, and A. Morzenti. From formal models to formally based methods: An industrial experience. ACM Transactions on Software Engineering and Methodology, 8(1):79-113, January 1999.
• [CS00] J. Cohen and A. Slissenko. On verification of refinements of timed distributed algorithms. In Y. Gurevich, P. Kutter. M. Odersky, and L. Thiele, editors, Proc. of the Intern. Workshop on Abstract State Machines (ASM'2000). March 20-24, 2000. Switzerland, Monte Verita. Ticino. Lect. Notes in Comput. Sci., vol. 1912, pages 34^9. Springer-Verlag, 2000.
• [CS03] J. Cohen and A. Slissenko. On implementations of distributed real-time abstract state machines. In Proc. of the 4th Intern. Conf. on Computer Science and Information Technology (CSIT'2003), September 22-26, 2003, Yerevan, Armenia. Organized by National Academy of Science of Armenia in cooperation with Test Technology Technical Council of IEEE Computer Society, pages 13-18. National Academy of Science of Armenia. 2003. (Plenary talk.).
• [ES03] T. Essafi and A. Slissenko. A heuristic algorithm for proving the security property of some protocols. In Proc. of the 4th Intern. Conf. on Computer Science and Information Technology (CSIT'2003), September 22-26. 2003. Yerevan. Armenia. Organized by National Academy of Science of Armenia in cooperation with Test Technology Technical Council of IEEE Computer Society, pages 58-62. National Academy of Science of Armenia, 2003.
• [FH94] R. Fagin and J. Halpern. Reasoning about knowledge and probability. J. of the Assoc. Comput. Mach. 41(2):340-367, 1994.
• [FHM90] R. Fagin, J. Halpern, and N. Megiddo. A logic for reasoning about probabilities. Information and Computation, 87(1-2):78-128. 1990.
• [FV59] S. Feferman and R. Vaught. The first order properties of algebraic systems. Fundamenta Mathematica, 47:57-103, 1959.
• [GH96] Y. Gurevich and J. Huggins. The railroad crossing problem: an experiment with instantaneous actions and immediate reactions. In H. K. Buening, editor. Computer Science Logics, Selected papers from CSL'95. pages 266-290. Springer-Verlag, 1996. Lect. Notes in Comput. Sci., vol. 1092.
• [GPT96] F. Giunchiglia, R Pecchiari, and C. Talcott. Reasoning theories - towards an architecture for open mechanized reasoning systems. In F. Baader and K. U. Schulz, editors, Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich (Germany), Applied Logic, pages 157-174. Kluwer Academic Publishers, March 1996.
• [Gur95] Y. Gurevich. Evolving algebra 1993: Lipari guide. In E. Borger, editor. Specification and Validation Methods, pages 9-93. Oxford University Press, 1995.
• [Gur00] Y. Gurevich. Sequential abstract-state machines capture sequential algorithms. ACM Transactions on Computational Logic, 1(1):77-l 11, July 2000.
• [Hal91] J. Halpern. Presburger arithmetic with unary predicates is TTJ-complete. J. of symbolic Logic, 56:637-642,1991.
• [HL94] C. Heitmeyer and N. Lynch. The generalized railroad crossing: a case study in formal verification of real-time systems. In Proc. of Real-Time Systems Symp. San Juan. Puerto Rico. IEEE, 1994.
• [HL96] C. Heitmeyer and N. Lynch. Formal verification of real-time systems using timed automata. In C. Heitmeyer and D. Mandrioli, editors. Formal Methods for Real-Time Computing, pages 83-106. John Wiley & Sons, 1996. In series: "Trends in Software", vol. 5, Series Editor: B. Krishnamurthy.
• [HM96] C. Heitmeyer and D. Mandrioli. editors. Formal Methods for Real Time Computing, volume 5 of Trends in Software. John Wiley & Sons, 1996. Series Editor: B. Krishnamurthy.
• [HR] Y. Hirshfeld and A. Rabinovich. Logic for real time: Decidability and complexity. This journal.
• [J. 96] J. Harrison. HOL light: A tutorial introduction. In M. Srivas and A. Camilleri, editors. First international conference on formal methods in computer-aided design, volume 1166 of Lecture Notes in Computer Science, pages 265-269, Palo Alto, CA, USA, November 1996. Springer Verlag.
• [Lam74] L. Lamport. A new solution of Dijkstra's concurrent programming problem. Communications of ACM, 17(8):453-455, 1974.
• [Mak04] J. Makowsky. Algorithmic uses of the Feferman-Vaughttheorem. Annals of Pure and Applied Logic, I26(1-3):159-213,2004.
• [MMP+96] D. Mandrioli, A. Morzenti, M. Pezze. R San Pietro, and S. Silva. A Petri net and logic approach to the specification and verification of real-time systems. In C. Heitmeyer and D. Mandrioli, editors. Formal Methods for Real-Time Computing, pages 135-165. John Wiley & Sons, 1996. In series: "Trends in Software", vol. 5. Series Editor: B. Krishnaniurtby.
• [MS85] N. Mahany and F. Schneider. Inexact agreement: accuracy, precision, and gracefull degradation. In Proc. of the 4nd Symp. on Principles of Distributed Computing, pages 231-249, 1985.
• [NC00] G. Naumovich and L. Clarke. Classifying properties: An alternative to the safety-liveness classificadon. In David S. Rosenblum, editor. Proceedings of the ACM SIGSOFT 8th International Symposium on the Foundations of Software Engineering (FSE-00), volume 25, 6 of ACM Software Engineering Notes, pages 159-168, NY. November 8-10 2000. ACM Press.
• [ORNvH95] S. Owre. J. Rushby, Shankar N., and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans, on Software Engineering, 21(2):107-125, 1995.
• [Pau94] L. C. Paulson. Isabelle: A generic theorem proven Lecture Notes in Computer Science, 828:xvii + 321, 1994.
• [PVS] PVS. WWW site of PVS papers, http://www.csl.sri.com/sri-csl-fm.html.
• [Rab] A. Rabinovich. Composition theorems for generalized sums. To be published.
• [SC94] J. Sanders and E. Curran. Software Quality. Addison-Wesley, 1994.
• [Sch87] F. Schneider. Understanding protocols for byzantine clock synchronization. Technical Report 87-859, Comput. Sci. Dept., Cornell University, Ithaca, NY, Ithaca, NY, August 1987.
• [Sch96] B. Schneier. Applied Cryptography. John Wiley & Sons, 2nd edition edition. 1996.
• [Sha92] N. Shankar. Mechanical verification of a generalized protocol and byzantine fault tolerant clock synchronization. In Proc. of the 2nd Intern. Symp. on Formal Technique in Real-Time and Fault-Tolerant Systems. Nijmegen, The Netherlands, 1992. Lect. Notes in Comput. Sci., vol. 571, pages 217-236. Springer-Verlag, 1992.
• [Sha93] N. Shankar. Verification of real-time systems using PVS. In Proc. 5th International Computer Aided Verification Conference, pages 280-291, 1993.
• [Sli03a] A. Slissenko. Complexity problems in the analysis of information systems security. In V. Gorodetsky, L. Popyack. and V. Skormin, editors, Proc. of the 2nd Intern. Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security (MMM-ACNS-2003), St. Petersburg, Russia, September 21-23. 2003. Lect. Notes in Comput. Sci. vol. 2776, pages 48-57. Springer-Verlag, 2003. (Invited talk.).
• [Sli03b] A. Slissenko. A logic framework for verification of timed distributed algorithms, version of April 2001. Technical Report 2003-04, University Paris 12. Department of Informatics, 2003. Available at http://www.univ-parisl2.fr/lacl/.
• [Som92] I. Sommerville. Software Engineering. Addison-Wesley, 4th edition. 1992.
• [SSB0l] R. Stark. J. Schid, and E. Borger, editors. Java and the Java Virtual Machine. Definition. Verification, Validation. Springer Verlag. 2001.
• [Tel94] G. Tel. editor. Introduction to Distributed Algorithms. Cambridge University Press, 1994.
• [Tho97] W. Thomas. Languages, automata and logic. In A. Salomaa and G. Rozenberg. editors. Handbook of Formal Languages, volume 3. Beyond Words, pages 389-455. Springer-Verlag, Berlin, 1997.
• [Tra] B. Trakhtenhrot. Understanding basic automata theory in the continuous time setting. This journal. [Wei99] V. Weispfenning. Mixed real-integer linear quantifier elimination. In Proc. of the 1999 Int. Symp. On Symbolic and Algebraic Computations flSSAC'99), pages 129-136. ACM Press. 1999.