A systematic verification of behavioral consistency between FBD design and ANSI-C implementation using HW-CBMC

Dong-Ah Lee, Junbeom Yoo and Jang-Soo Lee

Reliability Engineering and System Safety, 2013, vol. 120, issue C, 139-149

Abstract: Controllers in safety critical systems such as nuclear power plants often use the Function Block Diagram (FBD) to design software embedded in the PLC (Programmable Logic Controller). Software engineers develop FBD programs manually, while engineering tools provided by PLC vendors translate them into ANSI-C programs mechanically. Every new PLC and its software engineering tool should demonstrate the so-called FBD-to-C translator's correctness thoroughly. This paper proposes a verification process which can efficiently verify the translator's correctness using the model checking technique. The HW-CBMC model checker verifies the behavioral consistency between FBD and ANSI-C programs formally according to the process and templates which this paper proposes. We also developed a CASE tool ‘CWrapper’ and performed a case study with simplified examples of the APR-1400 (Advanced Power Reactor-1400) nuclear reactor protection system in Korea.

Keywords: Verification process; Behavioral consistency; Model checking; FBD; ANSI-C; HW-CBMC (search for similar items in EconPapers)
Date: 2013
References: View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
http://www.sciencedirect.com/science/article/pii/S0951832013001713
Full text for ScienceDirect subscribers only

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:eee:reensy:v:120:y:2013:i:c:p:139-149

DOI: 10.1016/j.ress.2013.06.006

Access Statistics for this article

Reliability Engineering and System Safety is currently edited by Carlos Guedes Soares

More articles in Reliability Engineering and System Safety from Elsevier
Bibliographic data for series maintained by Catherine Liu ().