延伸正規方法SpecTRM-RL以進行安全驗證

Extending Formal Method SpecTRM-RL for Safety Verification

史龍安(Lumg-An Shih)

指導教授 ： 范金鳳

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

摘要

本論文延伸N. Leveson的最新正規方法SpecTRM-RL，我們由SpecTRM-RL規格中，衍生了狀態轉換圖及UML時序圖以增進其可讀性。我們又在狀態圖及SpecTRM-RL上添增故障情況（failure condition），並根據此延伸的規格發展了一套有系統建構故障樹的方法，進行安全分析，我們的目的在提昇電腦控制系統的軟體安全性。我們以火車過平交道案例來說明此方法的可行性及有效性。並建議在限制（constraints）之外增添斷言（assertions）來確保系統執行時的安全。故障樹是屬於事前（靜態）的安全分析，分析的結論可以用於進一步的修正系統設計，或將故障的因子加入限制（constraints）或斷言（assertions）的考量中，可於執行時（動態）安全檢查。我們的靜態及動態安全驗證方法能增進系統的安全性。

關鍵字

SpecTRM-RL ； 故障樹 ； 安全分析 ； UML時序圖

並列摘要

This research extended Nancy Leveson’s newest formal specification method SpecTRM-RL. From SpecTRM-RL, we generated induced state transition diagrams and UML sequence diagrams to improve its understandability. Moreover, we added failure conditions in the state transition diagrams and SpecTRM’s AND/OR tables. Based on this proposed extension, we developed a systematic fault tree synthesis method to perform safety analysis. Our goal was to enhance software safety in computer-controlled systems. A railroad crossing case was used to demonstrate the feasibility and effectiveness of the proposed method.
Besides constraints, we suggested to add assertions to ensure run-time system safety. Fault tree analysis is an analytical safety analysis method performed before execution. The analysis results can be used to further modify system design or to be considered in constraints and assertions which are check at run time. Our static and dynamic safety analysis method can enhance system safety.

並列關鍵字

SpecTRM-RL ； fault trees ； safety analysis ； UML sequence diagrams

參考文獻

[1] 孫家禾,“以雙語言方式發展軟體正規規格”, 元智大學資訊工程研

[2] J.-R. Abrial,“The Specification Language Z : Syntax and

Semantics,”Oxford University Computing Laboratory,

[3] Jean-Raymond Abrial,“Steam-boiler control specification

Specifying and Programming the Steam Boiler Control,