Verification of PLC programs written in FBD with VIS

Junbeom Yoo; Sungdeok Cha; Eunkyoung Jee

doi:10.5516/NET.2009.41.1.079

Verification of PLC programs written in FBD with VIS

Junbeom Yoo, Sungdeok Cha, Eunkyoung Jee

Department of Computer Science and Engineering

Research output: Contribution to journal › Article › peer-review

24 Citations (Scopus)

Abstract

Verification of programmable logic controller (PLC) programs written in IEC 61131-3 function block diagram (FBD) is essential in the transition from the use of traditional relay-based analog systems to PLC-based digital systems. This paper describes effective use of the well-known verification tool VIS for automatic verification of behavioral equivalences between successive FBD revisions. We formally defined FBD semantics as a state-transition system, developed semantic-preserving translation rules from FBD to Verilog prograins, implemented a software tool to support the process, and conducted a case study on a subset of FBDs for APR-1400 reactor protection system design.

Original language	English
Pages (from-to)	79-90
Number of pages	12
Journal	Nuclear Engineering and Technology
Volume	41
Issue number	1
DOIs	https://doi.org/10.5516/NET.2009.41.1.079
Publication status	Published - 2009 Feb

Keywords

Equivalence checking
Function block diagram
IEC-61131
Programmable logic controller
VIS
Verification
Verilog

ASJC Scopus subject areas

Nuclear Energy and Engineering

Access to Document

10.5516/NET.2009.41.1.079

Fingerprint Dive into the research topics of 'Verification of PLC programs written in FBD with VIS'. Together they form a unique fingerprint.

Cite this

@article{8a56015a68e94937b408cf23461049e1,

title = "Verification of PLC programs written in FBD with VIS",

abstract = "Verification of programmable logic controller (PLC) programs written in IEC 61131-3 function block diagram (FBD) is essential in the transition from the use of traditional relay-based analog systems to PLC-based digital systems. This paper describes effective use of the well-known verification tool VIS for automatic verification of behavioral equivalences between successive FBD revisions. We formally defined FBD semantics as a state-transition system, developed semantic-preserving translation rules from FBD to Verilog prograins, implemented a software tool to support the process, and conducted a case study on a subset of FBDs for APR-1400 reactor protection system design.",

keywords = "Equivalence checking, Function block diagram, IEC-61131, Programmable logic controller, VIS, Verification, Verilog",

author = "Junbeom Yoo and Sungdeok Cha and Eunkyoung Jee",

year = "2009",

month = feb,

doi = "10.5516/NET.2009.41.1.079",

language = "English",

volume = "41",

pages = "79--90",

journal = "Nuclear Engineering and Technology",

issn = "1738-5733",

publisher = "Korean Nuclear Society",

number = "1",

}

TY - JOUR

T1 - Verification of PLC programs written in FBD with VIS

AU - Yoo, Junbeom

AU - Cha, Sungdeok

AU - Jee, Eunkyoung

PY - 2009/2

Y1 - 2009/2

N2 - Verification of programmable logic controller (PLC) programs written in IEC 61131-3 function block diagram (FBD) is essential in the transition from the use of traditional relay-based analog systems to PLC-based digital systems. This paper describes effective use of the well-known verification tool VIS for automatic verification of behavioral equivalences between successive FBD revisions. We formally defined FBD semantics as a state-transition system, developed semantic-preserving translation rules from FBD to Verilog prograins, implemented a software tool to support the process, and conducted a case study on a subset of FBDs for APR-1400 reactor protection system design.

AB - Verification of programmable logic controller (PLC) programs written in IEC 61131-3 function block diagram (FBD) is essential in the transition from the use of traditional relay-based analog systems to PLC-based digital systems. This paper describes effective use of the well-known verification tool VIS for automatic verification of behavioral equivalences between successive FBD revisions. We formally defined FBD semantics as a state-transition system, developed semantic-preserving translation rules from FBD to Verilog prograins, implemented a software tool to support the process, and conducted a case study on a subset of FBDs for APR-1400 reactor protection system design.

KW - Equivalence checking

KW - Function block diagram

KW - IEC-61131

KW - Programmable logic controller

KW - VIS

KW - Verification

KW - Verilog

UR - http://www.scopus.com/inward/record.url?scp=62249114181&partnerID=8YFLogxK

U2 - 10.5516/NET.2009.41.1.079

DO - 10.5516/NET.2009.41.1.079

M3 - Article

AN - SCOPUS:62249114181

VL - 41

SP - 79

EP - 90

JO - Nuclear Engineering and Technology

JF - Nuclear Engineering and Technology

SN - 1738-5733

IS - 1

ER -

Verification of PLC programs written in FBD with VIS

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Cite this