一种面向SCR需求模型的形式化验证方法研究

张 漾，胡 军，王立松，康介祥，王 辉，高忠杰

1(南京航空航天大学 计算机科学与技术学院，南京 211106)2(软件新技术与产业化协同创新中心，南京 210007)3(中国航空无线电电子研究所，上海 200233)

1 引 言

计算机系统软件本身的可靠性和安全性是安全关键系统[1，2]正常运行的先决条件.近年来航空事业发展迅速，航电系统[3]的复杂性急剧增加，机载软件适航认证标准DO-178C[4]支持采用形式化方法验证航空软件.基于模型的安全评估[5，6](MBSA)方法可以通过对安全关键系统建立模型，从而将复杂的系统行为描述为精确的、可读的数学表达式，并对相关需求规约[7，8]实现分析，检查需求模型的一致性和完备性，验证系统的正确性.

T-VEC是基于4变量模型[9，10]中的SCR方法，进行需求设计、需求建模的工具.通过表格表达式，它用模式转换表、条件表和事件表等形式化数学符号，描述系统在不同的模式、条件和状态下，状态变量不同的取值，表现系统状态迁移的逻辑关系，从而实现对系统行为形式化描述.

形式化验证[11]是用精确的、高效的数学方法验证系统的正确性或评估系统可能存在的缺陷，从而做出关于系统设计的正确决策.形式化方法有3大类分别是演绎证明(deductive proof)、模型检验(model checking)和抽象解释(abstract interpretation).本文主要介绍和使用在工业上应用最广泛的模型检验方法.模型检验[12]是一种自动化验证技术，其输入是描述成状态机的系统模型和描述成模态逻辑公式的待验证系统属性，通过验证“模型状态机可达路径是否满足模态逻辑公式”来给出结果；……