基于时间有色Petri网的联锁软件的形式化建模与分析

摘要

在众多计算机应用领域中，铁路车站联锁系统不仅是实时系统，而且还是安全一关键系统。这种系统和航天、核工业、军事等应用系统具有一个重要的共同特征，就是它们的正确运行与否关系到人的生命安危和大量财产损失或生态环境的破坏。这种系统的时间参量非常重要，但是系统运行是否安全更关键。因此，在计算机技术和智能控制技术得到充分发展和应用的今天，对铁路车站联锁系统进行完备的形式化描述越来越受到重视。现有对铁路车站联锁系统的形式化描述工具主要是petri网和扩展petri网相关技术。但是现有技术大多数限于满足逻辑的准确性及模型的简化，添加时间约束的建模和模型分析还鲜见报道。 本文主要研究铁路车站联锁系统的形式化建模和模型分析。在现有的时间petri网模型和有色petri网模型基础上，结合区间时间有色petri网(IntervalTimed Colored Petri Nets，简称ITCPN)对铁路车站联锁逻辑进行建模和模型分析。ITCPN使模型更接近实际系统(加入运行时间区间，即时延用上、下边界来规定)。本文主要以铁路车站联锁系统作为实际研究案例，但是同时也不失一般应用的案例描述。文中用充分的理论认证和实践案例证明了ITCPN是适合描述安全一关键系统的，并且可以对其模型进行分析。

目录

文摘

英文文摘

声明

第1章绪论

1.1引言

1.1.1实时系统

1.1.2安全—关键系统

1.1.3铁路车站计算机联锁系统

1.2国内外研究动态

1.2.1 petri网技术的发展

1.2.2计算机联锁系统发展

1.3论文主要工作

第2章petri网理论基础

2.1引言

2.2基本petri网

2.2.1 petri网的定义

2.2.2变迁的发射规则

2.2.3 petri网的动态性质

2.2.4 petri网的建模实例

2.3有色petri网

2.4时间petri网

2.4.1时间petri网(time petri nets)

2.4.2时延petri网(timed petri nets)

第3章petri网的模型分析方法

3.1引言

3.2一般petri网分析方法

3.2.1 P不变量分析法

3.2.2可达图

3.3时间petri网的分析方法

3.3.1状态类

3.3.2带时间戳的状态类(CS-class)分析方法

第4章时间有色petri的基本理论

4.1引言

4.2 ITCPN定义

4.3 ITCPN的动态性质

4.4 ITCPN建模举例

第5章ITCPN模型分析

5.1引言

5.2 ITCPN压缩状态空间分析法

5.2.1 ITCPN互斥模型

5.2.2压缩状态空间分析法

5.3 ITCPN化简可达图分析法

5.3.1无限状态可达图

5.3.2状态聚合化简方法

第6章基于ITCPN的车站联锁逻辑建模及分析

6.1铁路车站联锁系统

6.2联锁逻辑的ITCPN模型

6.2.1进路建立的ITCPN模型

6.2.2进路自动解锁三点检查的ITCPN模型

6.2.3 ITCPN模型的发射规则

6.3模型分析

6.3.1不考虑时间参量的分析

6.3.2考虑时间参量的分析

6.3小结

第7章总结与展望

致谢

参考文献

个人简历 在读期间发表的学术论文与研究成果