列车运行控制系统实时性的建模与验证

第1章列车运行控制系统实时性概述1 1.1列车运行控制系统简介1 1.1.1列车运行控制系统的现状与发展1 1.1.2列车运行控制系统的组成2 1.1.3列车运行控制系统的特点3 1.2列车运行控制系统的实时性要求5 1.3国内外研究现状6 1.4列车运行控制系统实时性的建模与验证方法8 第2章基于UML的列控系统实时性研究10 2.1UML概述10 2.1.1UML的定义10 2.1.2UML的组成10 2.1.3UML建模机制14 2.2UML扩展机制15 2.2.1约束15 2.2.2标记值16 2.2.3构造型17 2.3列控系统的UML模型18 2.3.1用例图18 2.3.2类图19 2.3.3活动图21 2.3.4部署图22 2.3.5序列图23 2.3.6状态图26 2.4基于UML的模型转换方法29 2.4.1模型转换的概念30 2.4.2UML元模型31 第3章基于UML与CSP的实时系统建模与分析35 3.1CSP相关理论36 3.1.1CSP的语法和语义36 3.1.2CSP的实时性扩展37 3.2UML到CSP的转换规则39 3.2.1活动图转换规则39 3.2.2状态图转换规则41 3.3模型转换中特性的保持与转换规则的证明45 3.3.1模型转换中特性的保持45 3.3.2模型转换规则的证明46 3.4UML转换至CSP的列控系统实时性分析实例50 第4章基于时间自动机的系统建模与验证53 4.1时间自动机53 4.1.1时间约束和时间解释53 4.1.2时间语言55 4.1.3时间自动机的语义55 4.1.4时间自动机的积57 4.2基于时间自动机的形式化建模58 4.3模型检验方法验证实时系统59 4.3.1时序逻辑60 4.3.2时序逻辑的时间化62 4.3.3验证流程64 4.4定理证明方法验证实时系统65 4.5基于时间自动机的列控系统模型实例67 4.5.1案例描述67 4.5.2案例模型的时间约束68 4.5.3案例建模与验证分析69 第5章基于着色Petri网的系统建模与分析72 5.1着色Petri网72 5.1.1Petri网概述72 5.1.2Petri网的结构73 5.1.3Petri网的行为特性74 5.1.4着色Petri网的定义76 5.2基于着色Petri网的复杂系统实时性任务的建模及其分析77 5.2.1复杂系统结构和实时性任务的基本假设77 5.2.2基于着色Petri网的复杂系统实时性任务建模78 5.2.3基于着色Petri网模型的复杂系统实时性任务的可靠性分析79 5.2.4着色Petri网中复杂系统实时性评价方法80 5.3基于着色Petri网的列控系统分析实例82 5.3.1实例描述82 5.3.2CPN模型的建立85 5.3.3时间模型的建立与验证91 第6章基于马尔可夫链的实时系统分析94 6.1马尔可夫链理论94 6.1.1马尔可夫链94 6.1.2状态转移95 6.1.3马尔可夫分析96 6.2马尔可夫链在列车行车时间预测中的应用98 6.2.1隐马尔可夫链98 6.2.2自回归模型算法99 6.2.3时间性和关联性聚类算法100 6.2.4维特比算法102 6.3多元马尔可夫链与列控系统信息时效性评价104 6.3.1列控系统的信息时效性判定104 6.3.2多元马尔可夫链模型的构造109 6.3.3模型参数的估计111 参考文献115