摘要
本文提出了一种以认证为导向的方法，用于无人机系统设计中的需求管理及模型验证。该方法旨在解决那些包含自行开发的硬件和软件组件的关键安全无人机平台的认证难题。该框架将需求工程、功能危险分析以及形式化模型验证整合到一个统一的设计与验证工作流中。文中还介绍了对系统需求进行分类、排序和分解的方法，以助力开发可靠的无人机软件及操作流程。此外，还提出了一种系统化的方法，用于将认证要求及功能危险分析的安全功能与无人机操作场景及系统用例相对应，从而实现安全要求、系统行为与验证结果之间的可追溯性。该框架采用统一建模语言的状态机模型，并通过线性时序逻辑和计算树逻辑对其进行分析验证。模型验证则借助NuSMV符号模型检查器来完成，以此评估操作场景在正确性、完整性、一致性及安全性方面的表现。一个关于无人机在地面控制站之间交接的实际案例研究展示了该方法的实用性。分析结果表明，操作模型中存在一些不一致之处，而形式化验证有助于及时发现不安全或不完整的系统行为。综上所述，该方法通过提升需求的可追溯性、减少验证中的模糊性，并简化关键飞行控制流程的验证工作，为开发符合认证标准的无人机系统提供了有力支持。
