Tools and Methods for RTCP-Nets Modeling and Verification

• Autorzy: Szpyrka M. , Biernacki J. , Biernacka A.

Identyfikatory

DOI

10.1515/acsc-2016-0019

• Języki publikacji: EN

Abstrakty

EN

RTCP-nets are high level Petri nets similar to timed colored Petri nets, but with different time model and some structural restrictions. The paper deals with practical aspects of using RTCP-nets for modeling and verification of real-time systems. It contains a survey of software tools developed to support RTCP-nets. Verification of RTCP-nets is based on coverability graphs which represent the set of reachable states in the form of directed graph. Two approaches to verification of RTCP-nets are considered in the paper. The former one is oriented towards states and is based on translation of a coverability graph into nuXmv (NuSMV) finite state model. The later approach is oriented towards transitions and uses the CADP toolkit to check whether requirements given as μ-calculus formulae hold for a given coverability graph. All presented concepts are discussed using illustrative examples.

Słowa kluczowe

EN

RTCP-nets; Petri nets; model checking; coverability graphs; nuXmv; CADP

• Wydawca: Polish Academy of Sciences, Committee of Automatic Control and Robotics
• Czasopismo: Archives of Control Sciences
• Rocznik: 2016
• Tom: Vol. 26, no. 3
• Strony: 339--365
• Opis fizyczny: Bibliogr. 23 poz.,

Twórcy

autor

Szpyrka M.

• AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Polan

autor

Biernacki J.

• AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Polan

autor

Biernacka A.

• AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Polan

Bibliografia

• [1] W. M. P. van der Aalst: Interval timed coloured Petri nets and their analysis. In Proc. of the 14th Int. Conf. on Application and Theory of Petri Nets, 691 London, UK, (1993), 453-472.
• [2] A. Biernacka, J. Biernacki and M. Szpyrka: State-based verification of RTCP-nets with nuXmv. In Int. Conf. of Computational Methods in Sciences and Engineering (ICCMSE 2015), 1702, Athens, Greece, (2015), 100010–1–100010–4.
• [3] J. Biernacki, A. Biernacka and M. Szpyrka: Action-based verification of RTCP-nets with CADP. In Int. Conf. of Computational Methods in Sciences and Engineering (ICCMSE 2015), 1702, Athens, Greece, (2015), 100011–1–100011–4.
• [4] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri and S. Tonetta: The nuXmv symbolic model checker. In Computer Aided Verification, 8559 of Lecture Notes in Computer Science, Springer, 2014, 334–342.
• [5] A. Cimatti, E. Clarke, F. Giunchiglia and M. Roveri: NUSMV: a new symbolic model checker. Int. J. on Software Tools for Technology Transfer, 2(4), (2000), 410-425.
• [6] J. Ciszewski, K. Kunecki, W. Markowski, J. Sawicki and M. Sobecki: SITP Guideline WP-02:2010. Fire alarm systems. The design, 2010.
• [7] E. M. Clarke, O. Grumberg and D. A. Peled: Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
• [8] E. A. Emerson: Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, B Elsevier Science, 1990, 995-1072.
• [9] E. A. Emerson: Model checking and the mu-calculus. In DIMACS Series in Discrete Mathematics, American Mathematical Society, (1997), 185-214.
• [10] Emden R. Gansner and Stephen C. North: An open graph visualization system and its applications to software engineering. Softw. Pract. Exper., 30(11), (2000), 1203–1233.
• [11] H. Garavel, F. Lang, R. Mateescu and W. Serwe: CADP 2006: A toolbox for the construction and analysis of distributed processes. In Computer Aided Verification, 4590 Springer-Verlag, 2007, 158-163.
• [12] B. Jasiul, M. Szpyrka and J. Śliwa: Malware behavior modelling with colored Petri nets. In Computer Information Systems and Industrial Management Proceedings of the 13th IFIP TC8 Int. Conf. CISIM 2014, 8838 Springer-Verlag, 2014, 667-679.
• [13] K. Jensen: Colored Petri Nets. Basic Concepts, Analysis Methods and Practical Use, volume 1–3. Springer-Verlag, Berlin, Germany, 1992-1997.
• [14] K. Jensen and L. M. Kristensen: Colored Petri nets. Modelling and Validation of Concurrent Systems. Springer, Heidelberg, 2009.
• [15] K. Jensen, L.M. Kristensen and L. Wells: Colored Petri nets and CPN Tools for modelling and validation of concurrent systems. Int. J. on Software Tools for Technology Transfer, 9(3-4), (2007), 213-254.
• [16] S. Kripke: A semantical analysis of modal logic I: normal modal propositional calculi. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 9 (1963), 67-96. Announced in J. of Symbolic Logic, 24 (1959), 323.
• [17] R. Mateescu and M. Sighireanu: Efficient on-the-fly model-checking for regular alternation-free μ-calculus. Technical Report 3899, INRIA, 2000.
• [18] T. Murata: Petri nets: Properties, analysis and applications. Proc. of the IEEE, 77(4), (1989), 541-580.
• [19] C. A. Petri: Communication with automata. Technical report, New York, 1965. English translation of Kommunikation mit Automaten, PhD Dissertation, University of Bonn, 1962.
• [20] S. Samolej and T. Szmuc: Time extensions of Petri nets for modelling and verification of hard real-time systems. Computer Science, 4 (2002), 55-76.
• [21] M. Szpyrka: Analysis of RTCP-nets with reachability graphs. Fundamenta Informaticae, 74(2–3), (2006), 375-390.
• [22] M. Szpyrka: Analysis of VME-Bus communication protocol – RTCP-net approach. Real-Time Systems, 35(1), (2007), 91-108.
• [23] M. Szpyrka, A. Biernacka and J. Biernacki: Methods of translation of Petri nets to NuSMV language. In Proc. of the Concurrency Specification and Programming Workshop (CSP 2014), 1269 Chemnitz, Germany, (2014), 245-256.

Uwagi

PL

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę