Database of Case Studies Achieved Using CADP

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
and from the VASY FTP site in PDF or PostScript
Marcin Szpyrka
AGH University of Science and Technology
Department of Applied Computer Science
Al. Mickiewicza 30
30-059 Krakow
Tel: +48 12 617 51 94

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Fri Jun 30 16:50:13 2017.

Back to the CADP case studies page