A formal verification method of function block diagrams with tool supporting: Practical experiences

Kwang Young Koh, Eun Kyoung Jee, Seungjae Jeon, Poong Hyun Seong, Sungdeok Cha

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

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.

Original languageEnglish
Title of host publicationAnnals of DAAAM and Proceedings of the International DAAAM Symposium
PublisherDanube Adria Association for Automation and Manufacturing, DAAAM
Pages713-714
Number of pages2
ISBN (Print)9783901509681
Publication statusPublished - 2008 Jan 1
EventAnnals of DAAAM for 2008 and 19th International DAAAM Symposium "Intelligent Manufacturing and Automation: Focus on Next Generation of Intelligent Systems and Solutions" - Trnava, Slovakia
Duration: 2008 Oct 222008 Oct 25

Other

OtherAnnals of DAAAM for 2008 and 19th International DAAAM Symposium "Intelligent Manufacturing and Automation: Focus on Next Generation of Intelligent Systems and Solutions"
CountrySlovakia
CityTrnava
Period08/10/2208/10/25

ASJC Scopus subject areas

  • Computer Science Applications
  • Control and Systems Engineering
  • Electrical and Electronic Engineering
  • Industrial and Manufacturing Engineering
  • Mechanical Engineering

Fingerprint Dive into the research topics of 'A formal verification method of function block diagrams with tool supporting: Practical experiences'. Together they form a unique fingerprint.

  • Cite this

    Koh, K. Y., Jee, E. K., Jeon, S., Seong, P. H., & Cha, S. (2008). A formal verification method of function block diagrams with tool supporting: Practical experiences. In Annals of DAAAM and Proceedings of the International DAAAM Symposium (pp. 713-714). Danube Adria Association for Automation and Manufacturing, DAAAM.