基于SCADE的CBTC联锁建模与验证.docx

基于SCADE的CBTC联锁建模与验证
CBTC联锁系统是现代地铁自动化控制系统的核心部分，主要负责保障列车运行安全。SCADE是一种广泛应用于航空、铁路、汽车等领域的高可信软件工程工具，其在铁路行业基于V&V方法在安全相关应用中也有着较高的应用价值。本文主要探讨基于SCADE的CBTC联锁建模与验证。
一、CBTC联锁系统的基本原理
CBTC全称是Communication-basedTrainControlSystem，即基于通讯的列车控制系统，是地铁自动化控制系统中的一种较新的技术。传统的列车控制信号系统通常采用称为ATC(AutomaticTrainControl)系统，该系统采用的是一些固定的信号点，通过信号点的状态来进行列车的控制，缺少对列车位置的直接感知，运输系统效率较低。而CBTC系统通过列车与地面控制中心之间的通讯，提高了列车位置感知的精确度，使列车能够在无需拉设信号线的前提下实现精确的位置控制和运行调度。
CBTC联锁系统主要由列车控制单元、车站控制单元、列车位置显示单元、列车功率制动单元等组成。其中列车控制单元用来监控列车的实时位置，调度列车速度；车站控制单元用来监控车站的运行情况，预测列车运行时间；列车位置显示单元用来显示列车实时位置信息；列车功率制动单元用来控制列车前进与停止。
二、SCADE软件工程工具
SCADE是清华大学和法国国家航空航天研究所研制的一种交互式软件工程工具，它可以帮助开发人员和验证人员共同开发一个高质量、高可靠性、高安全性的软件系统。SCADE系统提供了很多自动生成代码的方法，以便相应的软件应用可以符合不同的安全标准，满足各种安全需求。同时，它还可以支持多种系统模型验证，防止用户对不同交互模型偏差的错误理解，保证软件模型的准确性。
三、基于SCADE的CBTC联锁建模与验证
CBTC联锁系统的安全是保证列车安全运行的基础，为此可以借助SCADE软件工程工具来确保CBTC联锁系统设计的正确性。基于V&V方法，SCADE工具可以对CBTC联锁系统进行模型建模、自动生成代码和验证分析。
（一）模型建模
在建模过程中可以采用数据流图和状态转移图方法来建模，其优点是直观、清晰、易于理解，适合软件系统的功能建模。同时，由于SCADE软件工程工具所支持的模型是一种形式化的模型，所以可以避免建模过程中出现的代码错误，以及消除其他人的歧义。
（二）自动生成代码
借助于SCADE工具，可以快速、自动地生成高质量代码，省去了开发人员重新编写代码的麻烦。SCADE软件工程工具的自动生成代码功能不仅可以保证代码准确性，提高代码质量，同时避免了编写大量重复代码的麻烦。
（三）验证分析
在验证分析过程中，可以采用模型检测的方法，对CBTC联锁系统进行冗余路径分析。通过分析CBTC联锁系统所有可能情况的运行特性，找出系统的漏洞和缺陷，并对这些漏洞和缺陷进行修正，以保证CBTC联锁系统的可靠性和安全性。
四、结论
CBTC联锁系统在地铁自动化控制系统中占有重要地位，建模和验证非常重要。SCADE软件工程工具为CBTC联锁系统的建模和验证提供了有力的支持。基于SCADE的CBTC联锁建模与验证可以保证系统的正确性和可靠性，提高列车运行效率，减少事故的发生。