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

Leveson, 1995 I. IEC, 61131-3. Programmable controllers-part 3: programming languages, International Standard, Second Edition, International Electrotechnical Commission, Geneva, vol. 1; 2003. I. IEC, IEC 61508: Functional safety of electrical, electronic and programmable electronic (E/E/PE) safety-related systems, International Standard, Second Edition, International Electrotechnical Commission, Geneva, vol. 1; 2003. Areva, last accessed: Jan/4/2013 〈http://www.areva.com〉. invensys, last accessed: Jan/4/2013 〈http://iom.invensys.com〉. Posco ict, last accessed: Jan/4/2013 〈http://www.poscoict.co.kr〉. SIEMENS, SPACE, Engineering system of Teleperm XS PLC, Technical Report. KWU NLL1-1026-76-V1.0/11.96, Germany, last accessed: Jan/4/2013; 1996. SIEMENS, Teleperm xs, brief description, Technical Report. KWU NLL1-1004-76-V2.2/04.98, Germany; 1998. Richter, 2003, Verification and validation process for safety I&C systems, Nuclear Plant Journal, 21, 36 Istec: Industrielle software-technik gmbh, last accessed: Jan/4/2013 〈http://www.istec.de〉. iSTec, RETRANS, institute for safety technology, last accessed: Jan/4/2013 〈http://www.istec-gmbh.de/leistungen/qualifizierung/produkte〉. Safety software suite, last accessed: Jan/4/2013 〈http://iom.invensys.com/〉. KNICS, Korea nuclear instrumentation and control system r&d center, last accessed: Jan/1/2010 〈http://www.knics.re.kr/english/eindex.html〉. Cho S, Koo K, You B, Kim T.-W, Shim T, Lee JS. Development of the loader software for PLC programming. In: Proceedings of conference of the institute of electronics engineers of Korea, vol. 30; 2007. p. 995–60. Wikipedia, Nuclear power in South Korea, last accessed: Jan/4/2013 [〈http://en.wikipedia.org/wiki/Nuclear_power_in_South_Korea〉]. Clarke, 1999 Clarke E, Kroening D. Hardware verification using ANSI-C programs as a reference. In: Design automation conference, 2003. Proceedings of the ASP-DAC 2003. Asia and South Pacific, IEEE; 2003. p. 308–11. Yoo, 2009, Verification of PLC programs written in FBD with VIS, Nuclear Engineering and Technology, 41, 79, 10.5516/NET.2009.41.1.079 Brayton R, Hachtel G, Sangiovanni-Vincentelli A, Somenzi F, Aziz A, Cheng S, et al. Vis: a system for verification and synthesis. In: Computer aided verification. Springer; 1996. p. 428–32. Sommerville, 2007 Heitmeyer, 1996, Automated consistency checking of requirements specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), 5, 231, 10.1145/234426.234431 Yoo, 2005, A formal software requirements specification method for digital nuclear plant protection systems, Journal of Systems and Software, 74, 73, 10.1016/j.jss.2003.10.018 Yoo, 2009, Formal modeling and verification of safety-critical software, IEEE Software, 26, 42, 10.1109/MS.2009.67 TEXAS INSTRUMENTS, TMS320C55x Optimizing C/C++ Compiler User Guide; 2003. AREVA, Teleperm xs system overview, Online, last accessed: Jan/4/2013 〈http://de.areva.com/EN/customer-397/teleperm-xs-system-overview.html〉. Pezzè, 2008 I. Rational, Rational rhapsody, last accessed: Jan/4/2013 〈http://www-01.ibm.com/software/awdtools/rhapsody/〉. Lee, 2011, Equivalence checking between function block diagrams and C programs using HW-CBMC, Computer Safety, Reliability, and Security, 397, 10.1007/978-3-642-24270-0_29 Huang, 1998 IEC/IEEE behavioural languages—part 4: Verilog hardware description language (adoption of IEEE STD 1364-2001), IEC 61691-4 First edition 2004-10; IEEE 1364 (2004) 0–860. Jee, 2010, FBDVerifier, Journal of Research and Practice in Information Technology, 42, 171 PLCopen for efficiency in automation, last accessed: Jan/4/2013 〈http://www.plcopen.org〉. Yoo J, Lee J, Jeong S, Cha S. FBDtoVerilog: a vendor-independent translation from fbds into verilog programs. In: The twenty-third international conference on software engineering and knowledge engineering (SEKE 2011); 2010. p. 48–51. Cimatti, 1999, Nusmv, vol. 1644, 495 Lee D-A, Yoo J. pSET2TC6: a translation tool to standardize the output format of pSET. In: Korean institute of information scientists and engineers (KIISE) 2011, vol. 38; 2011. p. 105–7. Bombieri N, Fummi F, Pravadelli G, Marques-Silva J. Towards equivalence checking between TLM and RTL models. In: Fifth IEEE/ACM international conference on formal methods and models for codesign, 2007. MEMOCODE 2007, IEEE; 2007. p. 113–22. Hoare, 2003, The verifying compiler, Modular Programming Languages, 25, 10.1007/978-3-540-45213-3_4 Dave, 2003, Compiler verification, ACM SIGSOFT Software Engineering Notes, 28, 10.1145/966221.966235 Staats, 2008, Partial translation verification for untrusted code-generators, Formal Methods and Software Engineering, 226, 10.1007/978-3-540-88194-0_15 Dold, 2001, A mechanically verified compiling specification for a lisp compiler, FST TCS 2001, 144 S. Blazy, Z. Dargaye, X. Leroy, Formal verificationof a C compiler front-end, FM 2006: Formal Methods 2006: 460–75.