CTCS-3级列控系统规范建模与验证

结合统一建模语言UML与符号模型检验SMV形式化方法,提出需求规范严格建模和验证方法。利用需求管理工具,保证了模型和规范的一致性和对规范的覆盖性,同时实现了规范验证结果对模型、转换规则和规范的跟踪。给出了CTCS-3级列控系统严格建模与验证的方法体系和流程,并以CTCS-3级列控系统需求规范中的模式转换部分为例,说明了规范的建模、验证和分析过程。