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

作者：刘金涛; 唐涛; 徐田华; 赵林

来源：中国铁道科学, 2011, (03): 93-99.

• 列车控制系统
• 需求规范
• 形式化方法
• UML
• 符号模型检验 Train control system
• Requirement specification
• Formal method
• Symbolic model checking

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

• 单位
  北京交通大学; 轨道交通控制与安全国家重点实验室