计算机联锁系统(CBI)是铁路运输中的重要设备,它肩负着列车调度、安全行车、提高运输效率的重要工作。它通过对道岔、进路以及信号的控制,来实现铁路列车的调度指挥工作。随着计算机技术在铁路信号中的发展与应用,传统的分析设计方法已经无法满足当前社会对于铁路运输的安全性、高效性需求。为此我们采用模型驱动的嵌入式软件开发方法对联锁软件的设计与验证提出了新的思路,从而提高软件开发的精确性和高效性。本文首先深入研究了各种形式化建模语言在嵌入式软件中的应用,以及它们在当前国际国内的发展水平和未来发展趋势。主要对各个方法的优点与缺点进行了对比分析,找出了一种适合计算机联锁系统软件开发的以模型设计需求分析取代传统文本设计需求分析的方法,即时间自动机理论。本文以工大高科自主研发的计算机联锁系统软件GKI-33e为研究对象,对它的进路办理流程进行了深入的分析,根据EN系列标准以及国家铁路标准对它的安全性和功能性进行了主要描述,提出了软件设计的V模型。并根据此设计流程对进路办理流程进行了形式化建模与分析。本文针对进路办理中的五个主要阶段分别建立了对应的时间自动机模型,并且通过成熟的UPPAAL工具组建了时间自动机网络,并对该网络进行了仿真模拟,通过时间约束与全局变量的设定,解决了以往开发过程中存在的模糊性、二义性等问题。最后,本文从系统的功能性与安全性出发,对时间自动机网络进行了验证。通过BNF语法对系统安全功能进行了验证与分析。证明了以模型驱动方法为基础的嵌入式软件开发方法的可行性。为计算机联锁系统软件设计提供了重要的参考价值。