安全攸關系統是指當系統失效或誤動作，將可能導致生命損失的系統，例如汽車，飛機，交通號誌系統皆為安全攸關系統。為了避免因安全攸關系統失效，而引起嚴重的事故，可靠性分析對於安全攸關系統是非常重要的。安全工程師可以參考可靠度分析結果來獲得系統的關鍵元件，並在此些關鍵元件上增加適當的保護機制。

傳統上，可靠性分析由安全工程師以人工並搭配故障樹軟體半自動完成。對於安全關鍵系統而言，可靠性分析需依據故障注入產生的故障結果建立分析。透過故障注入技術，使得系統內的元件失效，並觀察是元件的失效事件是否對系統有所影響。然而，傳統的故障注入技術需要仰賴安全工程師的經驗，才可能將失效模式完整考量。由於系統非常龐大，就算有經驗的工程師，可能還是會忽略些許故障行為，導致安全工程師建立不正確的分析。

在本論文中，我們提出了一種利用模型驗證來辨識系統關鍵元件的方法。安全工程師可以使用此流程，透過模型驗證的特性，完整地實現故障注入技術。最後依據注入後的系統的狀態空間的特性建立可靠性框架圖，並使用布林邏輯簡化獲得系統的關鍵元件。

Safety-critical systems are those systems whose failure could result in loss of life such as car, airplane, traffic light system.
Reliability analysis is necessary to avoid accidents caused by safety critical system failures.
Safety engineer can refer to the analysis results to identify critical components of the system and add appropriate protection mechanisms.

Traditionally, reliability analysis is done semi-automatically by security engineers with specific software.
Reliability analysis of safety-critical systems requires the combination of failure results derived from fault injection.
It is necessary for reliability analysis to use fault injection technology to fail the system components and observe whether it affects the system.
However, the traditional fault injection technology relies on the experience of safety engineers, which may lead to many fault behaviors being ignored, and finally establishing incorrect analysis results.

In this paper, we propose a method for extracting the critical components which makes use of model checking.
Safety engineers can use this approach to achieve complete fault injection techniques and obtain critical components of the system according to the characteristics of state space.

