CTCS-2级列控系统的形式化建模与验证

摘要：

由于CTCS-2级列控系统设计复杂,因此提出一种将统一建模语言(UML)与符号模型检验相结合的形式化建模与验证方法.分析CTCS-2级列控车载设备的模式转换场景,对其进行UML建模得到UML类图和状态图,制定转换规则对UML模型进行扩展和抽象,使其转化为NuSMV模型.将待验证的系统性质和转化后的检验程序输入符号模型检验系统进行验证,验证结果都为true,表明CTCS-2级列控车载设备的模式转化场景具有活性、可达性和安全性.

关键词：列控系统、符号模型检验、形式化方法、车载设备、模式转换

所属期刊栏目：39

分类号：N945(系统科学)

资助基金：国家自然科学基金资助项目61164010;甘肃省教育厅硕导基金资助项目210110

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

页数：共4页

页码：12-15