计算机研究与发展

作者：黄益柯,阮锟,陈小红,金芝,

关键词：需求建模, 形式化验证, 需求工程, 机载系统, 设备模型,

机载系统在航空航天领域起着至关重要的作用，其突出的安全性使得软件需求的形式化验证成为一个非常重要的问题.但是随着机载系统需求复杂度和设备数量的增加，其形式化验证中出现了状态空间爆炸的问题.为了缓解该问题，提出了一种机载系统需求的建模与分时组合验证方法.这种方法通过利用时间维度，将复杂的验证系统分解为相互独立的组件，实现了对各组件的独立验证，进而综合出整个系统的验证结果.通过实际的案例研究，证明了该方法的可行性.并通过评估说明该方法不但可以验证一些传统单体验证不能验证的系统，缓解状态空间爆炸，而且可以避免不考虑分时所造成的误报.这一方法为机载系统的软件需求验证提供了一种新的技术途径，有助于提高验证的准确性和效率，确保机载系统的安全性.

来源：2025年第9期

《计算机研究与发展》期刊编辑部

查看计算机研究与发展杂志2025年第9期