Generalizing the Compositions of Petri Nets Modules

• Autorzy: Marechal A. , Buchs D.

Identyfikatory

DOI

10.3233/FI-2015-1171

• Języki publikacji: EN

Abstrakty

EN

Modularity is a mandatory principle to apply Petri nets to real world-sized systems. Modular extensions of Petri nets allow to create complex models by combining smaller entities. They facilitate the modeling and verification of large systems by applying a divide and conquer approach and promoting reuse. Modularity includes a wide range of notions such as encapsulation, hierarchy and instantiation. Over the years, Petri nets have been extended to include these mechanisms in many different ways. The heterogeneity of such extensions and their definitions makes it difficult to reason about their common features at a general level. We propose in this article an approach to standardize the semantics of modular Petri nets formalisms, with the objective of gathering even the most complex modular features from the literature. This is achieved with a new Petri nets formalism, called the LLAMAS Language for Advanced Modular Algebraic Nets (LLAMAS). We focus principally on the composition mechanism of LLAMAS, while introducing the rest of the language with an example. The composition mechanism is introduced both informally and with formal definitions. Our approach has two positive outcomes. First, the definition of new formalisms is facilitated, by providing common ground for the definition of their semantics. Second, it is possible to reason at a general level on the most advanced verification techniques, such as the recent advances in the domain of decision diagrams.

Słowa kluczowe

EN

system design and verification; modularity; high-level Petri nets; standardization; composition mechanism; LLAMAS

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2015
• Tom: Vol. 137, nr 1
• Strony: 87--116
• Opis fizyczny: Bibliogr. 32 poz., rys.

Twórcy

autor

Marechal A.

• Centro de Investigaciones en Nuevas Tecnolog´ıas Inform´aticas Universidad Privada Boliviana, La Paz, Bolivia

autor

Buchs D.

