FBDVerifier: Interactive and Visual Analysis of Counter-example in Formal Verification of Function Block Diagram
- Authors
- Jee, Eunkyoung; Jeon, Seungjae; Cha, Sungdeok; Koh, Kwangyong; Yoo, Junbeom; Park, Geeyong; Seong, Poonghyun
- Issue Date
- 8월-2010
- Publisher
- AUSTRALIAN COMPUTER SOC INC
- Keywords
- Function Block Diagram; Formal Verification; Counter-example Visualization; Verilog Translation; Programmable Logic Controller; Model Checking
- Citation
- JOURNAL OF RESEARCH AND PRACTICE IN INFORMATION TECHNOLOGY, v.42, no.3, pp.171 - 188
- Indexed
- SCIE
SCOPUS
- Journal Title
- JOURNAL OF RESEARCH AND PRACTICE IN INFORMATION TECHNOLOGY
- Volume
- 42
- Number
- 3
- Start Page
- 171
- End Page
- 188
- URI
- https://scholar.korea.ac.kr/handle/2021.sw.korea/115987
- ISSN
- 1443-458X
- 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.
- Files in This Item
- There are no files associated with this item.
- Appears in
Collections - Graduate School > Department of Computer Science and Engineering > 1. Journal Articles
Items in ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.