Compositional Petri Net Approach to the Development of Concurrent and Distributed Systems
Tóm tắt
In the paper, a formal model based on Petri nets is proposed in the context of a compositional approach to the development and analysis of complex concurrent and distributed systems. Mutlilabels of Petri nets are introduced allowing labeling a transition not only with a single symbol, but also with a multiset of symbols. Operations on multilabeled Petri nets—parallel composition and restriction—are defined. A definition of a Petri net entity is given based on the notion of multilabels. A Petri net entity is a Petri net with a set of multilabels, where each multilabel is regarded as an access point of the entity. The operation of entity composition is introduced. Equivalence of entities is defined based on bisimulation equivalence of Petri nets. It is shown that the equivalence relation is congruent with respect to entity composition. It is also demonstrated that the composition operation is commutative and associative.
Tài liệu tham khảo
Anisimov, N.A., Hierarchical Composition of Protocols, Avtom. Vychisl. Tekh., 1990, no. 1, pp. 3-10.
Achasova, S.M. and Bandman, O.L., Korrektnost' parallel'nykh vychislitel'nykh protsessov (Correctness of Parallel Computational Processes), Novosibirsk: Nauka, 1990.
Kotov, V.E., Seti Petri (Petri Nets), Moscow: Nauka, 1984.
Protokoly informatsionno-vychislitel'nykh setei. Spravochnik (Protocols of Information Computational Networks. Handbook), Mizina, I.A. and Kuleshova, A.P., Eds., Moscow: Radio i Svyaz', 1990.
Hoare, C., Communicating Sequential Processes, Englewood Cliffs: Prentice-Hall, 1985. Translated under the title Vzaimodeistvuyushchie posledovatel'nye protsessy, Moscow: Mir, 1989.
Alaiwan, H. and Toudic, J.M., Recherche de Semiflots, des Verrous et Trappes dans les Reseaux de Petri, Technique Et Sciences Informatiques, 1985, vol. 4, pp. 103-112.
Anisimov, N.A., A Petri Net Entity as a Formal Model for LOTOS, a Specification Language for Distributes and Concurrent Systems, Parallel Computing Technologies, Mirenkov, N.N., Ed., Singapore: World Sci., 1991, pp. 440-450.
Anisimov, N.A. and Koutny, M., On Compositionality and Petri Nets in Protocol Engineering, Protocol Speci-fication, Testing and Verification, XV, Dembinski, P. and Sredniawa, M., Eds., Chapman & Hall, 1996, pp. 71-86.
Anisimov, N.A., Kovalenko, A.A., Tarasov, G.V., Inzartsev, A.V., and Sherbatyuk, A.Ph., A Graphical Environment for AUV Mission Programming and Verification, Proc. of the 10th Int. Symp. on Unmanned Untethered Submersible Technology, New Hermpshire, USA, 1997, pp. 394-405.
Anisimov, N.A., Kovalenko, A.A., Postupalski, P.A., and Vuong, S.T., Application of Compositional Petri Nets and PN3-Tool to the Specification of Distributed Multimedia Objects, Advances in Distributed Multimedia Systems, Chang, S.K. et al., Eds., Singapore: World Sci., 1999, pp. 99-116.
Barbeau, M. and Bochmann, G.V., A Subset of Lotos with Computational Power of Place/Transition Nets, Lecture Notes in Computer Science, 1993, vol. 691, pp. 49-68.
Baumgarten, B., Ochsenschläger, P., and Prinoth, R., Building Blocks for Distributed System Design, Protocol Specification, Testing, and Verification, Diaz, M., Ed. (Proc. of the V IFIP WG 6.1 Conf.), North-Holland: Elsevier, 1986, pp. 19-38.
Berthelot, G., Roucairol, G., and Valk, R., Reduction of Nets and Parallel Programs, Lecture Notes in Computer Science, 1980, vol. 84, pp. 277-290.
Bergstra, J.A. and Klop, J.W., Algebra of Communicating Processes, in Math. on Comput. Sci. (Proc. CWI Symp.), 1986, pp.89-138.
Bernadinello, L. and De Cindio, F., A Survey of Basic Net Models and Modular Classes, Lecture Notes in Computer Sciences, Springer, 1992, vol. 609, pp. 304-351.
Best, E., Devillers, R., Kiehn, A., and Pomello, L., Concurrent Bisimulations in Petri Nets, Acta Informatica, 1991, vol. 28, pp. 231-261.
Best, E., Devillers, R., and Hall, J.G., The Box Calculus: A New Causal Algebra with Miltilabel Communication, Lecture Notes in Computer Sciences, Springer, 1992, vol. 609, pp. 21-69.
Bolognesi, T. and Brinksma, E., Introduction to the ISO Specification Language LOTOS, Comput. Networks ISDN Systems, 1987, vol. 14, pp. 25-89.
Cherkasova, L.A. and Kotov, V.E., Structured Nets, Lecture Notes in Computer Sciences, Springer, 1981, vol. 118, pp. 242-251.
Van Glabbeek, R.J., The Linear Time-Branching Time Spectrum, Lecture Notes in Computer Sciences, Berlin: Springer, 1990, vol. 458, pp. 278-297.
Van Glabbeek, R.J. and Vaandrager, F.W., Petri Net Models for Algebraic Theories of Concurrency, Lecture Notes in Computer Sciences, Springer, 1987, vol. 259, pp. 224-242.
Goltz, U., On Representing CCS Programs by Finite Petri Nets, Lecture Notes in Computer Sciences, Springer, 1988, vol. 324, pp. 339-350.
Hopkins, R., Hall, J., and Botti, O., A Basic-Net Algebra for Programs Semantics and Application to OCCAM, Lecture Notes in Computer Scences, Springer, 1992, vol. 609, pp. 179-214.
High-Level Petri Nets. Theory and Application, Jensen, K. and Rozenberg, G., Eds., Springer, 1991.
Kotov, V.E., An Algebra for Parallelism Based on Petri Nets, Lecture Notes in Computer Sciences, Springer, 1978, vol. 64, pp. 39-55.
Mauw, S. and Veltink, G.J., A Process Specification Formalism, Fundamenta Informaticae XIII, 1990, pp. 85-139.
Milner, R., A Calculus for Communication Systems, Lecture Notes in Computer Sceinces, Springer, 1980, vol. 92.
Olderog, E.-R., Operational Petri Net Semantics for CCSP, Lecture Notes in Computer Sciences, Springer, 1984, vol. 266.
Pomello, L., Rozenberg, G., and Simone, C., A Survey of Equivalence Notions for Net Based Systems, Lecture Notes in Computer Sciences, Springer, 1992, vol. 609.
Lecture Notes on Petri Nets. Parts I and II, Lecture Notes in Computer Sciences, Reising, W. and Rozenberg, G., Eds., Springer, 1998, vols. 1491-1492.
Advances in Petri Nets 1992, Lecture Notes in Computer Sciences, Rozenberg, G., Ed., Springer, 1992, vol. 609.
Taubner, D., Finite Representation of CCS and TCSP Programs by Automata and Petri Nets, Lecture Notes in Computer Sciences, Springer, 1989, vol. 369.
Valette, R., Analysis of Petri Nets by Stepwise Refinements. J. Comput. System Sci., 1979, vol. 18, pp. 35-46.
Vogler, W., Failures Semantics and Deadlocking of Modular Petri Nets, Acta Informatica, 1989, vol. 26, pp. 333-348.
Voss, K., System Specification with Labelled Nets and the Notion of Interface Equivalence, Arbeitspapiere Der GMD, 1986, vol. 221.