AGH University of Science and Technology, Krakow (POLAND)
CADP (Construction and Analysis of Distributed Processes)
Colored Petri nets (CP-nets) is one of the most widespread classes
of high level Petri nets. They provide a discrete-event modeling
language combining capabilities of Petri nets with the capabilities
of a high-level programming language that provides the primitives
for the definition of data types, variables, expressions for
describing data manipulation. CP-nets are aimed towards modeling
a very broad class of systems including information technology,
automatics, electronics, biology, chemistry, medicine, etc. All
those systems can be characterized as concurrent ones. Equipped
with a time model, CP-nets may be used to model real-time systems.
RTCP-nets (real-time colored Petri nets) are based on CP-nets, but are equipped with different time model that makes them suitable for modeling real-time systems. Analysis of RTCP-nets may be carried out with coverability graphs. Such a graph may be used to analyze boundedness, liveness and timing properties of the corresponding RTCP-net. If the set of reachable markings of an RTCP-net is finite, it is possible to construct a finite coverability graph that represents the set of all reachable states regardless of whether the set is finite or infinite. This work proposes a modeling and verification approach based on RTCP-nets, which starts by designing a model using the CPN Tools environment. The designed model is stored using XML file format. RTCP-net Compiler is a tool that takes an RTCP-net XML file and generates a Java application, which can be used to simulate and generate the coverability graph for the considered model.
PetriNet2ModelChecker is a tool that deals with the problem of translation of RTCP-net reachability or coverability graphs into the nuXmv language and AUT format. Thus, it provides the possibility of formal verification using model checking techniques and mainstream model checkers - nuXmv for LTL and CTL temporal logics, CADP Evaluator for regular alternation-free mu-calculus. The dot2aut translator (included in the PetriNet2ModelChecker tool) is used to convert a coverability graph into AUT format. Then, such a graph is converted into BCG (Binary Coded Graphs) format accepted as input by the CADP toolbox. The BCG format is independent from any particular model-based verification technique; it can be used either by tools performing graph comparison and reduction modulo equivalence relations, or by tools checking properties expressed in temporal logics. The proposed approach is illustrated on the design and analysis of a fire alarm control panel.
This work presents a survey of tools and verification methods
(algorithms) developed for RTCP-nets recently. RTCP-nest are described
using CPN Tools, a mainstream environment for CP-nets modeling.
To simulate behaviour of an RTCP-net and to compute its reachability
and coverability graphs, the rtcpnc compiler has been developed.
Formal verification of properties is carried out by model checking
techniques. Two established model checkers are used for that purpose,
namely nuXmv and CADP. The measured times of the verification tools
on the fire alarm case study proved to be entirely satisfactory.
Verification in nuXmv is visibly slower then in CADP Evaluator.
But on the other hand, nuXmv allows to use variables' values in the
specification while in CADP one can only use edges' labels. These
two approaches complete each other allowing formal verification of
Marcin Szpyrka, Jerzy Biernacki, Agnieszka Biernacka.
"Tools and Methods for RTCP-Nets Modeling and Verification".
Archives of Control Sciences 26(3):339-365, September 2016.
Available on-line at: https://www.infona.pl/resource/bwmeta1.element.baztech-cfef2ac0-54a7-4dad-8343-cd529b4bb667
or from our FTP site in PDF or PostScript
Department of Automatics
AGH University of Science and Technology
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|