Tools and Methods for RTCP-Nets Modeling and Verification

Journal title

Archives of Control Sciences




No 3

Publication authors

Divisions of PAS

Nauki Techniczne


<jats:title>Abstract</jats:title> <jats:p>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 <jats:italic>μ</jats:italic>-calculus formulae hold for a given coverability graph. All presented concepts are discussed using illustrative examples</jats:p>


Committee of Automatic Control and Robotics PAS




ISSN 1230-2384


Biernacka (2015), State - based verification of RTCP - nets with nuXmv of Computational Methods in Sciences and Athens Greece, Engineering, 1702. ; Jensen (2007), Colored Petri nets and CPN Tools for modelling and validation of concurrent systems on Software Tools for Technology Transfer, Int J, 9, 213. ; InProc (1993), van derAalst : Interval timed coloured Petri nets and their analysis of the th Int on Application and Theory of Petri London UK, Nets, 14. ; Emerson (1990), Temporal and modal logic In van Leeuwen editor Handbook of Theoretical Computer BElsevier, Science Science, 995. ; Szpyrka (2006), Analysis of RTCP - nets with reachability graphs, Fundamenta Informaticae, 74, 375. ; Samolejand (2002), Time extensions of Petri nets for modelling and verification of hard real - time systems Computer, Science, 4, 55. ; Emerson (1997), Model checking and the mu - calculus InDIMACS Series in Discrete Mathematics American Mathematical, Society, 185. ; Cavada (2014), The nuXmv symbolic model checker InComputer Aided Verification ofLecture Notes in Computer Springer, Science, 8559. ; Jasiul (2014), Szpyrka andJ Malware behavior modelling with colored Petri nets InComputer Information Systems and Industrial Management Proceedings of the th Springer - Verlag, Int, 8, 8838. ; Biernacki (2015), Action - based verification of RTCP - nets with CADP of Computational Methods in Sciences and Athens Greece, Engineering, 1702. ; Cimatti (2000), a new symbolic model checker on Software Tools for Technology Transfer, Int J, 2, 410.