Modelling and Analysis of Real-Time Systems with RTCP-Nets
Marcin Szpyrka · 2008
RTCP-nets are an adaptation of CP-nets to make modelling and verification of embedded systems easier and more efficient. Based upon the experience with application of CP-nets for embedded systems' modelling, some modifications were introduced in order to make timed CP-nets more suitable for this purpose. The main advantage of the presented formalism is the new time model. Together with transitions' priorities, the time model enable designers direct modelling of task priorities, timeouts, etc. that are typical for concurrent programming. The next advantage of RTCP-nets is the possibility of analysis of model properties with coverability graphs. Timed CP-nets can be also used to model embedded systems. A few different analysis methods have been proposed for untimed CP-nets but analysis of the timed ones may be difficult. In most cases, the state space of a live timed CP-net is infinite, so it is impossible to construct a full reachability graph that allows to analyse timing properties. To reduce such an infinite state space a few kinds of reduced reachability graphs have been defined, for example: graphs with stubborn sets, (Kristensen & Valmari 1998), graphs with equivalence classes (Jorgensen & Kristensen 1997), graphs with symmetries (Jorgensen & Kristensen 1999) and others. In most cases, analysis of time properties is impossible or limited significantly. In case of RTCP-nets coverability graphs can be used for these purposes. It has been proved (Szpyrka 2006a) that for strongly bounded RTCP-nets we may construct a finite coverability graph. Such a graph can be used for the analysis of typical Petri nets' properties as well as timing ones. The other advantage of RTCP-nets is the way hierarchical models are constructed. Using of