原文传递
列控系统混成行为的建模与验证方法
| 论文题名： | 列控系统混成行为的建模与验证方法 |
| 关键词： | 列控系统;混成特性;物理融合系统;验证工具 |
| 摘要： | 随着列控技术的发展，列车运行控制系统获得了巨大的进步和发展。在系统的设计和开发阶段，为了确保列控系统的安全性，列控系统需求规范的正确性起着越来越重要的作用。然而，在系统开发的初始阶段，通常会因为系统需求规范不完整而无法进行开发。在这种情况下，如何确定系统的关键参数成为主要的研究课题。同时，现有研究成果表明，在需求层面，分析和验证系统模型中的关键参数面临很多困难。因此，为了解决系统模型中关键参数的分析问题，需要提出一种合理的系统属性建模和形式化验证的框架结构。 列控系统需求规范的分析过程包括两部的内容，建立系统规范模型和对该形式化模型进行验证。一方面，统一建模语言(UML)是一种面向对象的建模语言，已广泛应用于不同工程领域。然而，列控系统属于典型的混成系统和安全苛求系统。正确地刻画系统的混成特性给列控系统需求规范的建模工作带来了巨大的挑战。另一方面，形式化方法已成为保障安全苛求系统的安全性与可靠性的重要手段。根据不同的分析或验证要求，设计者可以选择不同的形式化验证工具进行相关的验证工作。 因此，本文从列控系统需求规范建模方法与验证工具集成着手进行研究，主要内容包括: 1.对列控系统混成特性进行分析，研究UML扩展机制，设计混成UML概要文件，使之能够准确地刻画列控系统的混成特性。 2.为了验证混成系统的安全性，提出了时间有界的可达性分析算法。该算法基于BMC验证技术，对具体的自动机模型运用该算法可以计算有界时间内系统的所有可执行路径。时间有界的可达性分析算法适用于线性或非线性混成自动机的验证。 3.以移动闭塞中的追踪模型为案例，运用提出的混成UML概要文件对其进行建模;并根据转换规则将所建的列车追踪扩展模型转换为HYTECH模型;在开发的验证支持工具中完成了该模型的验证分析工作。通过案例分析，证明所提出的基于UML扩展机制对列控系统混成行为建模方法的可行性，以及所开发验证支持工具的可用性。 4.在Topcased平台上完成了验证工具的软件开发。Topcased平台上集成了UML的建模工具Papyrus，并在Topcased平台上扩展了视图(Views)，将PHAVer和HYTECH等验证工具集成到该平台上，实现对模型的自动化验证，并具备良好的可扩展性。同时提出由扩展后的UML模型到形式化验证模型的转换规则，构造了面向对象语言UML与PHAVer、HYTECH、HySAT等形式化语言之间的转换桥梁。 |
| 作者： | 程瑞军 |
| 专业： | 交通信息工程及控制 |
| 导师： | 赵林 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2014 |
| 正文语种： | 中文 |
检索历史
应用推荐
