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

doi:10.1109/MAES.2023.3238378

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 journal › Article › peer-review

Abstract

Developments in autonomous aircraft, such as <italic>electrical vertical take-off and landing</italic> (eVTOL) vehicles and multicopter drones, raise safety-critical concerns in populated areas. This article presents the ASSURE (<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> (IoP) infrastructure.

Original language	English (US)
Pages (from-to)	1-14
Number of pages	14
Journal	IEEE Aerospace and Electronic Systems Magazine
DOIs	https://doi.org/10.1109/MAES.2023.3238378
State	Accepted/In press - 2023

Keywords

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

Online availability

10.1109/MAES.2023.3238378

Cite this

@article{a9b09d6200784edda45e51a86a23363d,

title = "Formal Verification of Safety-Critical Aerospace Systems",

abstract = "Developments in autonomous aircraft, such as electrical vertical take-off and landing (eVTOL) vehicles and multicopter drones, raise safety-critical concerns in populated areas. This article presents the ASSURE (Analysis of Safety-Critical Systems Using Formal Methods-Based Runtime Evaluation) 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 proof libraries, and a data-driven runtime verification approach for aerospace systems towards a provably safe Internet of Planes (IoP) infrastructure.",

keywords = "Aerospace and electronic systems, Aerospace electronics, Aerospace safety, Aircraft, Cognition, distributed systems, Runtime, runtime verification, Software, stochastic systems, theorem proving",

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

note = "Publisher Copyright: IEEE",

year = "2023",

doi = "10.1109/MAES.2023.3238378",

language = "English (US)",

pages = "1--14",

journal = "IEEE Aerospace and Electronic Systems Magazine",

issn = "0885-8985",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - JOUR

T1 - Formal Verification of Safety-Critical Aerospace Systems

AU - Paul, Saswata

AU - Cruz, Elkin

AU - Dutta, Airin

AU - Bhaumik, Ankita

AU - Blasch, Erik

AU - Agha, Gul

AU - Patterson, Stacy

AU - Kopsaftopoulos, Fotis

AU - Varela, Carlos

N1 - Publisher Copyright: IEEE

PY - 2023

Y1 - 2023

N2 - Developments in autonomous aircraft, such as electrical vertical take-off and landing (eVTOL) vehicles and multicopter drones, raise safety-critical concerns in populated areas. This article presents the ASSURE (Analysis of Safety-Critical Systems Using Formal Methods-Based Runtime Evaluation) 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 proof libraries, and a data-driven runtime verification approach for aerospace systems towards a provably safe Internet of Planes (IoP) infrastructure.

AB - Developments in autonomous aircraft, such as electrical vertical take-off and landing (eVTOL) vehicles and multicopter drones, raise safety-critical concerns in populated areas. This article presents the ASSURE (Analysis of Safety-Critical Systems Using Formal Methods-Based Runtime Evaluation) 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 proof libraries, and a data-driven runtime verification approach for aerospace systems towards a provably safe Internet of Planes (IoP) infrastructure.

KW - Aerospace and electronic systems

KW - Aerospace electronics

KW - Aerospace safety

KW - Aircraft

KW - Cognition

KW - distributed systems

KW - Runtime

KW - runtime verification

KW - Software

KW - stochastic systems

KW - theorem proving

UR - http://www.scopus.com/inward/record.url?scp=85147265739&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85147265739&partnerID=8YFLogxK

U2 - 10.1109/MAES.2023.3238378

DO - 10.1109/MAES.2023.3238378

M3 - Article

AN - SCOPUS:85147265739

SN - 0885-8985

SP - 1

EP - 14

JO - IEEE Aerospace and Electronic Systems Magazine

JF - IEEE Aerospace and Electronic Systems Magazine

ER -

Formal Verification of Safety-Critical Aerospace Systems

Abstract

Keywords

ASJC Scopus subject areas

Online availability

Related links

Fingerprint

Cite this