Tools and Methods for RTCP-Nets Modeling and Verification
Copyright policy )Tools and Methods for RTCP-Nets Modeling and Verification
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
Specification and verification (program logics, model checking, etc.), coverability graphs, CADP, nuXmv, Petri nets, Information technology, T58.5-58.64, model checking, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), QA1-939, Mathematics, RTCP-nets
Specification and verification (program logics, model checking, etc.), coverability graphs, CADP, nuXmv, Petri nets, Information technology, T58.5-58.64, model checking, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), QA1-939, Mathematics, RTCP-nets
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).9 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Top 10% impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!