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

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

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

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

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

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

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

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

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

運動干涉檢測的模糊邏輯控制04-26

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

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

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

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

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

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