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

• 作者: 刘金涛 唐涛 徐田华 赵林
• 来源期刊: 中国铁道科学
• 学科: 交通运输
• 关键词: 列车控制系统 需求规范 形式化方法 UML 符号模型检验
• 年，卷（期）: 2011,（3）
• 页码范围: 93-99
• 分类号: U284.482|U238
• 字数: 6101字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学轨道交通控制与安全国家重点实验室	152	2578	27.0	40.0
2	徐田华	北京交通大学轨道交通控制与安全国家重点实验室	21	347	11.0	18.0
3	赵林	北京交通大学轨道交通控制与安全国家重点实验室	11	160	8.0	11.0
4	刘金涛	北京交通大学轨道交通控制与安全国家重点实验室	7	110	6.0	7.0