Model checking object petri nets in prolog

ABSTRACT

Object Petri nets (OPNs) provide a natural and modular method for modelling many real-world systems. We give a structure-pre-serving translation of OPNs to Prolog by encoding the OPN semantics, avoiding the need for an unfolding to a flat Petri net. The translation provides support for reference and value semantics, and even allows different objects to be treated as copyable or non-copyable. The method is developed for OPNs with arbitrary nesting. We then apply logic programming tools to animate, compile and model check OPNs. In particular, we use the partial evaluation system logen to produce an OPN compiler, and we use the model checker xtl to verify CTL formulae. We also use logen to produce special purpose model checkers. We present two case studies, along with experimental results. A comparison of OPN translations to Maude specifications and model checking is given, showing that our approach is roughly twice as fast for larger systems. We also tackle infinite state model checking using the ecce system.

REFERENCES

• 1: M. Butler. csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing, 12:182--198, 2000.
• 2: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 3: Berndt Farwer, Comparing concepts of object Petri net formalisms, Fundamenta Informaticae, v.47 n.3-4, p.247-258, August 2001
• 4: B. Farwer and M. Leuschel. Model checking object Petri nets in Prolog. Technical Report DSSE-TR-2003-4, Declarative Systems and Software Engineering Group, School of Electronics and Computer Science, University of Southampton, SO17 1BJ, UK, 2003.
• 5: B. Farwer and M. Leuschel. Model checking object Petri nets in Maude and Prolog. Technical Report FBI-HH-B-258/04, Fachbereich Informatik, Universität Hamburg, Germany, 2004.
• 6: Berndt Farwer , Kundan Misra, Modelling with hierarchical object Petri nets, Fundamenta Informaticae, v.55 n.2, p.129-147, May 2003
• 7: Alain Finkel, The Minimal Coverability Graph for Petri Nets, Papers from the 12th International Conference on Applications and Theory of Petri Nets: Advances in Petri Nets 1993, p.210-243, June 01, 1991
• 8: H. F. Guo, C. R. Ramakrishnan, and I. V. Ramakrishnan. Justification based on program transformation. In M. Leuschel, editor, Logic-based Program Synthesis and Transformation (LOPSTR'2002), LNCS 2664, pages 158--159, Madrid, Spain, September 2002. Springer-Verlag.
• 9: Peter Henderson, Modelling architectures for dynamic systems, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
• 10: K. Jensen. Coloured Petri nets and the invariant-method. Theoretical Computer Science, 14:317--336, 1981.
• 11: K. Jensen. Coloured Petri Nets. Volume 1: Basic Concepts. Springer-Verlag, 1992.
• 12: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 13: R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3:147--195, 1969.
• 14: C. A. Lakos. Object Petri nets---definition and relationship to coloured nets. Technical report, TR94-3, Computer Science Department, University of Tasmania, 1994.
• 15: Michael Leuschel, Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog, Proceedings of the Third International Symposium on Practical Aspects of Declarative Languages, p.14-28, March 11-12, 2001
• 16: M. Leuschel and M. Butler. ProB: A model checker for B. In K. Araki, S. Gnesi, and D. Mandrioli, editors, FME 2003: Formal Methods, LNCS 2805, pages 855--874. Springer-Verlag, 2003.
• 17: Michael Leuschel , Jesper Jørgensen , Wim Vanhoof , Maurice Bruynooghe, Offline specialisation in Prolog using a hand-written compiler generator, Theory and Practice of Logic Programming, v.4 n.2, p.139-191, January 2004 [doi>10.1017/S1471068403001662]
• 18: Michael Leuschel , Helko Lehmann, Solving coverability problems of petri nets by partial deduction, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.268-279, September 20-23, 2000, Montreal, Quebec, Canada [doi>10.1145/351268.351298]
• 19: Michael Leuschel , Bern Martens , Danny De Schreye, Controlling generalization and polyvariance in partial deduction of normal logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.208-258, Jan. 1998 [doi>10.1145/271510.271525]
• 20: Michael Leuschel , Thierry Massart, Infinite State Model Checking by Abstract Interpretation and Program Specialisation, Selected papers from the 9th International Workshop on Logic Programming Synthesis and Transformation, p.62-81, September 22-24, 1999
• 21: M. Leuschel and T. Massart. Logic programming and partial deduction for the verification of reactive systems: An experimental evaluation. In G. Norman, M. Kwiatkowska, and D. Guelev, editors, Proceedings of AVoCS 2002, Second Workshop on Automated Verification of Critical Systems, pages 143--149, 2002. Available as Technical Report CSR-02-6, University of Birmingham.
• 22: I. A. Lomazova. Nested Petri nets --- a formalism for specification of multi-agent distributed systems. In H.-D. Burkhard, L. Czaja, H.-S. Nguyen, and P. Starke, editors, Concurrency Specification and Programming (CSP'99), Proceedings, pages 127--140. University of Warsaw, 1999.
• 23: C. A. Petri. Kommunikation mit Automaten. Technical report, Rhein.-Westfäl. Inst. für Instr. Mathematik an der Universität Bonn. Schrift Nr. 2, 1962.
• 24: Y. S. Ramakrishna , C. R. Ramakrishnan , I. V. Ramakrishnan , Scott A. Smolka , Terrance Swift , David Scott Warren, Efficient Model Checking Using Tabled Resolution, Proceedings of the 9th International Conference on Computer Aided Verification, p.143-154, June 22-25, 1997
• 25: Wolfgang Reisig, Petri nets: an introduction, Springer-Verlag New York, Inc., New York, NY, 1985
• 26: Konstantinos Sagonas , Terrance Swift , David S. Warren, XSB as an efficient deductive database engine, Proceedings of the 1994 ACM SIGMOD international conference on Management of data, p.442-453, May 24-27, 1994, Minneapolis, Minnesota, United States
• 27: Rüdiger Valk, Petri Nets as Token Objects: An Introduction to Elementary Object Nets, Proceedings of the 19th International Conference on Application and Theory of Petri Nets, p.1-25, June 22-26, 1998
• 28: Ruediger Valk, Relating Different Semantics for Object Petri Nets, Universitaet Hamburg, Hamburg, Germany, 2000

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Object-oriented design methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Petri nets
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Algorithms, Performance, Verification

Keywords:
animation, compilation, model checking, object petri nets, prolog