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.
Preview
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).
[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).
[Berthomieu 81] B. Berthomieu. "Algebraic specification of communication protocols". UCS/Inform. Sci. Inst., Rep. RR-81-98 (1981).
[Brams 83] G.W. Brams. "Réseaux de Petri: théorie et pratique". Masson (Ed.), Paris (1983).
[Dijkstra 68] E.W. Dijkstra. "Cooperating sequential processes". In Programming Languages, F. Genuys (ed.), Academic Press, New York, pp. 43–112 (1968).
[Ehrig & Mahr 85] H. Ehrig, B. Mahr. "Fundamantals of Algebraic Specifications 1. Equations and Initial Semantics". W. Brauer (Ed.), Springer-Verlag, Berlin Heidelberg (1985).
[Gaudel 79] M.C. Gaudel. "Algebraic Specification of Abstract Data Types". Rap. de Rech. no360. INRIA, Le Chesnay (1979).
[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).
[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).
[Girault & Haddad 85] C. Girault, S. Haddad. "Structure algébrique des flots d'un réseau régulier". Manuscript.
[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).
[Hoare 78] C.A.R. Hoare. "Communicating Sequential Processes". Comm. ACM, Vol. 21, No 8, pp. 666–677 (1978).
[INMOS 84] INMOS Ltd. "The occam programming manual". Prentice-Hall (1984).
[Jensen 81] K. Jensen. "Coloured Petri Nets and the Invariant Method". T.C.S. 14. North-Holland Pub. Co. (1981).
[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).
[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).
[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).
[Memml & Vautherin 86] G. Memmi, J. Vautherin. "Advanced Algebraic Techniques". Proc. Advanced Course on Petri Nets, Bad-honnef, Germany (1985).
[Oberquelle 84] H. Oberquelle. "Basic Concepts of Object-Flow Nets" Fachbereich Informatik, Universitaet of Hamburg, Mitteilung no 122, IFI-HH-M-122/84, (1984).
[Peterson 80] J.L. Peterson. "A note on coloured Petri nets". Information Processing Letters, vol.11, no1, pp. 40–43 (1980).
[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).
[Relsig 84] W. Reisig. "Petri Nets". Springer-Verlag (1985).
[Reisig 85] W. Reisig. "Petri nets with individual tokens". T.C.S. 41, pp. 185–213, North-Holland Pub. Co. (1985).
[Schmidt & Papazoglou 85] H.W. Schmidt, M. Papazoglou. "Abstract Modular Implementation of Processes by Predicate-Event systems". Manuscript.
[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).
[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).
[Stark 82] E.W. Stark. "Semaphore Primitive and Starvation-Free Mutual Exclusion". Journal of ACM, vol. 29, no 4, pp. 1049–1072 (1982)
[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).
[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).
[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).
[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).
Author information
Authors and Affiliations
Editor information
Rights 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