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