Two CEGAR-based approaches for the safety verification of PLC-controlled plants

Johanna Nellen (), Kai Driessen (), Martin Neuhäußer (), Erika Ábrahám () and Benedikt Wolters ()
Additional contact information
Johanna Nellen: RWTH Aachen University
Kai Driessen: RWTH Aachen University
Martin Neuhäußer: Siemens AG
Erika Ábrahám: RWTH Aachen University
Benedikt Wolters: RWTH Aachen University

Information Systems Frontiers, 2016, vol. 18, issue 5, No 7, 927-952

Abstract: 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: Safety verification; Hybrid systems; CEGAR; Bounded model checking; Reachability analysis (search for similar items in EconPapers)
Date: 2016
References: View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
http://link.springer.com/10.1007/s10796-016-9671-9 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:infosf:v:18:y:2016:i:5:d:10.1007_s10796-016-9671-9

Ordering information: This journal article can be ordered from
http://www.springer.com/journal/10796

DOI: 10.1007/s10796-016-9671-9

Access Statistics for this article

Information Systems Frontiers is currently edited by Ram Ramesh and Raghav Rao

More articles in Information Systems Frontiers from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().