| 基于时序Petri网的联锁逻辑形式建模与验证 |
| |
| 引用本文： | 杜军威,徐中伟. 基于时序Petri网的联锁逻辑形式建模与验证[J]. 计算机工程与应用, 2007, 43(13): 7-10 |
| |
| 作者姓名： | 杜军威 徐中伟 |
| |
| 作者单位： | 同济大学,电子与信息工程学院,上海,200331;青岛科技大学,信息学院,山东,青岛,266061;同济大学,电子与信息工程学院,上海,200331 |
| |
| 摘 要： | 时序Petri网结合Petri和时序逻辑的优点,清晰简洁地描述并发系统事件间的时序和因果关系,包括系统的最终性和公平性。文章给出安全苛求系统——车站信号联锁逻辑系统的时序Petri网描述,并使用时序逻辑描述系统状态的时序和因果关系,最后通过分析和验证模型的性质得出系统是正确的。
|
| 关 键 词： | 联锁逻辑 时序Petri网 形式建模 时序逻辑 |
| 文章编号： | 1002-8331（2007）13-0007-04 |
| 收稿时间： | 2006-12-05 |
| 修稿时间： | 2007-01-01 |
Modeling and Verification of Interlocking Logic Based on Temporal Petri Nets |
| |
| DU Jun-wei,XU Zhong-wei. Modeling and Verification of Interlocking Logic Based on Temporal Petri Nets[J]. Computer Engineering and Applications, 2007, 43(13): 7-10 |
| |
| Authors: | DU Jun-wei XU Zhong-wei |
| |
| Abstract: | Temporal Petri nets,which combine the advantages of Petri nets and temporal logic,can describe clearly and compactly causal and temporal relationships between the events of a system,including eventuality and fairness.ln this paper,we firstly use temporal Petri nets to describe the railway signal interlocking logic system,a safety-critical system,and use temporal logic to describe temporal relationships of system states.Then,we analyze and verify the properties of model and conclude that the system is effective. |
| |
| Keywords: | interlocking logic temporal Petri nets formal modeling temporal logic |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
|
