Formal Modeling and Verification of the Safety Critical Fire-Fighting Control System
This research is supported by NSFC(61373034, 613030 14),ISTCP(2011DFG13000,2010DFB10930),TJSHG (2013 10028014),KM(201510028015) and No.IDHT20150507.
Computer Software and Applications Conference (COMPSAC), 2015 IEEE 39th Annual
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.
Locate the Document
Researchers can access the work here: http://dx.doi.org/10.1109/COMPSAC.2015.181
Wang, Ya, Rui Wang, Yong Guan, Xiaojuan Li, Jie Zhang, Hongxing Wei, and Xiaoyu Song. "Formal Modeling and Verification of the Safety Critical Fire-Fighting Control System." In Computer Software and Applications Conference (COMPSAC), 2015 IEEE 39th Annual, vol. 3, pp. 536-541. IEEE, 2015.