Action-based Verification of a Fire Alarm System

Organisation:	AGH University of Science and Technology (POLAND)
Method:	RTCP-net
Tools used:	PetriNet2ModelChecker CADP (Construction and Analysis of Distributed Processes)
Domain:	Embedded Systems.
Period:	2015
Size:	3077 states and 3986 transitions.
Description:	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.
Conclusions:	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.
Publications:	[Biernacki-Biernacka-Szpyrka-15] 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
Contact:	Marcin Szpyrka AGH University of Science and Technology Department of Applied Computer Science Al. Mickiewicza 30 30-059 Krakow POLAND Tel: +48 12 617 51 94 Email: mszpyrka@agh.edu.pl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page