面向VRM模型的软件需求的形式化组合验证方法

摘要

如何对软件需求展开有效验证是当前国内民机系统安全攸关软件研发过程中的重要挑战.本文对基于变量关系模型VRM(Variable Relation Model)的机载软件需求形式化建模与验证过程中出现的状态空间爆炸问题，提出了一个面向VRM需求模型的状态空间等价语义划分准则和形式化组合验证方法框架，包括：基于VRM模型的结构和语义，构建变量依赖图VDG(Variable Relation Graph);设计了多个独立性划分算法将模型划分为若干独立的子模型；同时考虑所需验证的属性公式中的变量依赖关系，提出了一种属性驱动的独立性划分方法，并证明了划分前后模型状态空间的语义等价性；最后建立了从VRM模型转换到SMV模型的流程，并给出了一个机载软件系统需求建模与验证的实例研究.

关键词

软件需求验证 / 安全攸关软件 / 模型检测 / 状态空间爆炸 / 模型划分