Iulian Ober

I Dragomir, M Bozga, Iulian Ober et al.

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.

Guillaume Vidot, Christophe Gabreau, Ileana Ober et al.

Advances in machine learning (ML) open the way to innovating functions in the avionic domain, such as navigation/surveillance assistance (e.g. vision-based navigation, obstacle sensing, virtual sensing), speechto-text applications, autonomous flight, predictive maintenance or cockpit assistance. Current certification standards and practices, which were defined and refined decades over decades with classical programming in mind, do not however support this new development paradigm. This article provides an overview of the main challenges raised by the use ML in the demonstration of compliance with regulation requirements, and a survey of literature relevant to these challenges, with particular focus on the issues of robustness and explainability of ML results.

Ronan Baduel, Iulian Ober, Jean-Michel Bruel

This paper presents the results achieved while pursuing the verification and validation of a train system behavior at the first steps of development in an industrial context. A method is proposed, supported by preliminary results through the definition and verification of constrained states and preconditions to use cases, as well as a structure for the behavior.