.png){kind=icon}
返回
Certification-Oriented Requirements and Model Verification Methodology for UAV Systems
.png){kind=icon}
OA
AI
DOI：10.3390/drones10070555.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
本文提出了一种面向认证的方法论，用于无人机（UAV）系统的需求管理及模型验证设计。该方法解决了认证安全关键型UAV平台所面临的挑战，这些平台的架构包含定制开发的硬件和软件组件。该方法论将需求工程、功能危险分析（FHA）和形式化模型验证整合为一个统一的设计与验证工作流程。文中介绍了对系统需求进行分类、优先级排序和分解的方法，以支持可靠UAV软件和操作流程的开发。引入了一种将认证需求与FHA安全功能映射到UAV操作场景和系统用例的系统化方法，实现了安全需求、系统行为和验证工件之间的可追溯性。所提出的框架采用统一建模语言（UML）状态机模型，并使用线性时态逻辑（LTL）和计算树逻辑（CTL）进行验证。模型验证通过NuSMV符号模型检查器执行，以评估操作场景的正确性、完整性、一致性和安全属性。一个关于地面控制站（GCS）之间UAV交接的实践案例研究证明了所提出方法的应用性。分析识别了操作模型中的不一致性，并展示了形式化验证如何支持对不安全或不完整的系统行为进行早期检测。所提出的方法通过提高需求可追溯性、减少验证模糊性以及促进安全关键型飞行控制流程的验证，支持开发符合认证要求的UAV系统。
Keyword:
unmanned aerial vehicle (UAV) certification
requirements management
airworthiness
functional hazard analysis (FHA)
safety-critical systems
model-based design
formal verification
linear temporal logic (LTL)
computation tree logic (CTL)
NuSMV
期刊
D
IF:
4.8
论文数:
3.9K
被引数:
8.3K
机构
引用论文
分享收藏X-RMTV: An Integrated Approach for Requirement Modeling, Traceability Management, and Verification in MBSE.png)
Systems
SystemsIF0
PREAI
分享收藏Model-based test case generation from UML sequence diagrams using extended finite state machines
PREAI
分享收藏Formal Modelling and Verification of Multi-Parameter Context and Agent Transition Systems: Application to Urban Delivery Zone and Autonomous Electric Vehicle多参数上下文与智能体转换系统的形式化建模与验证：在城区配送区域和自主电动车辆中的应用
OAAI
OAAI分享收藏Verification of the Protection Services in Antivirus Systems by Using Nusmv Model Checker使用NuSMV模型检查器验证杀毒系统中的保护服务
PREAI
分享收藏分享收藏
查看更多内容