联锁软件的Petri网形式化定义

• 作者: 何梅芳 杨扬 潘明
• 来源期刊: 中国铁道科学
• 学科: 交通运输
• 关键词: 铁路信号 计算机联锁 Petri网 形式化定义 形式化验证
• 年，卷（期）: 2002,（3）
• 页码范围: 49-54
• 页数: 6页
• 分类号: U284.362
• 字数: 4341字
• 语种: 中文
• DOI: 10.3321/j.issn:1001-4632.2002.03.010

摘要

用Petri网对联锁系统中的核心部分--联锁机中的联锁软件进行形式化定义和分析,以减少联锁系统中的不确定性因素,降低联锁软件的复杂性,保证联锁软件定义的正确性,并对该定义进行了形式化验证.同时以进路建立过程作为事例,说明了用Perti网形式化定义联锁软件的具体过程.采用分层模型化技术对联锁软件中的各个变迁(模块)进行逐级分解和验证,最终得到经过验证的、足够详细的联锁软件模型.利用该模型能对系统的一些重要性能(如安全性和实时性)进行分析和改进.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨扬		4	65	3.0	4.0
2	潘明		4	60	3.0	4.0
3	何梅芳		5	91	4.0	5.0