摘要:随着机载控制系统技术的快速进步,确保机载软件的可靠性、稳健性和适应性已变得势在必行,因为这些软件的故障可能导致灾难性的财产和生命损失。DO-333 是 DO-178C 标准的补充,致力于指导形式化方法在机载软件开发过程的审查和分析中的应用。然而,DO-333 缺乏关于如何在验证过程的每个阶段选择合适的形式化方法和工具来实现验证目标的理论指导,从而限制了它们的实际应用。本文旨在说明验证过程中可用的形式化方法和工具,为机载软件的形式化开发和验证提供一般指南。以大气数据计算机(ADC)软件为研究对象,应用不同的形式化方法来验证软件生命周期工件。本例说明了形式化方法在实际应用中的应用,并证明了形式化方法在机载软件验证中的有效性。
主要关键词