列车自动防护(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方法开发工具那样猜测操作参数的正确性，从而使模型验证结果更为准确。