AGH University of Science and Technology (POLAND)
CADP (Construction and Analysis of Distributed Processes)
3077 states and 3986 transitions.
A common practice in construction of fire alarm control panels, aiming
at the reduction of false fire alarms, is alarm variants usage. The
most popular variant is the two-stage alarming, which requires
personnel participation with strictly defined roles in the alarm
verification process. Erroneous behaviour of a fire alarm system may
cause major losses: false alarms generate high costs, and delays can
lead to loss of human lives and health. Therefore, a comprehensive
verification of such systems is of utmost importance.
A model of a fire alarm system was built using the RTCP-net (Real-Time Coloured Petri net) formalism. The coverability graph of the model has 3077 states and 3986 edges, making the manual verification practically impossible. The coverability graph of the system was automatically translated, using the PetriNet2ModelChecker tool, into the AUT format of CADP. Four properties were specified as regular alternation-free mu-calculus formulas and checked on the model using the EVALUATOR tool of CADP, which provided useful feedback about the system.
The action-based setting proves to be useful for analyzing RTCP-nets.
By translating the coverability graph of a RTCP-net into the AUT
format of CADP, RTCP-nets modeled with CPN Tools can be automatically
verified with CADP. Combined with the state-based verification,
this approach allows for a comprehensive verification of any system
modelled with the RTCP-net formalism.
J. Biernacki, A. Biernacka and M. Szpyrka.
"Action-based Verification of RTCP-nets with CADP".
Proceedings of the International Conference of Computational Methods
in Sciences and Engineering ICCMSE'2015 (Athens, Greece), AIP
Conference Proceedings vol. 1702, March 2015.
Available on-line from http://www.researchgate.net/profile/Jerzy_Biernacki/publication/274077745_Action-based_verification_of_RTCP-nets_with_CADP/links/55152b080cf260a7cb2ec42a.pdf
and from the CADP Web site in PDF or PostScript
AGH University of Science and Technology
Department of Applied Computer Science
Al. Mickiewicza 30
Tel: +48 12 617 51 94
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|