[1] Jean Arlat, Martine Aguera, Louis Amat, Yves Crouzet, J-C Fabre, J-C Laprie, Eliane Martins, and David Powell. Fault injection for dependability validation: A methodology and some applications. IEEE Transactions on software engineering, 16(2):166–182, 1990.
[2] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.
[3] Richard E Barlow and Frank Proschan. Importance of system components and fault tree events. Stochastic Processes and their applications, 3(2):153–173, 1975.
[4] F Bessayah. Une Approche Complémentaire de Test de Robustesse Basée sur lȷInjection de Fautes et le Test Passif. PhD thesis, Thèse de doctorat, Télécom & Management SudParis, 2010.
[5] Fayçal Bessayah, Ana Cavalli, and Eliane Martins. A formal approach for specification and verification of fault injection process. In Proceedings of the 2nd International Conference on Interaction Sciences: Information Technology, Culture and Human, pages 883–890. ACM, 2009.
[6] Michael C. Browne, Edmund M. Clarke, and Orna Grumberg. Characterizing finite kripke structures in propositional temporal logic. Theor. Comput. Sci., 59(1/2):115–131, 1988.
[7] Jin-Fu Chen, Yan-Sheng Lu, and Xiao-Dong Xie. Research on software fault injection testing. Journal of Software, 6:007, 2009.
[8] PL Clemens. Event tree analysis. JE Jacobs Sverdrup,, 2002.
[9] Elena Dubrova. Fault-tolerant design. Springer, 2013.
[10] E Allen Emerson and Joseph Y Halpern. “sometimes”and“not never”revisited: on branching versus linear time temporal logic. Journal of the ACM (JACM), 33(1):151–178, 1986.
[11] Jonathan Ezekiel and Alessio Lomuscio. Combining fault injection and model checking to verify fault tolerance in multi-agent systems. In Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems-Volume 1, pages 113–120. International Foundation for Autonomous Agents and Multiagent Systems, 2009.
[12] Nasser S Fard. Determination of minimal cut sets of a complex fault tree. Computers & industrial engineering, 33(1-2):59–62, 1997.
[13] Lars Grunske, Robert Colvin, and Kirsten Winter. Probabilistic model-checking support for fmea. In Quantitative Evaluation of Systems, 2007. QEST 2007. Fourth International Conference on the, pages 119–128. IEEE, 2007.
[14] Haitao Guo and Xianhui Yang. A simple reliability block diagram method for safety integrity verification. Reliability Engineering & System Safety, 92(9):1267–1273, 2007.
[15] Luke Thomas Herbert and Robin Sharp. Workflow fault tree generation through model checking. In 22nd ESREL conference, pages 2229–2236. CRC Press LLC, 2014.
[16] Pao-Ann Hsiung, Yean-Ru Chen, and Yen-Hung Lin. Model checking safety-critical systems using safecharts. IEEE Transactions on Computers, (5):692–705, 2007.
[17] Mei-Chen Hsueh, Timothy K Tsai, and Ravishankar K Iyer. Fault injection techniques and tools. Computer, 30(4):75–82, 1997.
[18] Anjali Joshi and Mats PE Heimdahl. Model-based safety analysis of simulink models using scade design verifier. In International Conference on Computer Safety, Reliability, and Security, pages 122–135. Springer, 2005.
[19] Anjali Joshi and Mats PE Heimdahl. Behavioral fault modeling for model-based safety analysis. In High
ssurance Systems Engineering Symposium, 2007. HASE’07. 10th IEEE, pages 199–208. IEEE, 2007.
[20] Sohag Kabir. An overview of fault tree analysis and its application in model based dependability analysis. Expert Systems with Applications, 77:114–135, 2017.
[21] Howard E Lambert. Use of fault tree analysis for automotive reliability and safety analysis. Technical report, SAE Technical Paper, 2004.
[22] Chien-tsug Lu, Michael Wetmore, and Robert Przetak. Another approach to enhance airline safety: Using management safety tools. 2006.
[23] Robin McDermott, Raymond J Mikulak, and Michael Beauregard. The basics of FMEA. SteinerBooks, 1996.
[24] Aureli Munoz, Sebastián Martorell, and Vicente Serradell. Genetic algorithms in optimizing surveillance and maintenance of components. Reliability Engineering & System Safety, 57(2):107–120, 1997.
[25] Kevin Ni, Nithya Ramanathan, Mohamed Nabil Hajj Chehade, Laura Balzano, Sheela Nair, Sadaf Zahedi, Eddie Kohler, Greg Pottie, Mark Hansen, and Mani Srivastava.
Sensor network data fault types. ACM Transactions on Sensor Networks (TOSN), 5(3):25, 2009.
[26] Nimal Nissanke and Hamdan Z Dammag. Risk bands-a novel feature of safecharts. In Software Reliability Engineering, 2000. ISSRE 2000. Proceedings. 11th International Symposium on, pages 293–301. IEEE, 2000.
[27] Frank Ortmeier, Matthias Güdemann, and Wolfgang Reif. Formal failure models. IFAC Proceedings Volumes, 40(6):145–150, 2007.
[28] Gabriel Petrica, Ionut-Daniel Barbu, Sabina-Daniela Axinte, and Cristian Pascariu. Reliability analysis of a web server by fta method. In Advanced Topics in lectrical Engineering (ATEE), 2017 10th International Symposium on, pages 683–686. IEEE, 2017.
[29] Roberta Piscitelli, Shivam Bhasin, and Francesco Regazzoni. Fault attacks, injection techniques and tools for simulation. In Hardware Security and Trust, pages 27–47.Springer, 2017.
[30] Vesely W. Dugan J. Fragola J. Minarick J. Railsback J Stamatelatos, M. Fault tree handbook with aerospace. Technical report, NASA, 2002.
[31] William E Vesely, Francine F Goldberg, Norman H Roberts, and David F Haasl. Fault tree handbook. Technical report, Nuclear Regulatory Commission ashington DC,1981.
[32] Haissam Ziade, Rafic A Ayoubi, Raoul Velazco, et al. A survey on fault injection techniques. Int. Arab J. Inf. Technol., 1(2):171–186, 2004.