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.
 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.
 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.
 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.
Financed by the National Centre for Research and Development under grant No. SP/I/1/77065/10 by the strategic scientific research and experimental development program:
SYNAT - “Interdisciplinary System for Interactive Scientific and Scientific-Technical Information”.