RUNVERSPACE

Runtime Verification for Space Software Architectures

Duration: 2024 - 2025 Funding: Swiss National Science Foundation (SNSF)

Recent technological advances have led to powerful and cost-effective on-board computers running software built with open frameworks targeting small-scale missions such as CubeSats and Unmanned Aerial Vehicles. While offering great flexibility, this also opens new potential sources of failures, posing challenges for requirements assurance as development may take place in fast cycles, at higher-levels of abstraction, across multiple teams and culminating into reusable component-based architectures.

RUNVERSPACE addresses the systematic engineering of contemporary small-scale flight- and space- software, arguing that integrating runtime verification facilities is crucial for increased operational requirements assurance. Addressing fundamental challenges of bringing such a goal to runtime has the potential of significant disruption. RUNVERSPACE is based on the premise that cutting-edge software engineering research leveraging applied formal methods is direly needed for the next generation of space applications. RUNVERSPACE will focus on defining suitable programming abstractions and specification notations in tandem with development of architectural support, with an overall goal of demonstrating the potential that runtime verification can bring.