论文部分内容阅读
系统规范是系统开发的起点和基础。系统规范的缺陷将给项目成功带来极大的风险。对系统规范进行建模和验证是消除潜在缺陷的有效方法，也是保证系统正确设计和开发的前提。 近些年来，中国轨道交通事业快速发展。以CTCS-3级列车运行控制系统为代表的基于无线通信的列车运行控制系统是今后的发展方向。CTCS-3级列车运行控制系统系统是一个典型的混成系统，列车的连续运行过程和无线闭塞中心(RBC)的离散作用机制之间交互影响，呈现复杂的混成性。列车事故的发生往往同速度、加速度、距离等连续变化量的不良控制密切相关。因此，从混成性的角度对安全关键CTCS-3系统规范进行建模与验证是非常有必要和有意义的。 以此为出发点，本文在列车运行控制系统规范建模与验证体系的基础上，给出面向混成性的CTCS-3系统规范建模与验证的方法和流程：首先利用可描述系统混成性的HybridUML对CTCS-3系统规范建模，接着将模型转换为形式化的微分动态逻辑模型，最后在验证工具里对系统规范的微分动态逻辑模型进行形式化验证。 本文重点阐述了基于UML2.0的扩展机制在建模软件RSA中构建概要文件(profile)实现UML2.0到HybridUML扩展的过程；同时以列车运动加速减速过程为例阐述了如何利用经扩展得到的HybridUML对CTCS-3系统规范进行建模；接着给出了从HybridUML模型到微分动态逻辑模型的转换规则，进而使CTCS-3系统的形式化模型的获得和对模型的形式化验证能够得以实现。 最后本文以CTCS-3系统中典型的RBC切换流程为案例，给出了面向混成性的CTCS-3系统规范建模与验证的方法的具体应用。首先介绍了CTCS-3系统规范中RBC切换流程的过程，接着在RSA中对RBC切换流程建立HybridUML模型，然后根据从HybridUML到微分动态逻辑的转换规则得到RBC切换的微分动态逻辑模型，最后在形式化验证工具KeYmaera中对微分动态逻辑模型的安全性等性质进行验证并对验证结果进行了分析。案例分析很好地展示了面向混成性的建模与验证的方法和流程，充分体现出方法和流程的有效性和可行性。