基于时序Petri网的联锁逻辑形式建模与验证

摘要：

时序Petri网结合Petri和时序逻辑的优点,清晰简洁地描述并发系统事件间的时序和因果关系,包括系统的最终性和公平性.文章给出安全苛求系统--车站信号联锁逻辑系统的时序Petri网描述,并使用时序逻辑描述系统状态的时序和因果关系,最后通过分析和验证模型的性质得出系统是正确的.

关键词：联锁逻辑、时序Petri网、形式建模、时序逻辑

所属期刊栏目：43

分类号：TP311.52(计算技术、计算机技术)

资助基金：国家自然科学基金60674004

在线出版日期：2007-10-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：7-10