未找到相关数据
联锁软件的Petri网形式化定义
被引：9
作者：
杨扬
潘明
何梅芳
机构：
[1] 铁道科学研究院
[2] 铁道科学研究院 北京
[3] 北京
来源：
关键词：
铁路信号;
计算机联锁;
Petri网;
形式化定义;
形式化验证;
D O I：
暂无
中图分类号：
U284.362 [];
学科分类号：
082302 ;
摘要：
用Petri网对联锁系统中的核心部分———联锁机中的联锁软件进行形式化定义和分析 ,以减少联锁系统中的不确定性因素 ,降低联锁软件的复杂性 ,保证联锁软件定义的正确性 ,并对该定义进行了形式化验证。同时以进路建立过程作为事例 ,说明了用Perti网形式化定义联锁软件的具体过程。采用分层模型化技术对联锁软件中的各个变迁 (模块 )进行逐级分解和验证 ,最终得到经过验证的、足够详细的联锁软件模型。利用该模型能对系统的一些重要性能 (如安全性和实时性 )进行分析和改进
引用
收藏
页码：51 / 56
页数：6
相关论文