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 | |
| 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
Fingerprint Dive into the research topics of 'Verification of PLC programs written in FBD with VIS'. Together they form a unique fingerprint.
Cite this
Yoo, J., Cha, S., & Jee, E. (2009). Verification of PLC programs written in FBD with VIS. Nuclear Engineering and Technology, 41(1), 79-90. https://doi.org/10.5516/NET.2009.41.1.079