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 | |
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