Model-checking for TASTE designed space software systems: results and lessons learned

Model-Based Systems Engineering (MBSE) is an adopted modelling and development approach for correct-by- construction of complex software systems, such as space applications. TASTE [1] is a pragmatic and mature MBSE toolset supported by ESA that enables and provides automation for most of the phases of software system development: (i) heterogeneous system design through several modelling and programming languages (e.g., ASN.1, AADL, SDL, C/C++), (ii) code generation, build and deployment of the binary application(s), (iii) validation through static analysis and simulation, and (iv) formal verification of properties by model-checking. The formal verification capabilities have been recently added to the TASTE toolset in the ESA project Model-Checking for Formal Verification of Space Systems (MoC4Space) and validated on two real-life case studies. Within this paper we report on the results and lessons learned during the project.