Modeling and Verification of Reactive Systems using Rebeca

• Autorzy: Sirjani M. , Movaghar A. , Shali A. , de Boer F. S.
• Języki publikacji: EN

Abstrakty

EN

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their correctness. In this paper, we develop an actor-based model for describing such systems, use temporal logic to specify properties of the model, and apply different abstraction and verification methods for verifying that the model meets its specification. We use a compositional verification approach for verifying safety properties of these models. For that we introduce a notion of component, based on an user-defined decomposition of the model. Components are more abstract than the model itself, and so we can reduce the state space of the model which makes it more amenable to model checking techniques. We prove that our abstraction technique preserves a set of behavioral specifications in temporal logic. The soundness of the abstraction is proved by the weak simulation relation between the constructs.

Słowa kluczowe

EN

actor model; reactive system; model checking; compositional verification; property preserving abstraction

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 63, nr 4
• Strony: 385--410
• Opis fizyczny: Bibliogr. 48 poz.

Twórcy

autor

Sirjani M.

• Department of Computer Engineering, Sharif University of Technology, Azadi Ave., Teheran, Iran

autor

Movaghar A.

• Department of Computer Engineering, Sharif University of Technology, Azadi Ave., Teheran, Iran

autor

Shali A.

• Department of Electrical and Computer Engineering, University of Tehran, Karegar Ave., Tehran, Iran

autor

de Boer F. S.

• Department of Software Engineering, Centrum voor Wiskunde en Informatica, Kruislaan 413, 1098 SJ, Amsterdam, The Netherlands

Bibliografia

