Automatic safety analysis of computer-controlled plants |
| |
| Affiliation: | 1. Department of Computer Science, Loughborough University, Loughborough, Leicestershire LE11 3TU, UK;2. Department of Chemical Engineering, Process Control Laboratory, University of Dortmund, D-44221 Dortmund, Germany;1. The Helen L. and Martin S. Kimmel Center for Biology and Medicine at the Skirball Institute of Biomolecular Medicine, Molecular Neurobiology Program, and Department of Cell Biology, NYU Langone Medical Center, New York, NY 10016, USA;1. Key Laboratory of Flame Retardancy Finishing of Textile Materials (CNTAC), National Engineering Laboratory for Modern Silk, College of Textile and Clothing Engineering, Soochow University, 199 Renai Road, Suzhou 215123, China;2. Suzhou Taihu Snow Silk Co. Ltd., Zhenze Industrial Park, Suzhou 215231, China;1. Department of Industrial Engineering and Management System, University of Central Florida, Orlando, FL 32816, USA;2. George W. Woodruff School of Mechanical Engineering, Georgia Institute of Technology, Atlanta, GA 30332, USA;3. Daniel Guggenheim School of Aerospace Engineering, Georgia Institute of Technology, Atlanta, GA 30332, USA |
| |
| Abstract: | The paper describes an approach to apply the formal technique of model checking to the verification of logic controllers within the safety analysis of processing plants. In order to investigate plant safety in an early design phase in which only basic information is available, we set up plant and controller models in a qualitative and modular fashion. In a first step, the computer-controlled plant is partitioned into functional units, named modules, and the communication between different modules is represented graphically in a so-called process control event diagram (PCED). The PCED can be transformed into a formal model in which the behaviour of each module is described in terms of logical expressions for the modules’ input, state and output variables. Based on the formal model, the method of model checking can be applied to determine algorithmically whether the system fulfils a set of given safety requirements. Specifically, we use the tool symbolic model verifier (SMV) to determine whether the plant can reach states that are, in some sense, critical for the plant operation. The whole approach is illustrated by application to an industrial computer-controlled tube reactor. |
| |
| Keywords: | |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
