Search

Model-Based Software 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, such as the TASTE toolset. TASTE is a pragmatic and mature open-source toolset supported by European Space Agency that enables and provides automation for most of the phases of software system development: (i) heterogeneous system design through several modelling and programming languages, (ii) code generation, build and deployment of the binary application(s), and (iii) validation through static analysis and simulation. 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 to enable the formal verification of properties on TASTE designs, as well as the results obtained 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.