软件学报

作者：杨晓，王小齐，陈小红，金芝

单位：杨晓，上海市高可信计算重点实验室 (华东师范大学), 上海 20006211,王小齐，上海市高可信计算重点实验室 (华东师范大学), 上海 20006202,陈小红，上海市高可信计算重点实验室 (华东师范大学), 上海 20006203,金芝，高可信软件技术教育部重点实验室(北京大学), 北京 100871;北京大学 计算机学院, 北京 10087104

关键词：复杂嵌入式系统;需求一致性;组合验证

形式化方法在需求一致性验证领域已经取得了显著的成就. 然而, 随着嵌入式系统需求复杂度的不断提升, 需求一致性验证面临着状态空间过大的挑战. 为了有效约减验证的状态空间, 同时考虑到嵌入式系统需求所涉及的设备强依赖性, 提出一种复杂嵌入式系统需求一致性的组合验证方法. 它基于需求分解, 识别需求间的依赖关系, 通过这些依赖关系组装验证子系统, 从而实现对复杂嵌入式系统需求的组合验证, 并能初步定位到不一致的需求. 具体而言, 采用问题框架方法对需求进行建模和分解, 并预设领域设备知识库对设备的物理特性进行建模. 在验证子系统的组装过程中, 生成预期软件的行为模型, 并结合物理设备的模型进行动态组装. 最后, 采用航空领域机载侦查系统进行了实例研究, 验证了方法的可行性和有效性, 并通过5个案例评估证实了验证状态空间的显著减小. 此方法为复杂嵌入式系统需求的验证提供了一种切实可行的解决方案.

来源：2025年第4期

《软件学报》期刊编辑部

查看软件学报杂志2025年第4期