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

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

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