计算机应用
計算機應用
계산궤응용
COMPUTER APPLICATION
2013年
12期
3419-3422,3431
,共5页
于丽贞%徐中伟%陈祖希%张舒青
于麗貞%徐中偉%陳祖希%張舒青
우려정%서중위%진조희%장서청
铁路联锁系统%模型检测%形式化方法%梯形逻辑%NuSMV模型检测
鐵路聯鎖繫統%模型檢測%形式化方法%梯形邏輯%NuSMV模型檢測
철로련쇄계통%모형검측%형식화방법%제형라집%NuSMV모형검측
railway interlocking system%model checking%formal method%ladder logic%NuSMV model checking
铁路联锁系统设计通常采用梯形逻辑进行建模.为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL),最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证.
鐵路聯鎖繫統設計通常採用梯形邏輯進行建模.為瞭實現對鐵路聯鎖繫統進行形式化驗證的目的,根據梯形邏輯的狀態變遷語義,將梯形邏輯錶示的聯鎖繫統模型轉換成模型檢測工具NuSMV的語言,併將鐵路聯鎖繫統的安全需求錶示為計算樹邏輯(CTL),最後實現基于NuSMV的鐵路聯鎖繫統設計模型的形式化驗證.
철로련쇄계통설계통상채용제형라집진행건모.위료실현대철로련쇄계통진행형식화험증적목적,근거제형라집적상태변천어의,장제형라집표시적련쇄계통모형전환성모형검측공구NuSMV적어언,병장철로련쇄계통적안전수구표시위계산수라집(CTL),최후실현기우NuSMV적철로련쇄계통설계모형적형식화험증.
