Skip to main content

Formal verification of safety-critical aerospace systems

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.

Reference

Paul S., Cruz-Camacho E., Dutta A., Bhaumik A., Blasch E., Agha G., Patterson S., Kopsaftopoulos F., Varela C.,, "Formal verification of safety-critical aerospace systems ,"

S. Paul et al., "Formal Verification of Safety-Critical Aerospace Systems," in IEEE Aerospace and Electronic Systems Magazine, vol. 38, no. 5, pp. 72-88, 1 May 2023, doi: 10.1109/MAES.2023.3238378. keywords: {Aircraft;Aerospace safety;Aerospace electronics;Software;Runtime;Cognition;Aerospace and electronic systems;Autonomous aerial vehicles;theorem proving;runtime verification;stochastic systems;distributed systems},

View Publication

Bibtex

@ARTICLE{10025818,
  author={Paul, Saswata and Cruz, Elkin and Dutta, Airin and Bhaumik, Ankita and Blasch, Erik and Agha, Gul and Patterson, Stacy and Kopsaftopoulos, Fotis and Varela, Carlos},
  journal={IEEE Aerospace and Electronic Systems Magazine}, 
  title={Formal Verification of Safety-Critical Aerospace Systems}, 
  year={2023},
  volume={38},
  number={5},
  pages={72-88},
  keywords={Aircraft;Aerospace safety;Aerospace electronics;Software;Runtime;Cognition;Aerospace and electronic systems;Autonomous aerial vehicles;theorem proving;runtime verification;stochastic systems;distributed systems},
  doi={10.1109/MAES.2023.3238378}}