• Centre Universitaire d’Informatique, University of Geneva 7 route de Drize, 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. Aalst, E. Best, Eds.), vol. 2679 of LNCS, Springer Berlin Heidelberg, 2003, ISBN 978-3-540-40334-0, 473–482.
• [2] Biberstein, O., Buchs, D., Guelfi, N.: Object-Oriented Nets with Algebraic Specifications: The CO-OPN/2 Formalism, in: Concurrent Object-Oriented Programming and Petri Nets (G. Agha, F. Cindio, G. Rozenberg, Eds.), vol. 2001 of LNCS, Springer Berlin Heidelberg, 2001, ISBN 978-3-540-41942-6, 73–130.
• [3] Bruni, R., Montanari, U.: Zero-Safe Nets, or Transition Synchronization Made Simple., Electronic Notes in Theoretical Computer Science: Proceedings of EXPRESS’97, 4th workshop on Expressiveness in Concurrency, 7, Elsevier Science, 1997.
• [4] 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`a di Pisa, 2009.
• [5] 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 LNCS, Springer Berlin Heidelberg, 2010, ISBN 978-3-642-12001-5, 349–352.
• [6] Christensen, S., Damgaard Hansen, N.: Coloured Petri Nets extended with channels for synchronous communication, in: Application and Theory of Petri Nets 1994 (R. Valette, Ed.), vol. 815 of LNCS, Springer Berlin Heidelberg, 1994, ISBN 978-3-540-58152-9, 159–178.
• [7] Christensen, S., Petrucci, L.: Modular Analysis of Petri Nets, Comput. J., 43(3), 2000, 224–242.
• [8] Clark, K. L.: Negation as failure, in: Logic and Data Bases (J. Minker, Ed.), vol. 1, Plenum Press, 1978, 293–322.
• [9] Devillers, R., Klaudel, H., Riemann, R.-C.: General parameterised refinement and recursion for the M-net calculus, Theoretical Computer Sc., 300, 2003, 259–300, ISSN 0304-3975.
• [10] Gelder, A. V.: Negation as failure using tight derivations for general logic programs, The Journal of Logic Programming, 6(1–2), 1989, 109 – 133, Special Issue:Third {IEEE} Symposium on Logic Programming.
• [11] Hillah, L., Kordon, F., Petrucci, L., Tr`eves, N.: PNML Framework: An Extendable Reference Implementation of the Petri Net Markup Language, in: Applications and Theory of Petri Nets (J. Lilius, W. Penczek, Eds.), vol. 6128 of LNCS, Springer Berlin Heidelberg, 2010, ISBN 978-3-642-13674-0, 318–327.
• [12] Hillah, L.-M., Kordon, F., Lakos, C., Petrucci, L.: Extending pnml Scope: A Framework to Combine Petri Nets Types, in: Transactions on Petri Nets and Other Models of Concurrency VI (K. Jensen, W. Aalst, M. Ajmone Marsan, G. Franceschinis, J. Kleijn, L. Kristensen, Eds.), vol. 7400 of LNCS, Springer Berlin Heidelberg, 2012, ISBN 978-3-642-35178-5, 46–70.
• [13] Hoare, C. A. R.: Communicating sequential processes, CACM, 21(8), 1978, 666–677.
• [14] Hostettler, S.: High-Level Petri Net Model Checking, The Symbolic Way, Ph.D. dissertation, University of Geneva, 2012.
• [15] Hostettler, S., Marechal, A., Linard, A., Risoldi, M., Buchs, D.: High-Level Petri Net Model Checking with AlPiNA, Fundam. Inf., 113(3-4), August 2011, 229–264, ISSN 0169-2968.
• [16] Huber, P., Jensen, K., Shapiro, R.: Hierarchies in coloured petri nets, in: Advances in Petri Nets 1990 (G. Rozenberg, Ed.), vol. 483 of LNCS, Springer Berlin Heidelberg, 1991, ISBN 978-3-540-53863-9, 313–341.
• [17] ISO/IEC: Software and Systems Engineering – High-level Petri Nets, Part 1: Concepts, Definitions and Graphical Notation, International Standard ISO/IEC 15909-1, 2004.
• [18] Jensen, K.: Coloured Petri nets: basic concepts, analysis methods, and practical use, Number vol. 1 in EATCS monographs on theoretical computer science, Springer-Verlag, 1992.
• [19] Köhler-Bußmeier, M.: Hornets: Nets within Nets Combined with Net Algebra, in: Applications and Theory of Petri Nets (G. Franceschinis, K. Wolf, Eds.), vol. 5606 of LNCS, Springer Berlin Heidelberg, 2009, ISBN 978-3-642-02423-8, 243–262.
• [20] Kindler, E., Petrucci, L.: Towards a Standard for Modular Petri Nets: A Formalisation, in: Applications and Theory of Petri Nets (G. Franceschinis, K.Wolf, Eds.), vol. 5606 of LNCS, Springer Berlin Heidelberg, 2009, ISBN 978-3-642-02423-8, 43–62.
• [21] Klaudel, H., Pommereau, F.: M-nets: a survey, Acta Informatica, 45(7-8), 2009, 537–564.
• [22] Kummer, O.: Referenznetze, Logos Verlag Berlin, 2002, ISBN 9783832500351.
• [23] Lakos, C.: Object Oriented Modeling with Object Petri Nets, Concurrent Object-Oriented Programming and Petri Nets, 2001.
• [24] Marechal, A.: Unifying the Syntax and Semantics of Modular Extensions of Petri Nets, Ph.D. dissertation, University of Geneva, 2013.
• [25] Marechal, A., Buchs, D.: Modular extensions of Petri Nets: a generic template metamodel, Technical Report 220, University of Geneva, 2012.
• [26] Marechal, A., Buchs, D.: Modular extensions of Petri nets: a survey, Technical Report 218, University of Geneva, 2012.
• [27] Marechal, A., Buchs, D.: Unifying the Semantics of Modular Extensions of Petri Nets, in: Application and Theory of Petri Nets and Concurrency (J.-M. Colom, J. Desel, Eds.), vol. 7927 of LNCS, Springer Berlin Heidelberg, 2013, ISBN 978-3-642-38696-1, 349–368.
• [28] Reiter, R.: On Closed World Data Bases, Logic and Data Bases, 1977.
• [29] Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical Set Decision Diagrams and Regular Models, 15th Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, Springer, 2009, ISBN 978-3-642-00767-5.
• [30] Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical Set Decision Diagrams and Regular Models, in: Tools and Algorithms for the Construction and Analysis of Systems (S. Kowalewski, A. Philippou, Eds.), vol. 5505 of LNCS, Springer Berlin Heidelberg, 2009, ISBN 978-3-642-00767-5, 1–15.
• [31] Tiu, A.: Stratification in Logics of Definitions, in: Automated Reasoning (B. Gramlich, D. Miller, U. Sattler, Eds.), vol. 7364 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2012, ISBN 978-3-642-31364-6, 544–558.
• [32] Valk, R.: Object Petri Nets, in: Lectures on Concurrency and Petri Nets (J. Desel, W. Reisig, G. Rozenberg, Eds.), vol. 3098 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, 2004, ISBN 978-3-540-22261-3, 819–848.