FBDverifier: Interactive and visual analysis of counterexample in formal verification of function block diagram

Eunkyoung Jee, Seungjae Jeon, Sungdeok Cha, Kwangyong Koh, Junbeom Yoo, Geeyong Park, Poonghyun Seong

Research output: Contribution to journalArticle

16 Citations (Scopus)

Abstract

Model checking is often applied to verify safety-critical software implemented in programmable logic controller (PLC) language such as a function block diagram (FBD). Counter-examples generated by a model checker are often too lengthy and complex to analyze. This paper describes the FBDVerifier which allows domain experts to perform automated model checking and intuitive visual analysis of counter-examples without having to know technical details on temporal logic or the model checker. Once the FBD program is automatically translated into a semantically equivalent Verilog model and model checking is performed using SMV, users can enter various expressions to investigate why verification of certain properties failed. When applied to FBD programs implementing a shutdown system for a nuclear power plant, domain engineers were able to perform effective FBD verification and detect logical errors in the FBD design.

Original languageEnglish
Pages (from-to)171-188
Number of pages18
JournalJournal of Research and Practice in Information Technology
Volume42
Issue number3
Publication statusPublished - 2010 Aug 1

Keywords

  • Counter-example Visualization
  • Formal Verification
  • Function Block Diagram
  • Model Checking
  • Programmable Logic Controller
  • Verilog Translation

ASJC Scopus subject areas

  • Hardware and Architecture
  • Software
  • Computer Networks and Communications
  • Information Systems
  • Management Information Systems

Fingerprint Dive into the research topics of 'FBDverifier: Interactive and visual analysis of counterexample in formal verification of function block diagram'. Together they form a unique fingerprint.

  • Cite this