Formal verification of space systems designed with TASTE

TL;DR

This paper presents a formal verification approach for space systems designed with TASTE, a model-based engineering toolset, using the IF model-checker to ensure system correctness against specified properties.

Contribution

It introduces a novel method integrating the IF model-checker with TASTE for formal verification of space system designs, addressing a previously open challenge.

Findings

Successful integration of IF model-checker with TASTE

Verification of properties on space system models

Under development in ESA MoC4Space project

Abstract

Model-Based Systems Engineering (MBSE) is a development approach aiming to build correct-by-construction systems, provided the use of clear, unambiguous and complete models to describe them along the design process. The approach is supported by several engineering tools that automate the development steps, for example the production of code, documentation, test cases and more. TASTE [1] is pragmatic MBSE toolset supported by ESA that encapsulates several technologies to design a system (data modelling, architecture modelling, behaviour modelling/implementation), to automatically generate the binary application(s), and to validate it. One topic left open in TASTE is the formal verification of a system design with respect to specified properties. In this paper we describe our approach based on the IF model-checker [4] to enable the formal verification of properties on TASTE designs. The approach is currently under development in the ESA MoC4Space project.