正規方法應用於安全個案上之論證

Formal Methods for Safety Case

楊仁賢(Zen-Shien Yang)

指導教授 ： 范金鳳

元智大學/工程學院/電機與資訊工程研究所/碩士(1998年)

摘要

安全個案 (safety case) 為一套論證 (argument) 的過程，提出足以令人信服的證據以說明一安全關鍵系統在給定的環境下符合安全的要求。在歐美各國，安全關鍵計算系統執照的申請均要求提出安全個案。而現今安全個案多數使用主觀論證，本研究提出以正規軟體發展方法應用在安全個案的論證上，發展的論證及方法包括 : 正規規格、證明符合法規之要求項目、故障樹為主之安全性論證、正規規格轉換成程式碼、規格為基礎之測試、預測測試結果及線上偵錯方法等。並以核能保護系統為範例，以上述方法作成一個完整的安全個案。使用正規方法的目的在於它具有很高的嚴謹性以及說服力，可以增加安全個案的可信任度，並確保軟體的安全性。

關鍵字

正規方法 ； 安全個案

並列摘要

Safety case is a process of an argument. It is a documented body of evidence that provides a convincing and valid argument that a system is adequately safe for a given application in a given environment. In Europe and America, a safety case is required in the application for an operation license of a safety-critical computing system. But most of the contemporary safety cases employ subjective argument. This thesis proposes to apply formal methods to safety case argument. The developed techniques include : formal software requirements specifications、formal proof requirements、safety argument using fault tree、formal program derivation、specification-based testing、and test oracle、as well as on-line testing. Using these techniques we have developed a complete safety case for a nuclear protecting system. Formal methods provide precision and persuasion; it enhances trustworthiness of safety cases, and also ensures software safety.

並列關鍵字

formal method ； safety case

參考文獻

[1] Bob Fields and Morten Elvang-Goransson, "A VDM Case Study in mural", IEEE Transactions on Software Engineering, vol. 18, no. 4, April 1992. pp. 279-295.

[2] L. M. Barroca and J. A. Mcdermid, "Formal Methods and Safety Critical Systems", The Computer Journal, vol. 35, no. 6, 1992.

[3] Juan Bicarregui and Brian Ritchie, "Invariants, Frames and Postconditions : A Comparison of the VDM and B Notations", IEEE Transactions on Software Engineering, vol. 21, no. 2, February 1995. pp. 79-89.

[6] Ralph Jeffords and Constance Heitmeyer , "Automatic Generaton of State Invariants from Requirements

[7] Nancy G. Leveson and Stephen S. Cha, "Safety Verification of ADA Programs Using Software Fault Trees".