High-Level Petri Net Model Checking with AlPiNA

• Autorzy: Hostettler S. , Marechal A. , Linard A. , Risoldi M. , Buchs D.
• Języki publikacji: EN

Abstrakty

EN

Although model checking is heavily used in the hardware domain, it did not take off in software engineering yet. One of the possible reasons is that software models are very complex. They integrate many dimensions such as data types and concurrency, leading to the infamous state space explosion problem. This article introduces the Algebraic Petri Nets Analyzer (AlPiNA), a symbolic model checker for High-level Petri nets. It is comprised of two independent modules: a GUI plug-in for Eclipse and an underlying model checking engine. AlPiNA is a step towards performing efficient and user-friendly model checking of large software systems. This is achieved by separating the model and its properties from the optimisation artifacts. This article describes the features that AlPiNA provides to the user for designing models and verifying properties. It also presents the techniques and artifacts used for tuning verification performance, along with some theoretical background.

Słowa kluczowe

EN

system design and verification; Higher-level nets models; algebraic Petri nets; state space generation; computer tools for nets; model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 113, nr 3/4
• Strony: 229--264
• Opis fizyczny: Bibliogr. 49 poz., wykr.

Twórcy

autor

Hostettler S.

autor

Marechal A.

autor

Linard A.

autor

Risoldi M.

autor

Buchs D.

• Centre Universitaire d’Informatique Université de Geneve Route de Drize 7, CH-1227 Carouge, Switzerland,

Bibliografia

