Formal Verification of Safety-Critical Aerospace Systems

Saswata Paul, Elkin Cruz, Airin Dutta, Ankita Bhaumik, Erik Blasch, Gul Agha, Stacy Patterson, Fotis Kopsaftopoulos, Carlos Varela

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Pages (from-to)72-88
Number of pages17
JournalIEEE Aerospace and Electronic Systems Magazine
Volume38
Issue number5
DOIs
StatePublished - May 1 2023

Keywords

  • distributed systems
  • runtime verification
  • stochastic systems
  • theorem proving

ASJC Scopus subject areas

  • Aerospace Engineering
  • Space and Planetary Science
  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'Formal Verification of Safety-Critical Aerospace Systems'. Together they form a unique fingerprint.

Cite this