Formal Modeling and Verification of the Safety Critical Fire-Fighting Control System

Published In

Computer Software and Applications Conference (COMPSAC), 2015 IEEE 39th Annual

Document Type


Publication Date



Machine theory, Emergency services, Fire extinction, Programmable controllers, Formal logic


A fire-fighting control system, which is usually implemented through programmable logic controllers, is a typical type of safety-critical cycle physical system. It has been widely used in currently complex industrial applications. So it is significant for a fire-fighting control system to conduct safety checking. There have been many methods to check safety of a fire-fighting control system so far, but they all ignore the effect of communication networks which are important for data transmission. In this paper, considering communication networks, we propose to model a fire-fighting control system with timed automata and describe system requirements with computation tree logic (CTL) formulas. A real dock fire fighting control system illustrates the method. And some safety properties are verified in the model checking tool Uppaal, and verified results show the effectiveness of the method.


© Copyright 2015 IEEE - All rights reserved.

Locate the Document

Researchers can access the work here:

Persistent Identifier