基于UML的CTCS-3级列控系统需求规范形式化验证方法

摘要：

采用UML与符号模型检验相结合的方法,对CTCS-3级列控系统需求规范进行形式化验证.使用引入事件、可见变量抽象的方法,对需求规范UML模型进行扩展和抽象.根据转换规则,建立需求规范的NuSMV模型,并对NuSMV模型进行领域无关特性和领域相关特性的验证,通过反例对错误进行追踪、定位和修改.以需求规范中的模式转换为例,采用给出的形式化验证方法对其进行验证,验证结果确认模式转换满足活性、转移性、无死锁性、确定性及安全性的要求;验证过程表明UML与符号模型检验相结合的方法适用于CTCS-3级列控系统需求规范的验证.

关键词：列车控制系统、需求规范、形式化方法、UML、符号模型检验

所属期刊栏目：32

分类号：U284.482;U238(铁路通信、信号)

资助基金：国家自然科学基金;轨道交通控制与安全国家重点实验室自主研究项目

在线出版日期：2011-09-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：93-99