計(jì)算機(jī)聯(lián)鎖控制邏輯的模型檢驗(yàn)方法

描述了符號(hào)化模型檢驗(yàn)策略和相應(yīng)的工具軟件SMV,通過該工具驗(yàn)證了鐵路計(jì)算機(jī)聯(lián)鎖控制邏輯的設(shè)計(jì)符合其安全規(guī)范,最后分析了模型檢驗(yàn)面臨的困難以及今后的努力方向.

作 者： 燕飛 唐濤 Yan Fei Tang Tao   作者單位： 燕飛,Yan Fei(北京交通大學(xué)軌道交通控制與安全國(guó)家重點(diǎn)實(shí)驗(yàn)室,100044,北京)

唐濤,Tang Tao(北京交通大學(xué)電子信息工程學(xué)院,100044,北京) 

刊 名： 鐵道通信信號(hào)  英文刊名： RAILWAY SIGNALLING & COMMUNICATION  年，卷(期)： 2009 45(5)  分類號(hào)： U2  關(guān)鍵詞： 鐵路計(jì)算機(jī)聯(lián)鎖系統(tǒng)   形式化方法   模型檢驗(yàn)  

【計(jì)算機(jī)聯(lián)鎖控制邏輯的模型檢驗(yàn)方法】相關(guān)文章：

水環(huán)境的非點(diǎn)源污染模型及污染控制方法04-29

基于模糊邏輯系統(tǒng)的轉(zhuǎn)子振動(dòng)控制方法研究04-29

群集模型的軟控制研究04-28

運(yùn)動(dòng)干涉檢測(cè)的模糊邏輯控制04-26

邏輯斯蒂曲線的幾個(gè)推廣模型與應(yīng)用04-30

基于描述邏輯的地圖語義模型初步研究04-27

工作壓力的要求--控制模型04-29

淺議數(shù)學(xué)模型方法04-26

邏輯演算與形式化方法04-30

計(jì)算機(jī)聯(lián)鎖控制系統(tǒng)在柳鋼鐵路中的運(yùn)用04-28