安全關鍵系統(tǒng)的形式化開發(fā)方法研究.pdf

1、該文立足于安全關鍵系統(tǒng),選擇鐵路車站信號控制系統(tǒng)作為具體的應用對象,對安全關鍵系統(tǒng)的形式化開發(fā)方法進行了下述主要研究和探索工作:總結了1.鐵路信號領域安全關鍵系統(tǒng)形式化方法的應用情況,指出了安全關鍵系統(tǒng)中存在的問題.2.從系統(tǒng)工程的角度出發(fā),基于形式化方法,對安全關鍵系統(tǒng)的開發(fā)方法進行了深入研究.3.對安全關鍵系統(tǒng)的基本特性—故障-安全性進行了研究,給出了形式化的 描述和驗證的方法.4.研究了安全關鍵系統(tǒng)的有限自動機,給出了系統(tǒng)故障-安

2、全性的有限自動機 表示方法和系統(tǒng)狀態(tài)的故障-安全轉移邏輯,從而使有限自動機可以被用來 進行系統(tǒng)故障-安全性的形式化驗證.5.對安全關鍵系統(tǒng)的模型檢驗形式化方法進行了深入的研究,提出了模型檢驗故障-安全約束的概念和方法.6.把FDN開發(fā)模型應用于鐵路車站信號控制系統(tǒng),給出了一種典型的鐵路車站信號控制系統(tǒng)的體系結構模型,推導了該系統(tǒng)的故障-安全性CTL公式,用模型檢驗方法對其進行了驗證.7.深入地研究了安全關鍵系統(tǒng)符號模型檢驗的形式化方法,