Verification and Validation of Real-Time Optimised Safety-Critical GNC SW Systems

The package includes the software deliverables developed under European Space Agency’s Technology Development Element (TDE) programme (ESA contract No. 4000136721/21/NL/CRS “Verification and validation of real-time optimised safety-critical GNC SW systems”). This study was led by GMV Portugal in partnership with Thales Alenia Space France, ENAC (Ecole Nationale de l'Aviation Civile), and IMTEK-SYSCOP (Institut für Mikrosystemtechnik - Systems Control and Optimization Laboratory of the University of Freiburg). The released software data pack contains:

• Simulators for the application of optimization-based control systems for space problems
• Conic optimization solver
• Verification and validation procedures

Further details regarding this activity can be found below.

Background and justification:

• In-space autonomy is a critical component in the design of upcoming missions, from re-entry and launch vehicles, deep space probes, constellations, space robotics (on-orbit servicing, manufacturing and assembly), or agile spacecraft.
• On-board optimisation in real-time is a fundamental building block of fully autonomous space operations.
• Developing methods to prove that these algorithms can fly safely, reliably, and efficiently on space-grade avionics is paramount for their adoption.

Objectives:

• Develop and validate a framework for the verification and validation (V&V) of GNC systems based on embedded optimisation.
• Augment the traditional GNC Design & Development Verification & Validation methodologies to explicitly address iterative embedded optimisation.
• Consolidate the necessary tools for prototyping and qualification of G&C software, grounded on theoretical foundations for optimisation and V&V.

Achievements and status:

• Extensive survey and definition of available techniques to employ convex optimisation in typical GNC applications.
• Design, development, and formal specification of a state-of-the-art embedded and auto-codable conic optimisation solver.
• Demonstration of formal specification and execution of a C-code implementation of the solver paving the way to executable formal specification.
• Application of convex optimisation to relevant benchmark problems, in particular, far- and close-range rendezvous tackling obstacle avoidance.
• Extension of traditional V&V to address local math-driven compositional verification of the optimisation solver.
• Auto-coding, software-in-the-loop and processor-in-the-loop testing of the developed algorithms (and underlying solver) on a space-grade processor.

Benefits:

• The V&V process devised in the activity is a cornerstone to an enhanced verification of critical software essential to complex upcoming missions.
• Convex optimisation algorithms are useful: 1) due to performance and safety improvements over traditional methods; and 2) since they are a convenient tool to address heritage-less applications.