TY - JOUR N2 - Abstract 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 L1 - http://www.czasopisma.pan.pl/Content/104498/PDF/acsc-2016-0019.pdf L2 - http://www.czasopisma.pan.pl/Content/104498 PY - 2016 IS - No 3 DO - 10.1515/acsc-2016-0019 A1 - Szpyrka, Marcin A1 - Biernacki, Jerzy A1 - Biernacka, Agnieszka PB - Committee of Automatic Control and Robotics PAS DA - 2016 T1 - Tools and Methods for RTCP-Nets Modeling and Verification UR - http://www.czasopisma.pan.pl/dlibra/publication/edition/104498 T2 - Archives of Control Sciences ER -