Abstract
This paper presents the combination of two well established principles: the CO-OPN synchronisation mechanism, and the Merlin and Farber time Petri nets. Real-time synchronised Petri nets systems are then defined such that a Petri net is an object that can ask to be synchronised with another net, and whose transition firing is constrained by relative time intervals. Our proposal enables to define complex systems with compact specifications, whose semantics is given through a small set of Structured Operational Semantics (sos) rules. The applicability of the new model is shown by applying it to a traditional benchmark adopted in the literature of real-time systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
B. Berthomieu. La méthode des Classes d’États pour l’Analyse des Réseaux Temporels-Mise en Oeuvre, Extension à la multi-sensibilisation. In Modélisation des Systèmes Réactifs, MSR’2001. Hermes, 2001.
O. Biberstein, D. Buchs, and N. Guelfi. Object-oriented nets with algebraic specifications: The CO-OPN/2 formalism. In G. Agha, F. De Cindio, and G. Rozenberg, editors, Advances in Petri Nets on Object-Orientation, volume 2001 of LNCS, pages 70–127. Springer-Verlag, 2001.
G. Bucci and E. Vicario. Compositional Validation of Time-Critical Systems Using Communicating Time Petri Nets. IEEE Transactions on Software Engineering, 21(12):969–992, 1995.
D. Buchs and N. Guelfi. A formal specification framework for object-oriented distributed systems. IEEE Transactions on Software Engineering, Special Section on Formal Methods for Object Systems, 26(7):635–652, July 2000.
G. Di Marzo Serugendo, D. Mandrioli, D. Buchs, and N. Guelfi. Real-time synchronised Petri nets. Technical Report 2000/341, Swiss Federal Institute of Technology (EPFL), Software Engineering Laboratory, Lausanne, Switzerland, 2000.
M. Felder, D. Mandrioli, and A. Morzenti. Proving properties of real-time systems through logical specifications and Petri net models. IEEE Transactions on Software Engineering, 20(2):127–141, February 1994.
A. Gargantini and A. Morzenti. Automated Deductive Requirements Analysis of Critical Systems. ACM TOSEM-Transactions On Software Engineering and Methodologies, 10(3):255–307, July 2001.
C. Heitmeyer and D. Mandrioli, editors. Formal methods for real-time computing. John Wiley & Sons, 1996.
M. Koutny. A Compositional Model of Time Petri Nets. In M. Nielsen and D. Simpson, editors, International Conference on Application and Theory of Petri Nets 2000, volume 1825 of LNCS, pages 303–322. Springer-Verlag, 2000.
C. A. Lakos and S. Christensen. A General Systematic Approach to Arc Extensions for Coloured Petri Nets. In R. Vallette, editor, Proceedings of the 15th International Conference on Application and Theory of Petri Nets, volume 815 of LNCS, pages 338–357. Springer-Verlag, 1994.
P.M. Merlin and D.J. Farber. Recoverability of communication protocols-implications of a theoretical study. IEEE Transactions on Communications, 24(9):1036–1043, 1976.
S. Souksavanh. Operational Semantics for Real-Time Synchronized Petri Nets. Master’s thesis, Swiss Federal Institute of Technology (EPFL), Software Engineering Laboratory, Lausanne, Switzerland, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Di Marzo Serugendo, G., Mandrioli, D., Buchs, D., Guelfi, N. (2002). Real-Time Synchronised Petri Nets. In: Esparza, J., Lakos, C. (eds) Application and Theory of Petri Nets 2002. ICATPN 2002. Lecture Notes in Computer Science, vol 2360. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48068-4_10
Download citation
DOI: https://doi.org/10.1007/3-540-48068-4_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43787-1
Online ISBN: 978-3-540-48068-6
eBook Packages: Springer Book Archive