Skip to main content

Parallel systems specifications with coloured Petri nets and algebraic specifications

  • Conference paper
  • First Online:
Advances in Petri Nets 1987 (APN 1986)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 266))

Included in the following conference series:

Abstract

We present a way of combining algebraic specifications and Petri nets for specifying parallel systems formally. The data structure of a system is algebraically specified while its behaviour, and especially the synchronization constraints, are specified by a Petri net-like schema. The semantics of a specification is defined as a class of coloured Petri nets.

By investigating the relationship between the different models of a specification and the terminal model — which is equivalent to an ordinary Petri net (a P/T-net) — we deduce some analysis results for such specifications.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  • [ADJ 78] Groupe ADJ: J.A. Goguen, J.W. Thatcher, E.G. Wagner. "An initial algebra approach to the specification, correctness and implementation of abstract data types". Current Trends in Programming Methodology, vol. IV, R.T. Yeh Ed. Prentice Hall, New Jersey (1978).

    Google Scholar 

  • [Berthelot 83] G. Berthelot. "Transformation et analyse de réseaux de Petri. Application aux protocoles". Thèse de Doctorat d'Etat, Université de Paris-Sud (1983).

    Google Scholar 

  • [Berthomieu 81] B. Berthomieu. "Algebraic specification of communication protocols". UCS/Inform. Sci. Inst., Rep. RR-81-98 (1981).

    Google Scholar 

  • [Brams 83] G.W. Brams. "Réseaux de Petri: théorie et pratique". Masson (Ed.), Paris (1983).

    Google Scholar 

  • [Dijkstra 68] E.W. Dijkstra. "Cooperating sequential processes". In Programming Languages, F. Genuys (ed.), Academic Press, New York, pp. 43–112 (1968).

    Google Scholar 

  • [Ehrig & Mahr 85] H. Ehrig, B. Mahr. "Fundamantals of Algebraic Specifications 1. Equations and Initial Semantics". W. Brauer (Ed.), Springer-Verlag, Berlin Heidelberg (1985).

    Google Scholar 

  • [Gaudel 79] M.C. Gaudel. "Algebraic Specification of Abstract Data Types". Rap. de Rech. no360. INRIA, Le Chesnay (1979).

    Google Scholar 

  • [Genrich & Lautenbach 81] H.J. Genrich, K. Lautenbach. "System modelling with high-level Petri-nets". Theoretical Computer Science 13, pp. 109–136. North-Holland Publishing Compagny (1981).

    Article  Google Scholar 

  • [Genrich & Lautenbach 82] H.J. Genrich, K. Lautenbach. "S-invariance in Predicate/Transition-Nets". Proc. of the 3rd European Workshop on Applications and Theory of Petri Nets, Varenna, Italy, 1982. In: A. Pagnoni and G. Rozenberg (eds.): Applications and Theory of Petri Nets, Informatik-Fachberichte vol. 66, Springer-Verlag (1983).

    Google Scholar 

  • [Girault & Haddad 85] C. Girault, S. Haddad. "Structure algébrique des flots d'un réseau régulier". Manuscript.

    Google Scholar 

  • [Goltz & Reisig 84] U. Goltz, W. Reisig. "CSP-programs as nets with individual tokens". Advances in Petri Nets 1984, L.N.C.S. 188, G. Rozenberg Ed., pp. 169–196. Springer-Verlag (1985).

    Google Scholar 

  • [Hoare 78] C.A.R. Hoare. "Communicating Sequential Processes". Comm. ACM, Vol. 21, No 8, pp. 666–677 (1978).

    Article  Google Scholar 

  • [INMOS 84] INMOS Ltd. "The occam programming manual". Prentice-Hall (1984).

    Google Scholar 

  • [Jensen 81] K. Jensen. "Coloured Petri Nets and the Invariant Method". T.C.S. 14. North-Holland Pub. Co. (1981).

    Google Scholar 

  • [Jensen 82] K. Jensen. "High-level Petri Nets". Proc. of the 3rd European Workshop on Applications and Theory of Petri Nets, Varenna, Italy, 1982. In: A. Pagnoni and G. Rozenberg (eds.): Applications and Theory of Petri Nets, Inf.-Fachberichte vol. 66, Springer-Verlag (1983).

    Google Scholar 

  • [Krämer 85] B. Krämer. "Stepwise Construction of Non-Sequential Software Systems Using a Net-Based Specification Language". Advances in Petri Nets 1984, L.N.C.S. 188, G. Rozenberg Ed., pp. 307–327. Springer-Verlag (1985).

    Google Scholar 

  • [Memml 83] G. Memmi. "Méthodes d'Analyse des Réseaux de Petri, Réseaux à Files et Application aux Systèmes Temps-Réel". Thèse de Doctorat d'Etat. Université P. & M. Curie, Paris (1983).

    Google Scholar 

  • [Memml & Vautherin 86] G. Memmi, J. Vautherin. "Advanced Algebraic Techniques". Proc. Advanced Course on Petri Nets, Bad-honnef, Germany (1985).

    Google Scholar 

  • [Oberquelle 84] H. Oberquelle. "Basic Concepts of Object-Flow Nets" Fachbereich Informatik, Universitaet of Hamburg, Mitteilung no 122, IFI-HH-M-122/84, (1984).

    Google Scholar 

  • [Peterson 80] J.L. Peterson. "A note on coloured Petri nets". Information Processing Letters, vol.11, no1, pp. 40–43 (1980).

    Google Scholar 

  • [Raoult 81] J. C. Raoult. "Finiteness Results on Rewriting Systems". R.A.I.R.O. Informatique Théorique / Theoretical Informatics, vol. 5, no4, pp. 373–391(1981).

    Google Scholar 

  • [Relsig 84] W. Reisig. "Petri Nets". Springer-Verlag (1985).

    Google Scholar 

  • [Reisig 85] W. Reisig. "Petri nets with individual tokens". T.C.S. 41, pp. 185–213, North-Holland Pub. Co. (1985).

    Google Scholar 

  • [Schmidt & Papazoglou 85] H.W. Schmidt, M. Papazoglou. "Abstract Modular Implementation of Processes by Predicate-Event systems". Manuscript.

    Google Scholar 

  • [Sibertin-Blanc 85] C. Sibertin-Blanc. "High level Petri nets with data structure". Proc. of the 6th European Workshop on Applications and Theory of Petri Nets, Espoo, Finland (1985).

    Google Scholar 

  • [Silva & al. 85] M. Silva, J. Martinez, P. Ladet, H. Alla. "Generalized inverses and symbolic computation of invariants in Coloured Petri nets". Techniques et Science Informatique, TSI, no 4, pp. 113–126 (1985).

    Google Scholar 

  • [Stark 82] E.W. Stark. "Semaphore Primitive and Starvation-Free Mutual Exclusion". Journal of ACM, vol. 29, no 4, pp. 1049–1072 (1982)

    Google Scholar 

  • [Sunshine & al.] C.A. Sunshine, D.H. Thompson, R.W. Erickson, S.L. Gerhart, D. Schwabe. "Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models". IEEE Trans. Soft. Eng., vol. SE-8, no 5, (1982).

    Google Scholar 

  • [Vautherin 85a] J. Vautherin. "Non-linear invariants for coloured Petri nets with interdependent tokens; application to the proof of parallel programs". Proc. of the 6th European Workshop on Applications and Theory of Petri Nets, Espoo, Finland (1985).

    Google Scholar 

  • [Vautherin 85b] J. Vautherin. "Un modèle algébrique, basé sur les réseaux de Petri, pour l'étude des systèmes parallèles". Thèse de Doctorat d'Ingénieur. Université de Paris-Sud (1985).

    Google Scholar 

  • [Vautherin & Memmi 84] J. Vautherin, G. Memmi. "Computation of Flows for Unary Predicates/Transitions Nets". Advances in Petri Nets 1984, L.N.C.S. 188, G. Rozenberg Ed., pp. 307–327. Springer-Verlag (1985).

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Grzegorz Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vautherin, J. (1987). Parallel systems specifications with coloured Petri nets and algebraic specifications. In: Rozenberg, G. (eds) Advances in Petri Nets 1987. APN 1986. Lecture Notes in Computer Science, vol 266. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-18086-9_31

Download citation

  • DOI: https://doi.org/10.1007/3-540-18086-9_31

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-18086-9

  • Online ISBN: 978-3-540-47743-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics