The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - May/June (2009 vol.26)
pp: 42-49
Junbeom Yoo , Konkuk University
Sungdeok (Steve) Cha , Korea University
ABSTRACT
Rigorous quality demonstration is important when developing safety-critical software such as a reactor protection system (RPS) for a nuclear power plant. Although using formal methods such as formal modeling and verification is strongly recommended, domain experts often reject formal methods for four reasons: there are too many candidate techniques, the notations appear complex, the tools often work only in isolation, and output is often too difficult for domain experts to understand. A formal-methods-based process that supports development, verification and validation, and safety analysis can help domain experts overcome these obstacles. Nuclear engineers can also use CASE tools to apply formal methods without having to know details of the underlying formalism. The authors spent more than seven years working with nuclear engineers in developing RPS software and applying formal methods. The engineers and regulatory personnel found the process effective and easy to apply with the integrated tool support.
INDEX TERMS
modeling, verification, safety-critical software, formal methods, function block diagram (FBD)
CITATION
Junbeom Yoo, Sungdeok (Steve) Cha, "Formal Modeling and Verification of Safety-Critical Software", IEEE Software, vol.26, no. 3, pp. 42-49, May/June 2009, doi:10.1109/MS.2009.67
REFERENCES
1. K.L. Heninger, "Specifying Software Requirements for Complex Systems: New Techniques and Their Application," IEEE Trans. Software Eng., vol. 6, no. 1, 1980, pp. 2–13.
2. J. Yoo et al., "A Formal Software Requirements Specification Method for Digital Nuclear Plants Protection Systems," J. Systems and Software, vol. 74, no. 1, 2005, pp. 73–83.
3. S. Cha, "Pet Formalisms versus Industry-Proven Sur—vivors: Issues on Formal Methods Education," J. Re-search and Practice in Information Technology, vol. 32, no. 1, 2000, pp. 39–46.
4. M.P.E. Heimdahl and N.G. Leveson, "Completeness and Consistency in Hierarchical State-Based Requirements," IEEE Trans. Software Eng., vol. 22, no. 6, 1996, pp. 363–377.
5. J. Yoo et al., "Synthesis of FBD-Based PLC Design from NuSCR Formal Specification," Reliability Eng. and System Safety, vol. 87, no. 2, 2005, pp. 287–294.
6. US Nat'l Research Council, Digital Instrumentation and Control Systems in Nuclear Power Plants: Safety and Reliability Issues, Nat'l Academy Press, 1997.
7. J. Cho, J. Yoo, and S. Cha, "NuEditor—a Tool Suite for Specification and Verification of NuSCR," Proc. 2nd ACIS Int'l Conf. Software Eng. Research, Management, and Applications (SERA 04), IEEE Press, 2004, pp. 298–304.
8. J. Yoo, S. Cha, and E. Jee, "A Verification Framework for FBD Based Software in Nuclear Power Plants," Proc. 15th Asia Pacific Software Eng. Conf., IEEE Press, 2008, pp. 385–392.
9. J. Yoo, S. Cha, and E. Jee, "Verification of PLC Programs Written in FBD with VIS," Nuclear Eng. and Technology, Feb. 2009.
10. T. Kim, J. Yoo, and S. Cha, "A Synthesis Method of Software Fault Tree from NuSCR Formal Specification Using Templates," J. Korea Inst. Information Scientists and Engineers, vol. 32, no. 12, 2005, pp. 1178–1192 (in Korean).
11. Y. Oh et al., "Software Safety Analysis of Function Block Diagrams Using Fault Trees," Reliability Eng. and System Safety, vol. 88, no. 3, 2005, pp. 215–228.
12. G.-Y. Park et al., "Fault Tree Analysis of KNICS RPS Software," Nuclear Eng. and Technology, vol. 40, no. 5, 2008, pp. 397–408.
5 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool