ESA GNC Conference Papers Repository

VV4RTOS is an activity supported by the European Space Agency aimed at the development and validation of a framework for the verification and validation of spacecraft guidance, navigation, and control (GNC) systems based on embedded optimisation, tailored to handle different layers of abstraction, from guidance and control (G&C) requirements down to hardware level. This is grounded on the parallel design and development of real-time optimisation-based G&C software, allowing to concurrently identify, develop, consolidate, and validate a set of engineering practices and analysis & verification tools to ensure safe code execution of the designed G&C software as test cases but aimed at streamlining general industrial V&V processes. This paper presents: 1) a review of the challenges and the state-of-the-art of formal verification methods applicable to optimization-based software; 2) the implementation for an embedded application and the analysis from a V&V standpoint of a conic optimization solver; 3) the technical approach devised towards and enhanced V&V process; and 4) experimental results up to processor-in-the-loop tests and conclusions. In general, this activity aims to contribute to the widespread usage of convex optimisation-based techniques across the space industry by 1) augmenting the traditional GNC software Design & Development Verification & Validation (DDVV) methodologies to explicitly address iterative embedded optimisation algorithms that are paramount for the success of new and extremely relevant space applications (from powered landing to active debris removal, from actuator allocation to attitude guidance & control) guaranteeing safe, reliable, repeatable, and accurate execution of the SW; and 2) consolidating the necessary tools for the fast prototyping and qualification of G&C software, grounded on strong theoretical foundations for the solution of convex optimisation problems generated by posing, discretization, convexification, and transcription of nonlinear nonconvex optimal control problems to online-solvable optimisation problems. Sound guidelines are provided for the high-to-low level translation of mission requirements and objectives aiming at their interfacing with verifiable embedded solvers tailored for the underlying hardware and exploiting the structure present in the common optimisation/optimal control problems. To fulfil this mandate, two avenues of research and development were followed: the development of a benchmarking framework with optimisation-based G&C and the improvement of the V&V process – two radical advances with respect to traditional GNC DDVV. On the first topic, the new optimisation-based hierarchy was exploited, from high-level requirements and objectives that can be mathematically posed as optimal control problems, themselves organised in different levels of abstraction, complexity, and time-criticality depending on how close to the actuator level they are. The main line of this work is then focused on the core component of optimisation-based G&C – the optimisation solver – starting with a formal analysis of its mathematical properties that allowed to identify meaningful requirements for V&V, and, concurrently, with a thorough, step-by-step, design and implementation for embedding in a space target board. This application-agnostic analysis and development was associated with the DDVV of specific usecases of optimisation-based G&C for common space applications of growing complexity, exploring different challenges in the form of convex problem complexity (up to second-order cone programs), problem size (model predictive control and trajectory optimization), and nonlinearity (both translation and attitude control problems). The novel V&V approach relies on the combination and exploitation of the two main approaches: classical testing of the global on-board software, and local and compositional, formal, math-driven, verification. While the former sees systems as black boxes, feeding it with comprehensive inputs and analysing statistically the outputs, the latter delves deep into the sub-components of the software, effectively seeing it as white boxes whenever mathematically possible. In between the two approaches lies the optimal path to a thorough, dependable, mathematically sound verification and validation process: local, potentially application-agnostic, validation of the building blocks with respect to mathematical specifications leading up to application-specific testing of global complex systems, this time informed by the results of local validation and testing. The deep analysis of the mathematical properties of the optimisation algorithm allows to derive requirements with increasing complexity (e.g., from “the code implements the proper computations”, to higher level mathematical properties such as optimality, convergence, and feasibility). These are related to quantities of interest that can be both verified resorting to e-ACSL specifications and Frama-C in a C-code implementation of the solver, but also observed in online monitors in Simulink or in post-processing during the model/software-in-the-loop testing. Finally, the activity applies the devised V&V process to the benchmark designs, from model-in-the-loop Monte Carlo testing, followed by autocoding and software-in-the-loop equivalence testing in parallel with the Frama-C runtime analysis, and concluded by processor-in-the-loop testing in a Hyperion on-board computer based around a Xilinx Zynq 7000 SoC.