.png){kind=icon}
Return
Applying Model Checking to Industrial-Sized PLC Programs
.png){kind=icon}
OA
AI
DOI：10.1109/TII.2015.2489184.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Programmable logic controllers (PLCs) are embedded computers widely used in industrial control systems. Ensuring that a PLC software complies with its specification is a challenging task. Formal verification has become a recommended practice to ensure the correctness of safety-critical software, but is still underused in industry due to the complexity of building and managing formal models of real applications. In this paper, we propose a general methodology to perform automated model checking of complex properties expressed in temporal logics [e.g., computation tree logic (CTL) and linear temporal logic (LTL)] on PLC programs. This methodology is based on an intermediate model (IM) meant to transform PLC programs written in various standard languages [structured text (ST), sequential function chart (SFC), etc.] to different modeling languages of verification tools. We present the syntax and semantics of the IM, and the transformation rules of the ST and SFC languages to the nuXmv model checker passing through the IM. Finally, two real cases studies of the European Organization for Nuclear Research (CERN) PLC programs, written mainly in the ST language, are presented to illustrate and validate the proposed approach.
Keywords:
Automata
IEC 61131
model checking
modeling
nuXmv
programmable logic controller (PLC)
verification
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
IF:
9.9
Papers:
8.6K
Citations:
6.0W
Organization
Cited Papers
.png){kind=icon}
ShareSaveShareSaveShareSaveShareSaveShareSave
View more