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
DOIs
Publication statusPublished - 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