This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Modeling and Verification of Safety-Critical Software
May/June 2009 (vol. 26 no. 3)
pp. 42-49
ASCII Text
x 
 
Junbeom Yoo, Eunkyoung Jee, Sungdeok (Steve) Cha, "Formal Modeling and Verification of Safety-Critical Software," IEEE Software, vol. 26, no. 3, pp. 42-49, May/June, 2009.
 
 
BibTex
x
 
@article{ 10.1109/MS.2009.67,
author = {Junbeom Yoo and Eunkyoung Jee and Sungdeok (Steve) Cha},
title = {Formal Modeling and Verification of Safety-Critical Software},
journal ={IEEE Software},
volume = {26},
number = {3},
issn = {0740-7459},
year = {2009},
pages = {42-49},
doi = {http://doi.ieeecomputersociety.org/10.1109/MS.2009.67},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - MGZN
JO - IEEE Software
TI - Formal Modeling and Verification of Safety-Critical Software
IS - 3
SN - 0740-7459
SP42
EP49
EPD - 42-49
A1 - Junbeom Yoo,
A1 - Eunkyoung Jee,
A1 - Sungdeok (Steve) Cha,
PY - 2009
KW - modeling
KW - verification
KW - safety-critical software
KW - formal methods
KW - function block diagram (FBD)
VL - 26
JA - IEEE Software
ER -
 
Junbeom Yoo, Konkuk University
Eunkyoung Jee, Korea Advanced Institute of Science and Technology
Sungdeok (Steve) Cha, Korea University
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.

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.

Index Terms:
modeling, verification, safety-critical software, formal methods, function block diagram (FBD)
Citation:
Junbeom Yoo, Eunkyoung Jee, 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
Usage of this product signifies your acceptance of the Terms of Use.