限制為基礎的軟體需求規格及安全驗證技術

Constraint-based Software Specification and Safety Verification

吳嘉國(Chia-Kuo Wu)

指導教授 ： 范金鳳

元智大學/資訊學院/資訊工程學系/碩士(2004年)

摘要

近年來，電腦系統被廣泛的應用在我們的日常生活中，包括許多安全關鍵應用的領域，例如核能電廠、醫療診察、飛航系統…等等。許多因為軟體錯誤而導致的意外事故，往往造成生命財產的嚴重損失。因此，為了有效確保安全關鍵系統的安全性，軟體規格及安全驗證技術的發展是值得重視與探討的。
以限制(Constraint)為基礎的軟體需求規格是在制訂軟體行為及特性的規格之外，添加許多的限制。在系統軟體執行時，若有違反限制的情形，操作人員可即時進行系統的調整，以確保系統在安全的模式下執行。本論文旨在發展以限制為基礎的軟體需求規格方法，並研究相關的安全檢查與分析驗證技術。
SpecTRM-RL是由Nancy G. Leveson所發展的一套最新的規格語言，為混合正規與非正規方法，其特色是以控制理論（control theory）為基礎，在系統規格中制定限制項目。DFM為George E. Apostolakis所發展的方法，用於設計電腦控制系統的行為，並可從DFM圖形中建構時間相關的故障樹(Fault Tree)進行安全分析。我們的方法延伸SpecTRM-RL需求規格，並結合DFM的軟體設計規格。在此論文中我們對SpecTRM-RL增加了圖形的表示、正規表示、增添的斷言、限制的一致性檢查及斷言的重要性評估，並針對需求規格與軟體設計層次，提供故障樹的自動安全分析技術。本研究可有效提昇安全關鍵軟體的規格品質及安全性。

關鍵字

軟體需求規格 ； 安全分析 ； 故障樹 ； 狀態轉換圖

並列摘要

In the recent years, computer has been extensively integrated into systems related to our daily life, including many safety-critical application systems. Many serious accidents incurred by software defects had occurred and caused loss of lives. Therefore it is critical to investigate development and verification methods for safety-critical software so as to ensure its safety.
Constraint-based specifications refer to the specifications that adds constraints besides behavior modeling or properties specification. If the system violates constraints, appropriate runtime adjustment can be made to ensure the system in safe state. This research aims to develop Constraint-based software specifications method suitable for safety analysis at requirement and design steps and also to develop related verification techniques.
SpecTRM is Nancy Leveson’s newest requirements specification method. It is based on control theory with a feedback loop. Dynamic Flowgraph Methodology (DFM) developed by George E. Apostolakis is an approach to modeling and analyzing the safe behavior of a computer-controlled system at design level. DFM includes a systematical way to generate timed fault trees from DFM specification for safety analysis. This research adds graph representation, augmented assertions, formal representation, consistency checking of constraints and safety analysis to the original SpecTRM-RL. We also incorporate it with DFM, so as to perform safety analysis at design stage. Thus, the research will enhance the quality and safety of safety-critical software.

並列關鍵字

SpecTRM-RL ； DFM ； SCR ； Fault tree ； Safety analysis ； Statechart ； Constraint

參考文獻

2. B. E. Malhart,“Software fault tree analysis for a requirements system model,” Systems Engineering of Computer Based Systems, 1995., Proceedings of the 1995 International Symposium and Workshop on , 6-9 March 1995 Pages:133 — 140.

3. B. Mavko M. and Cepin,“Fault tree developed by an object-based method improves requirements specification for safety-related systems,” Elsevier Science, Reliability Engineering and System Safety 63 (1999) 111-125.

5. C. Fan and S. Yih, “Frame-based Safety Analysis Approach for Decision-based Errors,” Reliability Engineering and System Safety, Vol. 55, no. 3, pp. 243-256, March, 1997.

6. C. Fan and W. Cheng, "Accident Sequence Analysis of Human-Computer Interface Design," Reliability Engineering and System Safety, Vol. 67, no. 1, PP. 29-40, Jan. 2000.

8. C. J. Garrett, S. B. Gyarro, and G. E. Apostolakis, “The Dynamic Flowgraph Methodology for Assessing the Dependability of Embedded Software Systems, ” IEEE Transactions on systems. man. and cybernetics. Vol. 25. 5, MAY 1995.