The Community for Technology Leaders
2014 IEEE International Conference on Information Reuse and Integration (IRI) (2014)
Redwood City, CA, USA
Aug. 13, 2014 to Aug. 15, 2014
ISBN: 978-1-4799-5880-1
pp: 500-507
Johanna Nellen , RWTH Aachen University, CS Department, 52056 Aachen, Germany
Erika Abraham , RWTH Aachen University, CS Department, 52056 Aachen, Germany
ABSTRACT
In this paper we address the safety analysis of chemical plants controlled by programmable logic controllers (PLCs). We consider sequential function charts (SFCs)for the programming of the PLCs, extended with the specification of the dynamic plant behavior. The resulting hybrid SFC models can be transformed to hybrid automata, opening the way to the application of advanced techniques for their reachability analysis. However, the hybrid automata models are often too large to be analyzed. To keep the size of the models moderate, we propose a counterexample-guided abstraction refinement (CEGAR) approach, which starts with the purely discrete SFC model of the controller and extends it with those parts of the dynamic behavior, which are relevant for proving or disproving safety.
INDEX TERMS
Automata, Reachability analysis, Reactive power, Analytical models, Valves, Algorithm design and analysis, Synchronization
CITATION

J. Nellen and E. Abraham, "A CEGAR approach for the reachability analysis of PLC-controlled chemical plants," 2014 IEEE International Conference on Information Reuse and Integration (IRI), Redwood City, CA, USA, 2014, pp. 500-507.
doi:10.1109/IRI.2014.7051930
239 ms
(Ver 3.3 (11022016))