Welcome to the InfoSci Platform
Reference Hub1
Safecharts Model Checking for the Verfication of Safety-Critical Systems

Safecharts Model Checking for the Verfication of Safety-Critical Systems

Pao-Ann. Hsiung, Yen-Hung Lin, Yean-Ru Chen
Copyright: © 2007 |Pages: 40
ISBN13: 9781591408512|ISBN10: 1591408512|ISBN13 Softcover: 9781591408529|EISBN13: 9781591408536
DOI: 10.4018/978-1-59140-851-2.ch014
Cite Chapter Cite Chapter

MLA

Hsiung, Pao-Ann., et al. "Safecharts Model Checking for the Verfication of Safety-Critical Systems." Verification, Validation and Testing in Software Engineering, edited by Aristides Dasso and Ana Funes, IGI Global, 2007, pp. 427-466. https://doi.org/10.4018/978-1-59140-851-2.ch014

APA

Hsiung, P., Lin, Y., & Chen, Y. (2007). Safecharts Model Checking for the Verfication of Safety-Critical Systems. In A. Dasso & A. Funes (Eds.), Verification, Validation and Testing in Software Engineering (pp. 427-466). IGI Global. https://doi.org/10.4018/978-1-59140-851-2.ch014

Chicago

Hsiung, Pao-Ann., Yen-Hung Lin, and Yean-Ru Chen. "Safecharts Model Checking for the Verfication of Safety-Critical Systems." In Verification, Validation and Testing in Software Engineering, edited by Aristides Dasso and Ana Funes, 427-466. Hershey, PA: IGI Global, 2007. https://doi.org/10.4018/978-1-59140-851-2.ch014

Export Reference

Mendeley
Favorite

Abstract

Unintentional design faults in safety-critical systems might result in injury or even death to human beings. However, the safety verification of such systems is getting very difficult because designs are becoming very complex. To cope with high design complexity, model-driven architecture (MDA) design is becoming a well-accepted trend. However, conventional methods of code testing and hazard analysis do not fit very well with MDA. To bridge this gap, we propose a safecharts model-based formal verification technique for safety-critical systems. The safety constraints in safecharts are mapped to semantic equivalents in timed automata. The theory for safety verification is proved and implemented in the SGM model checker. Prioritized and urgent transitions are implemented in SGM to model the safe chart risk semantics. Finally, it is shown that priority-based approach to mutual exclusion of resource usage in safecharts is unsafe and solutions are proposed. Application examples show the benefits of the proposed model-driven verification method.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.