Verification of PLC programs written in FBD with VIS

Junbeom Yoo, Sungdeok Cha, Eunkyoung Jee

Research output: Contribution to journalArticle

21 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 languageEnglish
Pages (from-to)79-90
Number of pages12
JournalNuclear Engineering and Technology
Volume41
Issue number1
Publication statusPublished - 2009 Feb 1

Fingerprint

Programmable logic controllers
Semantics
Computer hardware description languages
Systems analysis

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 journalArticle

Yoo, Junbeom ; Cha, Sungdeok ; Jee, Eunkyoung. / Verification of PLC programs written in FBD with VIS. In: Nuclear Engineering and Technology. 2009 ; Vol. 41, No. 1. pp. 79-90.
@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, Verification, Verilog, VIS",
author = "Junbeom Yoo and Sungdeok Cha and Eunkyoung Jee",
year = "2009",
month = "2",
day = "1",
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/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 -