Computer Engineering and Applications ›› 2007, Vol. 43 ›› Issue (13): 7-10.
• 博士论坛 • Previous Articles Next Articles
Jun-Wei Du
Received:
Revised:
Online:
Published:
Contact:
杜军威 徐中伟
通讯作者:
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. In 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.
Key words: temporal logic, interlocking logic, temporal Petri nets, formal modeling
摘要: 时序Petri网结合Petri和时序逻辑的优点,清晰简洁的描述并发系统事件间的时序和因果关系,包括系统的最终性和公平性。本文给出安全苛求系统——车站信号联锁逻辑系统的时序Petri网描述,并使用时序逻辑描述系统状态的时序和因果关系,最后通过分析和验证模型的性质得出系统是正确的。
关键词: 时序逻辑, 联锁逻辑, 时序Petri网, 形式建模
Jun-Wei Du. Modeling and Verification of Interlocking Logic Based on Temporal Petri Nets[J]. Computer Engineering and Applications, 2007, 43(13): 7-10.
杜军威 徐中伟. 基于时序Petri网的联锁逻辑形式建模与验证[J]. 计算机工程与应用, 2007, 43(13): 7-10.
0 / Recommend
Add to citation manager EndNote|Ris|BibTeX
URL: http://cea.ceaj.org/EN/
http://cea.ceaj.org/EN/Y2007/V43/I13/7