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


Developments in autonomous aircraft, such as <italic>electrical vertical take-off and landing</italic>&#x00A0;(eVTOL) vehicles and multicopter drones, raise safety-critical concerns in populated areas. This article presents the ASSURE&#x00A0;(<italic/><bold>A</bold><italic>nalysis of</italic> <bold>S</bold><italic>afety-Critical</italic> <bold>S</bold><italic>ystems</italic> <bold>U</bold><italic>sing Formal Methods-Based</italic> <bold>R</bold><italic>untime</italic> <bold>E</bold><italic>valuation</italic>) 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 non-deterministic properties of both distributed and centralized aerospace applications by using formal theorem proving tools. We present verifiable algorithms and software, formal reasoning models, formal <italic>proof libraries</italic>, and a data-driven runtime verification approach for aerospace systems towards a provably safe <italic>Internet of Planes</italic>&#x00A0;(IoP) infrastructure.

Original languageEnglish (US)
Pages (from-to)1-14
Number of pages14
JournalIEEE Aerospace and Electronic Systems Magazine
StateAccepted/In press - 2023


  • Aerospace and electronic systems
  • Aerospace electronics
  • Aerospace safety
  • Aircraft
  • Cognition
  • distributed systems
  • Runtime
  • runtime verification
  • Software
  • stochastic systems
  • theorem proving

ASJC Scopus subject areas

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


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

Cite this