Paper Info
Title
FBDVerifier: Interactive and Visual Analysis of Counterexample in Formal Verification of Function Block Diagram.
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.
Year
Venue
Keywords
2010
JOURNAL OF RESEARCH AND PRACTICE IN INFORMATION TECHNOLOGY
Function Block Diagram,Formal Verification,Counter-example Visualization,Verilog Translation,Programmable Logic Controller,Model Checking
Field
DocType
Volume
Programming language,Model checking,Expression (mathematics),Computer science,Software,Programmable logic controller,Function block diagram,Temporal logic,Verilog,Formal verification
Journal
42
Issue
ISSN
Citations 
3
1443-458X
11
PageRank 
References 
Authors
1.01
5
7
Name
Order
Citations
PageRank
Eunkyoung Jee121317.57
Seungjae Jeon2141.62
Sung Deok Cha338129.92
Kwang Yong Koh4183.62
Junbeom Yoo514319.86
Gee-Yong Park6152.31
Poong-hyun Seong711524.53