科技快速的發展下，系統越來越複雜，而安全性一直是人們最關注的議題之一。
安全攸關系統處處可見，隨時都可能運用到，從大眾交通工具到交通號誌，這類系統都屬於安全攸關系統，一旦系統失效將可能使人們暴露於危險當中。系統失效的根本原因來自內部元件的故障、錯誤，在沒有防範、容錯機制的運用下，系統很難避免因故障、錯誤而導致的系統失效。透過這些安全機制的運用，將可以使系統失效的機率降為最低。
為了檢驗系統，我們探討系統中常出現的故障種類，將這些故障的關係模型化；使用客製化的防範機制，探討防範機制是否真的能達到作用；為了使系統的安全性更加提升，避免在未知情況下引發無法預期的錯誤，造成系統帶來的危害，因此加入容錯機制，建立出容錯模型，使得安全分析師分析時能有所依據。而受惠於現在驗證工具的完整與嚴謹性，我們使用正規驗證的工具- PRISM 機率模型驗證器，藉由此工具可以詳盡的檢驗完整個系統所有可能發生的狀態轉換，確認系統發生故障的緣故；且PRISM 附有機率的模型功能，我們可以透過此機率模型驗證工具檢測出使用安全機制後的成效，分析使用安全機制後，降低系統失效的幅度為何。

With the progress of the times, science and technology change rapidly, the complexity of the system is getting higher and higher. The issue of safety has always been one of the most concerned topics. Safety-critical systems can be found everywhere, from time to time, from mass transit to traffic signs. These systems are safety-critical systems that can expose people to danger if they got failure. The root cause of system failure comes from faults and errors of internal components. When a fault occurs, it is difficult for the system to continue its function without the prevention and fault tolerance mechanism. Through the use of these safety mechanisms, the chances of system failure will be minimized.
In order to verify the safety of the system, we explore the types of faults that often occur in the safety-critical system and model the relationship of these faults. Using a customized prevention mechanisms for those faults and exploring whether the prevention mechanism can really achieve its effect. To improve the safety of the system, avoid system failures caused by unforeseen errors, the fault tolerance mechanism is added to establish a fault-tolerant model, which makes the safety analysts have a basis for analysis. Thanks to the completeness and rigor of the current verification tool, we use the formal verification tool - PRISM probabilistic model checker, which can thoroughly verify all possible state transitions of the entire system and confirm the cause of the system failure. Through the probability function of PRISM, we can use this model checker to calculate the effectiveness of using the safety mechanism, and analyze the use of safety mechanisms to reduce the extent of system failure.

