航空航天
形式验证
形式化方法
计算机科学
运行时验证
不确定性算法
模型检查
生命关键系统
正式规范
软件验证
自动定理证明
软件
系统工程
软件工程
软件系统
工程类
程序设计语言
算法
航空航天工程
软件建设
作者
Saswata Paul,Elkin Cruz-Camacho,Airin Dutta,Ankita Bhaumik,Erik Blasch,Gul Agha,Stacy Patterson,Fotis Kopsaftopoulos,Carlos A. Varela
出处
期刊:IEEE Aerospace and Electronic Systems Magazine
[Institute of Electrical and Electronics Engineers]
日期:2023-01-25
卷期号:38 (5): 72-88
被引量:10
标识
DOI:10.1109/maes.2023.3238378
摘要
Developments in autonomous aircraft, such as electrical vertical take-off and landing vehicles and multicopter drones, raise safety-critical concerns in populated areas. This article presents the Analysis of Safety-Critical Systems Using Formal Methods-Based Runtime Evaluation (ASSURE) framework, which is a collection of techniques for aiding in the formal verification of safety-critical aerospace systems. ASSURE supports the rigorous verification of deterministic and nondeterministic properties of both distributed and centralized aerospace applications by using formal theorem proving tools. We present verifiable algorithms and software, formal reasoning models, formal proof libraries, and a data-driven runtime verification approach for aerospace systems toward a provably safe Internet of Planes infrastructure.
科研通智能强力驱动
Strongly Powered by AbleSci AI