Symbolic Analysis of Programmable Logic Controllers

Author

Hehua Zhang ; Yu Jiang ; Hung, William N. N. ; Xiaoyu Song ; Ming Gu ; Jiaguang Sun

Author_Institution

Tsinghua Inf. Sci. & Technol. Nat. Lab., Tsinghua Univ., Beijing, China

Volume

63

Issue

10

fYear

2014

fDate

Oct. 2014

Firstpage

2563

Lastpage

2575

Abstract

Programmable Logic Controllers (PLC) are widely used in industry. The reliability of the PLC is vital to many critical applications. This paper presents a novel approach to the symbolic analysis of PLC systems. The approach includes, (1) calculating the uncertainty characterization of the PLC system, (2) abstracting the PLC system as a Hidden Markov Model, (3) solving the Hidden Markov Model with domain knowledge, (4) combining the solved Hidden Markov Model and the uncertainty characterization to form a regular Markov model, and (5) utilizing probabilistic model checking to analyze properties of the Markov model. This framework provides automated analysis of both uncertainty calculations and performance measurements, without the need for expensive simulations. A case study of an industrial, automated PLC system demonstrates the effectiveness of our work.

Keywords

formal verification; hidden Markov models; probability; programmable controllers; PLC reliability; PLC system symbolic analysis; PLC system uncertainty characterization; hidden Markov model; probabilistic model checking; programmable logic controller symbolic analysis; regular Markov model; Abstracts; Hidden Markov models; Markov processes; Probabilistic logic; Reliability; Syntactics; Uncertainty; Hidden Markov model; PLC; probabilistic analysis;

fLanguage

English

Journal_Title

Computers, IEEE Transactions on

Publisher

ieee

ISSN

0018-9340

Type

jour

DOI

10.1109/TC.2013.124

Filename

6532278