Analysis of RTCP-nets with Reachability Graphs

• Autorzy: Szpyrka M.
• Języki publikacji: EN

Abstrakty

EN

RTCP-nets are a subclass of timed coloured Petri nets defined for modelling and analysis of embedded real-time systems. One of the main advantages of strongly bounded RTCP-nets is a possibility to present the set of reachable states of an RTCP-net using a finite reachability and/or coverability graph. These graphs can be used to verify most of the net's properties, including the timing ones. The paper discusses analysis methods based on these graphs. A formal definition of RTCP-nets and a survey of their properties are also presented in the paper.

Słowa kluczowe

EN

RTCP-nets; analysis; reachability graphs; coverability graphs

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 74, nr 2,3
• Strony: 375--390
• Opis fizyczny: bibliogr. 10 poz., wykr.

Twórcy

autor

Szpyrka M.

• Institute of Automatics, AGH University of Science and technology, Al. Mickiewicza 30, 30-059 Kraków, Poland,

Bibliografia

• [1] Bowden, F. D. J.: Modelling Time in Petri Nets, Proceedings of the Second Australia-Japan Workshop on Stochastic Models in Engineering, Technology and Management, Gold Coast, Australia, 6-9 July 1996.
• [2] Christensen, S., Kristensen, L. M., Mailund, T.: Condensed State Spaces for Timed Petri Nets, Proc. of 22nd International Conf. on Applications and Theory of Petri Nets 2001 (ICATPN 2001), 2075, Newcastle upon Tyne, UK, 2001.
• [3] Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, vol. 1-3, Springer-Verlag, 1992-1997.
• [4] Jørgensen, J. B., Kristensen, L. M.: Verification of Coloured Petri Nets Using State Spaces with Equivalence Classes, Proceedings of Workshop on Petri Nets in System Engineering, Modelling, Verification and Validation, Hamburg, Germany, 25-26 September 1997.
• [5] Jørgensen, J. B., Kristensen, L. M.: Computer Aided Verification of Lamport's Fast Mutual Exclusion Algorithm Using Coloured Petri Nets Occurrence Graphs with Symmetries, IEEE Transactions on Parallel and Distributed Systems, 10(7), 1999, 714-732.
• [6] Murata, T.: Petri Nets: Properties, Analysis and Applications, Proceedings of the IEEE, 77(4), 1989, 541-580.
• [7] Samolej, S., Szmuc, T.: Time Extensions of Petri Nets for Modelling and Verification of Hard Real-Time Systems, Computer Science, 4, 2002, 55-76.
• [8] Szpyrka, M.: Fast and Flexible Modelling of Real-time Systems with RTCP-nets, Computer Science, 6, 2004, 81-94.
• [9] Szpyrka, M., Szmuc, T., Matyasik, P., Szmuc, W.: A Formal Approach to Modelling of Real-time Systems Using RTCP-nets, Foundations of Computing and Decision Sciences, 30(1), 2005, 61-71.
• [10] Valmari, A.: Stubborn Sets of Coloured Petri Nets, Proceedings of the 12th International Conference on Application and Theory of Petri Nets, 674, Gjern, Denmark, June 1991.