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

第1章 列车运行控制系统实时性概述
1．1 列车运行控制系统简介
1．1．1 列车运行控制系统的现状与发展
1．1．2 列车运行控制系统的组成
1．1．3 列车运行控制系统的特点
1．2 列车运行控制系统的实时性要求
1．3 国内外研究现状
1．4 列车运行控制系统实时性的建模与验证方法
第2章 基于UML的列控系统实时性研究
2．1 UML概述
2．1．1 UML的定义
2．1．2 UML的组成
2．1．3 UML建模机制
2．2 UML扩展机制
2．2．1 约束
2．2．2 标记值
2．2．3 构造型
2．3 列控系统的UML模型
2．3．1 用例图
2．3．2 类图
2．3．3 活动图
2．3．4 部署图
2．3．5 序列图
2．3．6 状态图
2．4 基于UML的模型转换方法
2．4．1 模型转换的概念
2．4．2 UML元模型
第3章 基于UML与CSP的实时系统建模与分析
3．1 CSP相关理论
3．1．1 CSP的语法和语义
3．1．2 CSP的实时性扩展
3．2 UML到CSP的转换规则
3．2．1 活动图转换规则
3．2．2 状态图转换规则
3．3 模型转换中特性的保持与转换规则的证明
3．3．1 模型转换中特性的保持
3．3．2 模型转换规则的证明
3．4 UML转换至CSP的列控系统实时性分析实例
第4章 基于时间自动机的系统建模与验证
4．1 时间自动机
4．1．1 时间约束和时间解释
4．1．2 时间语言
4．1．3 时间自动机的语义
4．1．4 时间自动机的积
4．2 基于时间自动机的形式化建模
4．3 模型检验方法验证实时系统
4．3．1 时序逻辑
4．3．2 时序逻辑的时间化
4．3．3 验证流程
4．4 定理证明方法验证实时系统
……