信息技术
信息技術
신식기술
INFORMATION TECHNOLOGY
2013年
2期
7-10,14
,共5页
联锁逻辑%形式化建模%Event-B
聯鎖邏輯%形式化建模%Event-B
련쇄라집%형식화건모%Event-B
铁路车站信号联锁逻辑的形式化描述无论对计算机联锁软件的研发,还是对联锁软件的第三方测试都是非常重要的.基于Event-B方法,利用自动机模型和形式化语言对车站的一种信号联锁逻辑进行建模研究,并通过逐步精化的方法扩展联锁功能,依赖不变式技术形式化地保证了该模型的安全性.所建模型通过Rodin平台的验证,结果表明它们是安全的.
鐵路車站信號聯鎖邏輯的形式化描述無論對計算機聯鎖軟件的研髮,還是對聯鎖軟件的第三方測試都是非常重要的.基于Event-B方法,利用自動機模型和形式化語言對車站的一種信號聯鎖邏輯進行建模研究,併通過逐步精化的方法擴展聯鎖功能,依賴不變式技術形式化地保證瞭該模型的安全性.所建模型通過Rodin平檯的驗證,結果錶明它們是安全的.
철로차참신호련쇄라집적형식화묘술무론대계산궤련쇄연건적연발,환시대련쇄연건적제삼방측시도시비상중요적.기우Event-B방법,이용자동궤모형화형식화어언대차참적일충신호련쇄라집진행건모연구,병통과축보정화적방법확전련쇄공능,의뢰불변식기술형식화지보증료해모형적안전성.소건모형통과Rodin평태적험증,결과표명타문시안전적.
