2014 IEEE International Conference on Information Reuse and Integration (IRI) (2014)
Redwood City, CA, USA
Aug. 13, 2014 to Aug. 15, 2014
Johanna Nellen , RWTH Aachen University, CS Department, 52056 Aachen, Germany
Erika Abraham , RWTH Aachen University, CS Department, 52056 Aachen, Germany
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.
Automata, Reachability analysis, Reactive power, Analytical models, Valves, Algorithm design and analysis, Synchronization
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.