• [1] NuSMV User Manual, Availabe through http://nusmv.irst.itc.it/NuSMV/ userman/index-v2.html.
• [2] Spin User Manual, Available through http://netlib.bell-labs.com/netlib/spin/whatisspin.html.
• [3] Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems, MIT Press, Cambridge, MA, USA, 1990.
• [4] Agha, G.: The Structure and Semantics of Actor Languages, in: Foundations of Object-Oriented Languages (J. W. de Bakker,W.-P. de Roever, G. Rozenberg, Eds.), Springer-Verlag, Berlin, Germany, 1990, 1-59.
• [5] Agha, G., Mason, I., Smith, S., Talcott, C.: A Foundation for Actor Computation, Journal of Functional Programming, 7, 1997, 1-72.
• [6] Alur, R., de Alfaro, L., Henzinger, T. A., Mang, F. Y. C.: Automating Modular Verification, Proceedings of CONCUR: 10th International Conference on Concurrency Theory, LNCS 1664, Springer-Verlag, Berlin, 1999, 82-97.
• [7] Alur, R., Henzinger, T. A.: Computer Aided Verification, Technical Report Draft, 1999.
• [8] Alur, R., Henzinger, T. A.: Reactive Modules, Formal Methods in System Design: An International Journal, 15(1), July 1999, 7-48.
• [9] Alur, R., Henzinger, T. A., Mang, F. Y. C., Qadeer, S.: MOCHA:Modularity inModel Checking, Proceedings of CAV’98, LNCS 1427, Springer-Verlag, Berlin, 1998, 521-525.
• [10] America, P., de Bakker, J., Kok, J.N., Rutten, J.J.J.M.: Denotational Semantics of a Parallel Object-Oriented Language, Information and Computation , 83(2), 1989, 152-205.
• [11] Clarke, E. M., Grumberg, O., Peled, D. A.: Model Checking, The MIT Press, Cambridge, Massachusetts, 1999.
• [12] Clarke, E. M., Long, D. E., McMillan, K. L.: Compositional Model Checking, Proceedings of Fourth Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, Asilomar Conference Center, Pacific Grove, California, 5-8 June 1989, 353-362.
• [13] Damm,W., Josko, B., Pnueli, A., Votintseva, A.: Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML, Proceedings of Formal Methods for Components and Objects, LNCS 2852, Springer-Verlag, Berlin, Leiden, The Netherlands, 2003, 71-98.
• [14] de Boer, F.S.: A Proof System for the Language POOL, Proceedings of the REX School/Workshop Foundations on Object-Oriented Languages, LNCS 489, Springer-Verlag, Berlin, 1991, 124-150.
• [15] Dwyer, M., Hatcliff, J., Joehanes, R., Laubach, S., Pasareanu, C., Robby, Visser, W., Zheng, H.: Tool-Supported Program Abstraction for Finite-State Verification, Proceedings of the 23nd International Conference on Software Engineering, 2001, 177-187.
• [16] E.A. Emerson: Temporal and Modal Logic, Handbook of Theoretical Computer Science (J. van Leeuwen, Ed.), B, Elsevier Science Publishers, Amsterdam, 1990, 996-1072.
• [17] Gaspari,M., Zavattaro, G.: An Actor Algebra for Specifying Distributed Systems: The Hurried Philosophers Case Study, Proceedings of Concurrent Object-Oriented Programming and Petri Nets, Advances in Petri Nets, LNCS 2001, 2001, 428-444, ISSN 0302-9743.
• [18] Havelund, K., Pressburger, T.: Model Checking Java Programs using Java PathFinder, International Journal on Software Tools for Technology Transfer, 2(4), 2000, 366-381.
• [19] Hewitt, C.: Description and Theoretical Analysis (Using Schemata) of PLANNER: A Language for Proving Theorems and Manipulating Models in a Robot, MIT Artificial Intelligence Technical Report 258, Department of Computer Science, MIT, April 1972.
• [20] Hoare, C. A. R.: Communicating Sequential Processes, Prentice-Hall, Englewood Cliffs (NJ), USA, 1985.
• [21] Ioustinova, N., Sidorova, N., Steffen, M.: Closing Open SDL-Systems for Model Checking with DTSpin, Proceedings of FME’2002, LNCS 2391, Springer-Verlag, Berlin, Germany, 2002, 531-548, ISSN 0302-9743.
• [22] Kesten, Y., Pnueli, A.: Modularization and Abstraction: The Keys to Practical Formal Verification, Proceedings of 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS’98), LNCS 1450, Springer-Verlag, Berlin, Germany, 1998, 54-71, ISSN 0302-9743.
• [23] Kupferman, O., Vardi, M. Y., Wolper, P.: Module Checking, Information and Computation, 164(2), 2001, 322-344.
• [24] Lamport, L.: Composition: A Way to Make Proofs Harder, Proceedings of COMPOS: International Symposium on Compositionality: The Significant Difference, LNCS 1536, Springer-Verlag, Berlin, Germany, 1997, 402-407.
• [25] Larsen, K. G., Milner, R.: A Compositional Protocol Verification Using Relativized Bisimulation, Information and Computation, 99(1), July 1992, 80-108.
• [26] Lynch, N.: Distributed Algorithms, Morgan Kaufmann, San Francisco, CS, 1996, ISBN SBN 1-55860-348-4.
• [27] Lynch, N. A., Tuttle, M. R.: Hierarchical correctness proofs for distributed algorithms, Technical Report MIT/LCS/TR-387, MIT, 1987.
• [28] Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, Berlin, Germany, 1992.
• [29] Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems (Safety), Springer-Verlag, Berlin, Germany, 1995.
• [30] Mason, I. A., Talcott, C. L.: Actor languages: Their syntax, semantics, translation, and equivalence, Theoretical Computer Science, 220(2), June 1999, 409-467, ISSN 0304-3975.
• [31] McMillan, K.: Verification of Digital and Hybrid Systems, Springer-Verlag, Berlin, Germany, 2000.
• [32] McMillan, K. L.: A methodology for hardware verification using compositional model checking, Science of Computer Programming, 37(1-3),May 2000, 279-309, ISSN 0167-6423.
• [33] Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Information and Computation, 100(1), September 1992, 1-77.
• [34] Ren, S., Agha, G.: RTsynchronizer: language support for real-time specifications in distributed systems, ACM SIGPLAN Notices, 30(11), November 1995, 50-59, ISSN 0362-1340.
• [35] de Roever, W. P., Langmaack, h., Pnueli, A., Eds.: Compositionality: The Significant Difference, International Symposium, COMPOS’97, Bad Malente, Germany, September 1997, Revised Lectures, LNCS 1536, Springer-Verlag, Berlin, 1998.
• [36] Roscoe, W. A.: Theory and Practice of Concurrency, Prentice-Hall, 1998.
• [37] Schacht, S.: Formal Reasoning about Actor Programs Using Temporal Logic, Proceedings of Concurrent Object-Oriented Programming and Petri Nets, LNCS 2001, Springer-Verlag, Berlin, 2001, 445-460.
• [38] Sidorova, N., Steffen, M.: Embedding Chaos, Proceedings of Static Analysis Symposium (SAS’01) , LNCS 2126, 2001, 319-334, ISSN 0302-9743.
• [39] Sirjani, M., Movaghar, A.: An Actor-Based Model for Formal Modelling of Reactive Systems: Rebeca, Technical Report CS-TR-80-01, Tehran, Iran, 2001.
• [40] Sirjani, M., Movaghar, A., Iravanchi, H., Jaghoori, M., Shali, A.: Model Checking Rebeca by SMV, Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS’03), Southampton, UK, April 2003, 233-236.
• [41] Sirjani, M., Movaghar, A., Mousavi, M.: Compositional Verification of an Object-Based Reactive System, Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS’01), Oxford, UK, April 2001, 114-118.
• [42] Sirjani, M., Shali, A., Jaghoori, M., Iravanchi, H., Movaghar, A.: A Front-End Tool for Automated Abstraction and Modular Verification of Actor-Based Models, Proceedings of ACSD 2004, IEEE Computer Society, 2004, 145-148.
• [43] Stahl, K., Baukus, K., Lakhnech, Y., Steffen, M.: Divide, abstract and model-check, Proceedings of the 5th International SPIN Workshop on Theoretical Aspects of Model Checking, LNCS 1680, Springer-Verlag, Berlin, 1999.
• [44] Talcott, C.: Composable Semantic Models for Actor Theories, Higher-Order and Symbolic Computation, 11(3), December 1998, 281-343, ISSN 1388-3690.
• [45] Talcott, C.: Actor theories in rewriting logic, Theoretical Computer Science, 285(2), August 2002, 441-485, ISSN 0304-3975.
• [46] Tsay, Y.: Compositional Verification in Linear-Time Temporal Logic, Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS’00), LNCS 1784, 2000, 344-358, ISSN 0302-9743.
• [47] Varela, C., Agha, G.: Programming Dynamically Reconfigurable Open Systems with SALSA, ACM SIGPLAN Notices, 36(12), 2001, 20-34.
• [48] Yonezawa, A.: ABCL: An Object-Oriented Concurrent System, Series in Computer Systems, MIT Press, 1990.