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 |
| Publication status | Published - 2009 Feb 1 |
Fingerprint
Keywords
- Equivalence checking
- Function block diagram
- IEC-61131
- Programmable logic controller
- Verification
- Verilog
- VIS
ASJC Scopus subject areas
- Nuclear Energy and Engineering
Cite this
Verification of PLC programs written in FBD with VIS. / Yoo, Junbeom; Cha, Sungdeok; Jee, Eunkyoung.
In: Nuclear Engineering and Technology, Vol. 41, No. 1, 01.02.2009, p. 79-90.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - Verification of PLC programs written in FBD with VIS
AU - Yoo, Junbeom
AU - Cha, Sungdeok
AU - Jee, Eunkyoung
PY - 2009/2/1
Y1 - 2009/2/1
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 - Verification
KW - Verilog
KW - VIS
UR - http://www.scopus.com/inward/record.url?scp=62249114181&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=62249114181&partnerID=8YFLogxK
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 -