FBDVerifier: Interactive and Visual Analysis of Counter-example in Formal Verification of Function Block Diagram
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Jee, Eunkyoung | - |
dc.contributor.author | Jeon, Seungjae | - |
dc.contributor.author | Cha, Sungdeok | - |
dc.contributor.author | Koh, Kwangyong | - |
dc.contributor.author | Yoo, Junbeom | - |
dc.contributor.author | Park, Geeyong | - |
dc.contributor.author | Seong, Poonghyun | - |
dc.date.accessioned | 2021-09-08T01:18:10Z | - |
dc.date.available | 2021-09-08T01:18:10Z | - |
dc.date.created | 2021-06-14 | - |
dc.date.issued | 2010-08 | - |
dc.identifier.issn | 1443-458X | - |
dc.identifier.uri | https://scholar.korea.ac.kr/handle/2021.sw.korea/115987 | - |
dc.description.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. | - |
dc.language | English | - |
dc.language.iso | en | - |
dc.publisher | AUSTRALIAN COMPUTER SOC INC | - |
dc.title | FBDVerifier: Interactive and Visual Analysis of Counter-example in Formal Verification of Function Block Diagram | - |
dc.type | Article | - |
dc.contributor.affiliatedAuthor | Cha, Sungdeok | - |
dc.identifier.scopusid | 2-s2.0-78649513129 | - |
dc.identifier.wosid | 000286137700002 | - |
dc.identifier.bibliographicCitation | JOURNAL OF RESEARCH AND PRACTICE IN INFORMATION TECHNOLOGY, v.42, no.3, pp.171 - 188 | - |
dc.relation.isPartOf | JOURNAL OF RESEARCH AND PRACTICE IN INFORMATION TECHNOLOGY | - |
dc.citation.title | JOURNAL OF RESEARCH AND PRACTICE IN INFORMATION TECHNOLOGY | - |
dc.citation.volume | 42 | - |
dc.citation.number | 3 | - |
dc.citation.startPage | 171 | - |
dc.citation.endPage | 188 | - |
dc.type.rims | ART | - |
dc.type.docType | Editorial Material | - |
dc.description.journalClass | 1 | - |
dc.description.journalRegisteredClass | scie | - |
dc.description.journalRegisteredClass | scopus | - |
dc.relation.journalResearchArea | Computer Science | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Information Systems | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Software Engineering | - |
dc.subject.keywordAuthor | Function Block Diagram | - |
dc.subject.keywordAuthor | Formal Verification | - |
dc.subject.keywordAuthor | Counter-example Visualization | - |
dc.subject.keywordAuthor | Verilog Translation | - |
dc.subject.keywordAuthor | Programmable Logic Controller | - |
dc.subject.keywordAuthor | Model Checking | - |
Items in ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
(02841) 서울특별시 성북구 안암로 14502-3290-1114
COPYRIGHT © 2021 Korea University. All Rights Reserved.
Certain data included herein are derived from the © Web of Science of Clarivate Analytics. All rights reserved.
You may not copy or re-distribute this material in whole or in part without the prior written consent of Clarivate Analytics.