Two CEGAR-based approaches for the safety verification of PLC-controlled plants |
| |
Authors: | Johanna Nellen Kai Driessen Martin Neuhäußer Erika Ábrahám Benedikt Wolters |
| |
Affiliation: | 1.RWTH Aachen University,Aachen,Germany;2.Siemens AG,Nürnberg,Germany |
| |
Abstract: | In this paper we address the safety analysis of chemical plants controlled by programmable logic controllers (PLCs). We consider a specification of the control program of the PLCs, extended with the specification of the dynamic plant behavior. The resulting hybrid models can be transformed to hybrid automata, for which advanced techniques for reachability analysis exist. However, the hybrid automata models are often too large to be analyzed. We propose two counterexample-guided abstraction refinement (CEGAR) approaches to keep the size of the hybrid models moderate. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|