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

Citation

Publication Date

7-2015

Subjects

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

Abstract

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.

Description

© Copyright 2015 IEEE - All rights reserved.

Locate the Document

Researchers can access the work here: http://dx.doi.org/10.1109/COMPSAC.2015.181

Persistent Identifier

http://archives.pdx.edu/ds/psu/20912

Share

COinS