在城轨列车运行车载控制系统中，硬件和软件同等重要，车载硬件已经逐步采用标准工业计算机产品，而负责实现核心功能的软件，已经成为保障列车安全高效运营的一个重要因素。由软件错误导致事故发生将会造成生命财产重大损失，所以针对城轨车载软件开发前期过程中的模型建立，模型测试、模型验证方法的研究具有重要意义。列控系统软件是多层次结构的复杂系统，具有并发性、响应性特性和状态空间庞大的特点，研究适合描述软件需求的基于模型驱动的建模方法、模型状态的转换、相关测试序列生成验证方法和模型软件测试，全套流程已经成为城轨列控系统软件的系统级建模评估理论的研究重点。根据城轨列控系统软件的需求及其实际功能相关的特点，提出了针对软件的建模技术、序列生成验证及测试方法。建模方面，从城轨列控软件需求出发，提出了基于模型驱动的软件架构的需求分析和功能划分，以车载设备软件为应用对象，使用了标准化建模语言UML，以图形化方式表述软件系统过程和实现方法。分析了具体模型的分层架构，用两种静态图和两种动态图从不同层面对细节进行了描述，对内建关联进行了层次连接。验证方面，介绍了模型检验的概念，说明了计算树逻辑（CTL）的扩展形式ASK-CTL在着色Petri网上的应用。从图的遍历角度，提出了深度优先算法在寻找有效测试路径的概念，并将算法运用于CPN Tools，以生成测试案例路径。引入实际的列控系统模型，提出了一种针对多线程的形式化定义ThrCPN及其图形描述，和基于对象UML模型的形式化建模方法ObjCPN。在层次化建模方法中，分别运用了ThrCPN和ObjCPN。提出了UML模型转换形式化有色Petri网的转换方法，缩小了功能模型到验证方案之间差距，简化了转换的复杂过程，形成了可验证的形式化模型。测试序列生成方面，在CPN Tools工具中应用了ML编写的深度优先搜索算法，生成的测试序列，解决了并发系统不可达状态过多的问题。形式化验证方法生成的案例工具为形式化检验的主要手段。测试序列的生成对后期软件模拟测试起到了测试案例的作用。对证例路径的修改和完善，也为后期代码的标准化起到关键作用。最后以城轨车载设备软件为测试对象，运用TestBed进行软件测试案例的生成和测试执行。比较了实际案例和形式化方法生成的路径，结果说明，基于模型驱动的软件建模方法可有效的实现系统的软件状态和行为，一定程度上约束了模型状态空间路径，且生成的针对软件需求的测试序列具有接近软件实际功能要求的特点。本方法还可用生成的模型指导应用软件的开发。