IEEE - Aerospace and Electronic Systems - May 2023 - 72

Feature Article:
DOI. No. 10.1109/MAES.2023.3238378
Formal Verification of Safety-Critical Aerospace
Systems
Saswata Paul , Elkin Cruz, Airin Dutta, and Ankita Bhaumik, Rensselaer
Polytechnic Institute, Troy, NY 12180 USA
Erik Blasch
, Air Force Research Laboratory, Rome, NY 13441 USA
Gul Agha, University of Illinois Urbana-Champaign, Champaign,
IL 61801 USA
Stacy Patterson , Fotis Kopsaftopoulos , and Carlos Varela, Rensselaer
Polytechnic Institute, Troy, NY 12180 USA
INTRODUCTION
The rapid advancement in the field ofautonomous aircraft
has revolutionized scientific data collection, package
delivery, disaster relief, agriculture surveillance, weather
tracking, and passenger transportation. As autonomous
aircraft technologies evolve to become more accessible
and cost-efficient, it will become necessary to rigorously
verify their performance to guarantee that they will operate
safely, securely, and efficiently.
MOTIVATION
Aerospace systems are safety-critical and errors in aerospace
operations such as flight control and navigation can be catastrophic.
Recently, there were two fatal accidents involving
the Boeing 737 Max 8 series of aircraft-Lion Air flight 610
on 29 October 2018 (189 fatalities) and Ethiopian Airlines
flight 302 on 10 March 2019 (157 fatalities). These were
caused by failing sensors sending erroneous data to
Authors' current address: Saswata Paul, ElkinCruz, Ankita
Bhaumik, Stacy Patterson, and Carlos Varela are with the
Department of Computer Science, Rensselaer Polytechnic
Institute, Troy, NY 12180 USA (e-mail: paulsaswata1@
gmail.com). Airin Datta and Fotis Kopsaftopoulos arewith
the Department of Mechanical, Aerospace, and Nuclear
Engineering, Rensselaer Polytechnic Institute, Troy, NY
12180USA. Erik Blasch is with theAir ForceResearchLaboratory,
Rome, NY 13441 USA. Gul Agha is with the
Department of Computer Science, University of Illinois
Urbana-Champaign,Champaign, IL 61801 USA.
Manuscript received 18 February 2022, revised 11 June
2022; accepted 16 January 2023, and ready for
publication 25 January 2023.
Review handled by Roberto Sabatini.
0885-8985/23/$26.00 ß 2023 IEEE
72
the Maneuvering Characteristics Augmentation System
(MCAS), which is a flight stabilization software designed to
automatically prevent aircraft from stalling during flight by
adjusting the angle of attack (AoA) (see Figure 1) [1]. Similarly,
navigational errors can lead to mid-air collisions, such as
in 2002 at €Uberlingen [2], where a Boeing 757 cargo jet and a
Tupolev Tu-154 passengerjet collidedmid-air (Figure 2) causing
69 fatalities, and the mid-air collision involving a Cirrus
SR-22 airplane and a Swearingen Metroliner airplane near
Centennial Airport, Denver, CO, USA, in May 2021 [3].
Figure 1.
Boeing's MCAS system's failure.
IEEE A&E SYSTEMS MAGAZINE
MAY 2023

https://orcid.org/0000-0002-1792-9858 https://orcid.org/0000-0001-6894-6108 https://orcid.org/0000-0001-7711-6018 https://orcid.org/0000-0001-8795-3725

IEEE - Aerospace and Electronic Systems - May 2023

Table of Contents for the Digital Edition of IEEE - Aerospace and Electronic Systems - May 2023