Modere: the model-checking engine of Rebeca

ABSTRACT

Rebeca is an actor-based language with formal semantics that can be used in modeling concurrent and distributed software and protocols. Automatic verification of these systems in the design stage helps develop error free systems. In this paper, we describe the model checking tool developed for verification of Rebeca models. This tool uses partial order reduction technique for reducing the size of the state space generated for a given model. Using this tool for model checking Rebeca yields much better results than the previous attempts for model checking Rebeca.

REFERENCES

• 1: Gul Agha, The Structure and Semantics of Actor Languages, Proceedings of the REX School/Workshop on Foundations of Object-Oriented Languages, p.1-59, May 28-June 01, 1990
• 2: D. Bosnacki. Enhancing State Space Reduction Techniques for Model Checking. PhD thesis, Technische Universiteite Eindhoven, 2001.
• 3: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 4: E. Allen Emerson , A. Prasad Sistla, Symmetry and model checking, Formal Methods in System Design, v.9 n.1-2, p.105-131, Aug. 1996 [doi>10.1007/BF00625970]
• 5: E. Allen Emerson , Somesh Jha , Doron Peled, Combining Partial Order and Symmetry Reductions, Proceedings of the Third International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.19-34, April 02-04, 1997
• 6: P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An approach to the State-Explosion Problem, PhD thesis, 1995.
• 7: C. Hewitt. Procedural embedding of knowledge in planner. In Proc. 2nd International Joint Conference on Artificial Intelligence, pages 167--184, 1971.
• 8: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 9: Gerard J. Holzmann , Doron Peled, An improvement in formal verification, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, p.197-211, January 1995
• 10: G. J. Holzmann, D. Peled, and M. Yannakakis. On nested depth first search. In Proc. Second SPIN Workshop, pages 23--32, 1996.
• 11: T. Hune, J. Romijn, M. Stoelinga, and F. W. Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming (JLAP), 52-53:183--220, 2002.
• 12: C. Norris Ip , David L. Dill, Better verification through symmetry, Formal Methods in System Design, v.9 n.1-2, p.41-75, Aug. 1996 [doi>10.1007/BF00625968]
• 13: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 14: NuSMV user manual. http://nusmv.irst.itc.it/NuSMV/userman/index-v2.html.
• 15: Rebeca homepage. http://khorshid.ut.ac.ir/~rebeca/.
• 16: M. Sirjani, A. Movaghar, A. Shali, and F. S. de Boer. Modeling and verification of reactive systems using Rebeca. Fundamamenta Informaticae, 63(4):385--410, 2004.
• 17: A Front-End Tool for Automated Abstraction and Modular Verification of Actor-Based Models, Proceedings of the Fourth International Conference on Application of Concurrency to System Design, p.145, June 16-18, 2004
• 18: M. Y. Vardi and P. Wolper. An automata theoretic approach to automatic program verification. In D. Kozen, editor, LICS, pages 322--331, 1986.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Verification

Keywords:
actor model, automated verification tool, partial order reduction, rebeca