• [1] Al-Shabibi, A., Buchs, D., Buffo, M., Chachkov, S., Chen, A., Hurzeler, D.: Prototyping Object Oriented Specifications, in: Applications and Theory of Petri Nets 2003 (W. van der Aalst, E. Best, Eds.), vol. 2679 of Lecture Notes in Computer Science, Springer, 2003, 473-482.
• [2] Barbey, S., Buchs, D., Péraire, C.: A theory of specification-based testing for object-oriented software, in: Dependable Computing - EDCC-2 (A. Hlawiczka, J. Silva, L. Simoncini, Eds.), vol. 1150 of Lecture Notes in Computer Science, Springer, 1996, 303-320, Also available as Tech. Report (EPFL-DI-LGL No 96/163).
• [3] Barwise, J., Etchemendy, J.: The Language of First-Order Logic (Windows Program, Tarski's World), 3rd Ed., Revised & Expanded, Center for the Study of Language and Information, Stanford University, April 1993, ISBN 0937073903.
• [4] Bryant, R. E.: Graph-based algorithms for boolean functionmanipulation, Transactions on Computers, C-35, IEEE, 1986, 677-691.
• [5] Buchs, D., Guelfi, N.: A Formal Specification Framework for Object-Oriented Distributed Systems, IEEE Transactions on Software Engineering, 26(7), July 2000, 635-652.
• [6] Buchs, D., Hostettler, S.: Managing Complexity in Model Checking with Decision Diagrams for Algebraic Petri Net, Pre-proceedings of the InternationalWorkshop on Petri Nets and Software Engineering (D.Moldt, Ed.), 2009, 255-271, Available at htp:/w.inf ormatik.uni-hamburg.de/TGI/evnts/pnse09/pnse09-profirstagespdedings- .
• [7] Buchs, D., Hostettler, S.: Sigma Decision Diagrams, TERMGRAPH 2009: Preliminary proceedings of the 5th International Workshop on Computing with Terms and Graphs (A. Corradini, Ed.), number TR-09-05 in TERMGRAPH workshops, Università di Pisa, 2009, 18-32, Available at htp:/ompas2.di.unip.it/TR/Files/TR-09-05.pdf.gz.
• [8] Buchs, D., Hostettler, S.: Toward Efficient State Space Generation of Algebraic Petri Nets, Technical Report 206, CUI, Université de Genève, htp:/arhive-ouverte.unige.h/unige:1232, January 2009.
• [9] Buchs, D., Hostettler, S., Marechal, A., Risoldi, M.: AlPiNA: An Algebraic Petri Net Analyzer, in: Tools and Algorithms for the Construction and Analysis of Systems (J. Esparza, R. Majumdar, Eds.), vol. 6015 of Lecture Notes in Computer Science, Springer, 2010, 349-352.
• [10] Buchs, D., Lucio, L., Chen, A.: Model Checking Techniques for Test Generation from Business Process Models, in: Reliable Software Technologies - Ada-Europe 2009 (F. Kordon, Y. Kermarrec, Eds.), vol. 5570 of Lecture Notes in Computer Science, Springer, 2009, 59-74.
• [11] Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., Hwang, L. J.: Symbolic model checking: 1020 states and beyond, Information and Computation, 98(2), 1992, 142-170, ISSN 0890-5401.
• [12] Ciardo, G., Lüttgen, G., Siminiceanu, R.: Efficient Symbolic State-Space Construction for Asynchronous Systems, in: Application and Theory of Petri Nets 2000 (M. Nielsen, D. Simpson, Eds.), vol. 1825 of Lecture Notes in Computer Science, Springer, 2000, 103-122.
• [13] Ciardo, G., Lüttgen, G., Siminiceanu, R.: Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation, in: Tools and Algorithms for the Construction and Analysis of Systems (T. Margaria, W. Yi, Eds.), vol. 2031 of Lecture Notes in Computer Science, Springer, 2001, 328-342.
• [14] Clarke, E. M., Emerson, E. A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, Springer, 1982, ISBN 3-540-11212-X, 52-71.
• [15] Clarke, Jr., E. M., Grumberg, O., Peled, D. A.: Model checking, MIT Press, Cambridge, MA, USA, 1999, ISBN 0-262-03270-8.
• [16] Clavel,M., Durán, F., Eker, S., Lincoln, P.,Martí-Oliet, N.,Meseguer, J., Quesada, J. F.: Maude: specification and programming in rewriting logic, Theor. Comput. Sci., 285, August 2002, 187-243, ISSN 0304-3975.
• [17] Couvreur, J.-M., Encrenaz, E., Paviot-Adet, E., Poitrenaud, D., Wacrenier, P.-A.: Data Decision Diagrams for Petri Net Analysis, in: Application and Theory of Petri Nets 2002 (J. Esparza, C. Lakos, Eds.), vol. 2360 of Lecture Notes in Computer Science, Springer, 2002, 129-158.
• [18] Couvreur, J.-M., Thierry-Mieg, Y.: Hierarchical Decision Diagrams to Exploit Model Structure, in: Formal Techniques for Networked and Distributed Systems - FORTE 2005 (F.Wang, Ed.), vol. 3731 of Lecture Notes in Computer Science, Springer, 2005, 443-457.
• [19] Dutheillet, C., Ilié, J.-M., Poitrenaud, D., Vernier-Mounier, I.: State-Space-Based Methods and Model Checking, in: Petri Nets for Systems Engineering, A Guide to Modeling, Verification, and Applications (C. Girault, R. Valk, Eds.), chapter 14, Springer, 2002, 201-276.
• [20] Eclipse: Eclipse Modeling Project, htp:/w.elipse.org/modeling/.
• [21] Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, Monographs in Theoretical Computer Science. An EATCS Series, Springer, 1985.
• [22] Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns - Elements of Reusable Object-Oriented Software, Professional Computing, Addison-Wesley, 1995.
• [23] Geldenhuys, J., Valmari, A.: Techniques for Smaller Intermediary BDDs, CONCUR 2001 - Concurrency Theory (K. Larsen, M. Nielsen, Eds.), 2154, Springer, 2001, ISBN 978-3-540-42497-0, 233-247.
• [24] Godefroid, P.: Using partial orders to improve automatic verification methods, in: Computer-Aided Verification (E. Clarke, R. Kurshan, Eds.), vol. 531 of Lecture Notes in Computer Science, Springer, 1991, 176-185.
• [25] Goguen, J. A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci., 105, November 1992, 217-273, ISSN 0304-3975.
• [26] Goto, E.: Monocopy and Associative Algorithms in Extended Lisp, Technical Report TR-74-03, University of Tokyo, 1974.
• [27] Object Management Group: Business Process Model and Notation (BPMN) version 2.0, htp:/w.omg.org/spe/BPMN/2.0/PDF/.
• [28] Hamez, A., Thierry-Mieg, Y., Kordon, F.: Building EfficientModel Checkers using Hierarchical Set Decision Diagrams and Automatic Saturation, Fundamenta Informaticae, 94(3-4), 2009, 413-437.
• [29] Hong, S., Kordon, F., Paviot-Adet, E., Evangelista, S.: Computing a Hierarchical Static order for Decision Diagram-Based Representation from P/T Nets, Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), 2012, Accepted, in press.
• [30] Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Volume 1, Monographs in Theoretical Computer Science. An EATCS Series, Springer, 1997.
• [31] Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use: Volume 2, Monographs in Theoretical Computer Science. An EATCS Series, Springer, 1997, ISBN 3540582762.
• [32] Kordon, F., Linard, A., Buchs, D., Colanage, M., Evangelista, S., Jensen, J. F., Lampka, K., Lohmann, N., Paviot-Adet, E., Thierry-Mieg, Y., Wimmel, H.: Report on the Model Checking Contest at Petri Nets 2011, Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), 2011, Submitted.
• [33] Linard, A., Paviot-Adet, E., Kordon, F., Buchs, D., Charron, S.: polyDD: Towards a Framework Generalizing Decision Diagrams, Application of Concurrency to System Design (ACSD), 2010 10th International Conference on, June 2010, ISSN 1550-4808, 124 -133.
• [34] Lucio, L., Hostettler, S.: Multi-Set Decision Diagrams, Technical Report 205, CUI, Université de Genève, htp:/smv.unige.h/tehnial-reports/pdfs/TR205-MSD.pdf, January 2009.
• [35] Marechal, A., Buchs, D.: Properties specification language for Algebraic Petri Nets, Technical Report 216, Université de Genève, htp:/smv.unige.h/tehnial-reports/pdfs/ApnProperties.pdf,October 2010.
• [36] Michie, D.: "Memo" functions and machine learning, Nature, 218(218), 1968, 19-22.
• [37] Murata, T.: Petri nets: Properties, analysis and applications, Proceedings of the IEEE, 77(4), April 1989, 541-580, ISSN 0018-9219.
• [38] Pajault, C., Evangelista, S.: High LEvel Net Analyzer, 2009, htp:/helna-m.soureforge.net/.
• [39] Pedro, L., Risoldi, M., Buchs, D., Amaral, V.: Developing Domain-Specific Modeling Languages by MetamodelSemantic Enrichment and Composition: a Case Study, Proceedings of the 10th workshop on Domain-Specific Modeling (DSM'10), Aalto University School of Economics, 2010, ISBN 978-952-60-1043-4, 97-102.
• [40] Pnueli, A.: The Temporal Logic of Programs, 18th Annual Symposium on Foundations of Computer Science,31 October-2 November, Providence, Rhode Island, USA, IEEE, 1977, 46-57.
• [41] Reisig, W.: Petri nets and algebraic specifications, Theor. Comput. Sci., 80, March 1991, 1-34, ISSN 0304-3975.
• [42] Rice, M., Kulhari, S.: A Survey of Static Variable Ordering Heuristics for Efficient BDD/MDD Construction, Technical report, University of California, Riverside, 2008.
• [43] Risoldi, M.: A Methodology For The Development Of Complex Domain Specific Languages, Ph.D. Thesis, University of Geneva, 2010, Number 4230.
• [44] Sedlmajer, N., Buchs, D., Hostettler, S., Linard, A., Lopez, E., Marechal, A.: GReg: a Domain Specific Language for the Modeling of Genetic Regulatory Mechanisms, BioPPN 2011: International Workshop on Biological Processes & Petri Nets (M. Heiner, H. Matsuno, Eds.), 724, CEUR-WS, 2011, 21-35.
• [45] Terese: Term Rewriting Systems, vol. 55 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2003.
• [46] Valmari, A.: A stubborn attack on state explosion, Form. Methods Syst. Des., 1(4), 1992, 297-322, ISSN 0925-9856.
• [47] Valmari, A.: The state explosion problem, in: Lectures on Petri Nets I: Basic Models (W. Reisig, G. Rozenberg, Eds.), vol. 1491 of Lecture Notes in Computer Science, Springer, 1998, ISBN 978-3-540-65306-6, 429-528.
• [48] Vautherin, J.: Parallel systems specifications with coloured Petri nets and algebraic specifications, in: Advances in Petri Nets 1987 (G. Rozenberg, Ed.), vol. 266 of Lecture Notes in Computer Science, Springer, 1987, 293-308.
• [49] Weber, M., Kindler, E.: The Petri Net Markup Language, in: Petri Net Technology for Communication-Based Systems (H. Ehrig,W. Reisig, G. Rozenberg, H.Weber, Eds.), vol. 2472 of Lecture Notes in Computer Science, Springer, 2003, 124-144.