Tools and Methods for RTCP-nets Modeling and Verification

Organisation:	AGH University of Science and Technology, Krakow (POLAND)
Functionality:	Formal Verification.
Tools used:	CPN nuXmv CADP (Construction and Analysis of Distributed Processes)
Period:	2016
Description:	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.
Conclusions:	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 complex models.
Publications:	[Szpyrka-Biernacki-Biernacka-16] 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 the CADP Web site in PDF or PostScript
Contact:	Marcin Szpyrka Department of Automatics AGH University of Science and Technology Krakow Poland Email: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page