Nuclear Engineering and Technology

Korean Nuclear Society (한국원자력학회)
권호 표지
DOI QR코드

DOI QR Code

VERIFICATION OF PLC PROGRAMS WRITTEN IN FBD WITH VIS

  • Yoo, Jun-Beom (Konkuk University, Division of Computer Science and Engineering) ;
  • Cha, Sung-Deok (Korea University, Department of Computer Science and Engineering) ;
  • Jee, Eun-Kyung (KAIST, Department of Electrical Engineering and Computer Science)
  • Published : 2009.02.28
Download PDF
⟨ Previous Next ⟩

Abstract

Verification of programmable logic controller (PLC) programs written in IEC 61131-3 function block diagram (FBD) is essential in the transition from the use of traditional relay-based analog systems to PLC-based digital systems. This paper describes effective use of the well-known verification tool VIS for automatic verification of behavioral equivalences between successive FBD revisions. We formally defined FBD semantics as a state-transition system, developed semantic-preserving translation rules from FBD to Verilog programs, implemented a software tool to support the process, and conducted a case study on a subset of FBDs for APR-1400 reactor protection system design.

Keywords

References

  1. N.G. Leveson, SAFEWARE, System safety and Computers, Addison Wesley, 1995
  2. D.A. Peled, SOFTWARE RELIABILITY METHODS, Springer, 2001
  3. KNICS, Korea Nuclear Instrumentation & Control System R&D Center, http://www.knics.re.kr/
  4. J. Yoo, T. Kim, S. Cha, J.S. Lee, and H.S. Son, “A formal software requirements specification method for digital nuclear plants protection systems,” Journal of Systems and Software, 74, 1, pp.73-83, 2005 https://doi.org/10.1016/j.jss.2003.10.018
  5. NuSRS, http://dependable.kaist.ac.kr/~nusrs
  6. E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Trans. Programming Languages and Systems, 8, 2, pp.244–263, 1986 https://doi.org/10.1145/5397.5399
  7. J. Cho, J. Yoo, and S. Cha, “NuEditor - a tool suite for specification and verification of NuSCR,” SERA2004:Second ACIS International Conference on Software Engineering Research, Management and Applications, pp.298–304, 2004
  8. IEC, International standard for programmable controllers: Programming languages 61131- Part 3, 1993
  9. R.K. Brayton, G.D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.T. Cheng, S.A. Edwards, S.P. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R.K. Ranjan, S. Sarwary, T.R. Shiple, G. Swamy, and T. Villa, “VIS : A system for verification and synthesis,” the Eighth International Conference on Computer Aided Verification,” CAV '96, pp.428–432, 1996 https://doi.org/10.1007/3-540-61474-5_95
  10. D.E. Thomas and P.R. Moorby, The Verilog Hardware Description Language, Kluwer Academic Publishers, 1991
  11. E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking, MIT Press, 1999
  12. Cadence SMV, http://www.cadence.com
  13. S.J. Jeon, “Verification of Function Block Diagram through Verilog Translation,” Master’s thesis, Korea Advanced Institute of Science and Technology, 2007
  14. J. Yoo, E. Jee, and S. Cha, “A Verification framework for FBD based software in nuclear power plants,” The 15th Asian Pacific Software Engineering Conference (APSEC 2008), pp.385-392, 2008 https://doi.org/10.1109/APSEC.2008.26
  15. J. Yoo, Synthesis of Function Block Diagrams from NuSCR Formal Specification, Ph.D. thesis, Korea Advanced Institute of Science and Technology, 2005
  16. KAERI, SDS for reactor protection system, KNICS-RPSSDS101 Rev.00 Draft, Sept. 2003
  17. S. Cho, K. Koo, B. You, T.W. Kim, T. Shim, and J.S. Lee, “Development of the loader software for PLC programming,” Conference of the Institute of Electronics Engineers of Korea, pp.959–960, 2007
  18. S.T. Cheng and R.K. Brayton, “Compiling verilog into automata,” Tech. Rep. UCB/ERL M94/37, EECS Department, University of California, Berkeley, 1994
  19. KAERI, SRS for Reactor Protection System, KNICS-RPSSRS101 REV.00, Feb. 2003
  20. J. Yoo, S. Cha, C.H. Kim, and D.Y. Song, “Synthesis of FBD-based PLC design from NuSCR formal specification,” Reliability Engineering and System Safety, 87, 2, pp.287- 294, 2005 https://doi.org/10.1016/j.ress.2004.05.005
  21. G. Frey and L. Litz, “Formal moethods in PLC programming,” IEEE Conference in System Man and Cybernetics:SMC 2000, 2000 https://doi.org/10.1109/ICSMC.2000.884356
  22. L. Baresi, M. Mandrioli, S. Morasca, and M. Pezz`e, “Plctools: Design, formal verification, and code generation for programmable controllers,” the IEEE Conference on System, Man, and Cybernetics (SMC), Nashville, USA, pp.2437-2442, Oct. 2000 https://doi.org/10.1109/ICSMC.2000.884357
  23. B.J. Kramer and N. Volker, “A higher dependable computer architecture for safety critical control applications,” Real- Time Systems Journal, 13, 3, pp.237-251, 1997 https://doi.org/10.1023/A:1007959310351
  24. T. Nipkow, L.C. Paulson, and M. Wenzel, Isabelle/HOL - A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, Springer, 2002
  25. IEC, Function blocks - Part 1: Architecture (IEC 61499-1), 2005
  26. V. Vyatkin and H.M. Hanisch, “Modeling of IEC 61499 function blocks - a cue to their verification,” XI Workshop on Supervising and Diagnostics of Machining System, pp.59-68, 2000
  27. P.H. Starke, “Symmetries of signal-net systems,” Workshop on Concurrency, Specification and Programming, pp.285- 297, 2000
  28. P.H. Starke and S. Roch, “Tools for formal specification, verification, and validation of requirements,” the 12th Annual Conference on Computer Assurance, COMPASS ’97, pp.35- 47, 1997
  29. Bounded Model Checking for ANSI-C, http://www.cs.cmu. edu/~modelcheck/cbmc
  30. H. Jain, N. Sharygina, D. Kroening, and E. Clarke, “Word level predicate abstraction and refinement for verifying rtl verilog,” 42nd Design Automation Conference (DAC), 2005 https://doi.org/10.1145/1065579.1065697

Cited by

  1. Formal Modeling and Verification of Safety-Critical Software vol.26, pp.3, 2009, https://doi.org/10.1109/MS.2009.67