ATP系统形式化开发方法的研究

摘要

列车自动防护(Automatic Train Protection,简称 ATP)系统是基于通信的列车控制系统的一个负责列车安全的子系统。ATP系统负责了列车的测速、测距、超速防护、速度曲线的计算等等功能。因此,ATP系统软件的开发尤为重要。这是列车安全运行的保证,目前国内对ATP系统的研究成果还不是很成熟,然而ATP系统的系统化和网络化程度非常的高,且非常庞大和复杂,采用形式化方法建立其系统的整体模型能够更为直观的理解和分析车载 ATP系统,并可以消除软件开发的二义性,减小软件开发成本,保证ATP系统功能的逻辑正确性和完备性。
　　统一建模语言(Unified Modeling Language,简称UML)是面向对象开发方法中常用的技术手段,B方法是一种形式化开发方法。将B方法与UML语言结合就能弥补UML语言的不足,结合之后的方法也具有更精确的语义且无二义性。B方法与传统的软件开发方法一样,可以参与到从系统需求分析、设计到最后系统功能实现的全过程中去。
　　本文以列车ATP系统为研究对象,围绕着对ATP系统建模和验证方法展开研究。选取UML静态模型图中的类图和状态图,采用B方法的抽象机语言对UML类图和状态图进行形式化描述,建立了类图和状态图到 B方法抽象机之间的映射关系。最后将UML类图和状态图到B方法的形式化规约应用到ATP系统的列车间距控制功能、车门控制功能、超速防护功能上去,应用proB作为模型验证工具,验证了ATP系统功能的模型正确性。
　　本论文通过形式化建模和其验证方法,改进了目前 ATP系统需求规范的建模和验证方法。与传统的建模和验证方式只能简单应用到 ATP系统的某一个功能不同,这个方法能用到整个ATP系统中去。
　　针对ATP系统的特点,通过UML类图和状态图到B方法形式化规约的映射关系,将形式化方法应用于ATP系统建模和验证的过程中去,强化了ATP系统建模和验证的安全。并且应用proB作为模型验证工具,不会像其他B方法开发工具那样猜测操作参数的正确性,从而使模型验证结果更为准确。

目录

封面

声明

中文摘要

英文摘要

目录

1绪论

1.1研究背景及意义

1.2国内外研究现状

1.3论文的研究内容和结构

2基于CBTC的列车自动防护系统

2.1 CBTC系统简介

2.2 ATP系统的组成

2.3 ATP系统的总体结构

2.4 ATP系统功能

2.5本章小结

3 ATP系统需求规范与验证方法的演化

3.1形式化方法与传统建模方法的比较

3.2形式化方法的主要研究内容

3.3形式化B方法

3.4本章小结

4基于UML的ATP系统需求规范建模分析

4.1统一建模语言UML

4.2 ATP系统需求规范UML模型图的形式化描述

4.3本章小结

5 ATP系统主要功能模型图及检测

5.1列车间隔控制功能的UML模型图

5.2列车速度监督与超速防护功能的UML模型图

5.3 ATP系统的总体结构

5.4系统的模型检测

5.5本章小结

结论

致谢

参考文献

攻读学位期间的研究成果