@inproceedings{41e528d878134600999fc37a30e94ae8,
title = "A formal verification method of function block diagrams with tool supporting: Practical experiences",
abstract = "Function Block Diagram (FBD) is a standard application programming language for the Programmable Logic Controller (PLC) and currently being used in the development of a fully-digitalized Reactor Protection System (RPS) under the Korea Nuclear Instrumentation & Control System (KNICS) project. Therefore, rigorous verification of the FBD programs is indispensible. In this paper, we propose a formal verification technique of FBD programs used in KNICS RPS and its supporting tool, FBDVerifier, which performs model checking and gives us counterexamples displayed in the form of timing graph to enhance their readability. Several important errors of FBD programs were found and reflected to the next version. Large scale case study showed that the proposed method is effective and practical.",
keywords = "Formal verification, Function block diagram (FBD), Model checking, Programmable logic controller (PLC)",
author = "Koh, {Kwang Young} and Jee, {Eun Kyoung} and Seungjae Jeon and Seong, {Poong Hyun} and Sungdeok Cha",
year = "2008",
language = "English",
isbn = "9783901509681",
series = "Annals of DAAAM and Proceedings of the International DAAAM Symposium",
publisher = "Danube Adria Association for Automation and Manufacturing, DAAAM",
pages = "713--714",
booktitle = "Annals of DAAAM for 2008 and Proceedings of the 19th International DAAAM Symposium {"}Intelligent Manufacturing and Automation",
note = "Annals of DAAAM for 2008 and 19th International DAAAM Symposium {"}Intelligent Manufacturing and Automation: Focus on Next Generation of Intelligent Systems and Solutions{"} ; Conference date: 22-10-2008 Through 25-10-2008",
}