[1] A. Avižienis, J.C. Laprie, B. Randell, and University of Newcastle upon Tyne. Computing
Science. Fundamental Concepts of Dependability. Technical report series. University
of Newcastle upon Tyne, Computing Science, 2001.
[2] Algirdas Avizienis, J-C Laprie, Brian Randell, and Carl Landwehr. Basic concepts and
taxonomy of dependable and secure computing. IEEE transactions on dependable and
secure computing, 1(1):11–33, 2004.
[3] Algirdas Avizienis, Jean-Claude Laprie, and Brian Randell. Fundamental concepts of
computer system dependability. In Workshop on Robot Dependability: Technological
Challenge of Dependable Robots in Human Environments, pages 1–16, 2001.
[4] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.
[5] Meenakshi Bheevgade and Rajendra M Patrikar. Implementation of watch dog timer
for fault tolerant computing on cluster server. World Academy of Science, Engineering
and Technology, 38:265–268, 2008.
[6] Yean-Ru Chen, Pao-Ann Hsiung, and Sao-Jie Chen. Modeling and automatic failure
analysis of safety-critical systems using extended safecharts. In International Conference
on Computer Safety, Reliability, and Security, pages 451–464. Springer, 2007.
[7] Abraham Cherfi, Michel Leeman, Florent Meurville, and Antoine Rauzy. Modeling automotive
safety mechanisms: A markovian approach. Reliability Engineering & System
Safety, 130:42–49, 2014.
[8] Edmund M Clarke, Orna Grumberg, and Doron Peled. Model checking. MIT press,
1999.
[9] David E Culler, Jaswinder Pal Singh, and Anoop Gupta. Parallel computer architecture:
a hardware/software approach. Gulf Professional Publishing, 1999.
[10] Edsger W Dijkstra. An assertional proof of a program by fGL Petersong. 1981.
[11] Ana Gainaru and Franck Cappello. Errors and Faults, pages 89–144. Springer International
Publishing, Cham, 2015.
[12] Walter Heimerdinger and Charles Weinstock. A conceptual framework for system
fault tolerance. Technical Report CMU/SEI-92-TR-033, Software Engineering Institute,
Carnegie Mellon University, Pittsburgh, PA, 1992.
[13] Alex Ho, Steven Smith, and Steven Hand. On deadlock, livelock, and forward progress.
Technical report, University of Cambridge, Computer Laboratory, 2005.
[14] Micha Hofri. Proof of a mutual exclusion algorithm—a classic example. ACM SIGOPS
Operating Systems Review, 24(1):18–22, 1990.
[15] Roberto Horowitz and Pravin Varaiya. Control design of an automated highway system.
Proceedings of the IEEE, 88(7):913–925, 2000.
[16] Ashok D Ingle and Daniel P Siewiorek. A reliability model for various switch designs
in hybrid redundancy. IEEE Transactions on Computers, 100(2):115–133, 1976.
[17] Bernhard Kaiser, Catharina Gramlich, and Marc Förster. State/event fault trees—a
safety analysis model for software-controlled systems. Reliability Engineering & System
Safety, 92(11):1521–1537, 2007.
[18] Hyunki Kim, Hyung-Joon Jeon, Keyseo Lee, and Hyuntae Lee. The design and evaluation
of all voting triple modular redundancy system. In Reliability and Maintainability
Symposium, 2002. Proceedings. Annual, pages 439–444. IEEE, 2002.
[19] Man Ho Kim, Suk Lee, and Kyung Chang Lee. Kalman predictive redundancy system
for fault tolerance of safety-critical systems. IEEE Transactions on Industrial Informatics,
6(1):46–53, 2010.
[20] Heba Kurdi, Ebtesam Aloboud, Sarah Alhassan, and Ebtehal T Alotaibi. An algorithm
for handling starvation and resource rejection in public clouds. Procedia Computer
Science, 34:242–248, 2014.
[21] J. C. Laprie. Dependability: Basic Concepts and Terminology, pages 3–245. Springer
Vienna, Vienna, 1992.
[22] Jaehwan Lee and Vincent John Mooney III. A novel deadlock avoidance algorithm
and its hardware implementation. In Proceedings of the 2nd IEEE/ACM/IFIP international
conference on Hardware/software codesign and system synthesis, pages 200–205.
ACM, 2004.
[23] John Lygeros, Datta N Godbole, and Mireille E Broucke. Design of an extended architecture
for degraded modes of operation of ivhs. In American Control Conference,
Proceedings of the 1995, volume 5, pages 3592–3596. IEEE, 1995.
[24] Mathilde Machin, Fanny Dufossé, Jean-Paul Blanquart, Jérémie Guiochet, David Powell,
and Hélène Waeselynck. Specifying safety monitors for autonomous systems using
model-checking. In International Conference on Computer Safety, Reliability, and Security,
pages 262–277. Springer, 2014.
[25] Thomas Maier. Fmea and fta to support safe design of embedded software in safetycritical
systems. In Safety and reliability of software based systems, pages 351–367.
Springer, 1997.
[26] Milo MK Martin, Daniel J Sorin, Bradford M Beckmann, Michael R Marty, Min Xu,
Alaa R Alameldeen, Kevin E Moore, Mark D Hill, and David A Wood. Multifacet’s
general execution-driven multiprocessor simulator (gems) toolset. ACM SIGARCH
Computer Architecture News, 33(4):92–99, 2005.
[27] Sebastian Müller and Peter Liggesmeyer. Dynamic safety contracts for functional cooperation
of automotive systems. In International Conference on Computer Safety,
Reliability, and Security, pages 171–182. Springer, 2016.
[28] Victor P Nelson. Fault-tolerant computing: Fundamental concepts. Computer,
23(7):19–25, 1990.
[29] Behrooz Parhami. Defect, fault, error,..., or failure? IEEE Transactions on Reliability,
46(4):450–451, 1997.
[30] Gary L. Peterson. Myths about the mutual exclusion problem. Information Processing
Letters, 12:115–116, 1981.
[31] Ishwari Singh Rajput and Deepa Gupta. A priority based round robin cpu scheduling
algorithm for real time systems. International Journal of Innovations in Engineering
and Technology, 1(3):1–11, 2012.
[32] A. Silberschatz, P.B. Galvin, and G. Gagne. Operating System Concepts, 9th Edition.
Wiley Global Education, 2012.
[33] Kuo-Chung Tai Kuo-Chung Tai. Definitions and detection of deadlock, livelock, and
starvation in concurrent programs. In Parallel Processing, 1994. ICPP 1994 Volume 2.
International Conference on, volume 2, pages 69–72. IEEE, 1994.
[34] Miaomiao Zhang, Zhiming Liu, Charles Morisset, and Anders P Ravn. Design and
verification of fault-tolerant components. In Methods, Models and Tools for Fault Tolerance,
pages 57–84. Springer, 2009.