Model Checking for Formal Verification of Space Systems

To develop a tool-supported workflow capable of formally specifying and then verifying properties on a system based on its behavioral description, in order to allow system and software engineers to make early verification of their models and to automate the production of test cases 

Interest for MBSSE (Model-based system and software engineering) is growing as the complexity of missions becomes difficult to manage with traditional development approaches.;Existing technology allows to address a large spectrum of the MBSSE scope, from data modelling to automatic code generation. However, much more concrete and quantifiable benefits shall come from automated system verification and testing.;Some MBSSE principles can be and are currently deployed on operational projects to various degrees. To become more useful as an analysis tool at system level, the development processes shall be complemented with an engine supporting the verification of system functional properties, as well as the generation of test cases. A tool can make some guarantees regarding the system coverage (exhaustiveness) and the resource usage efficiency (uniqueness).;Research and development are still necessary as this technology mostly only exists as laboratory prototypes used in universities.;The proposed tasks are the following:1) Identify the workflow, including benefits and limitations for using model checking and automatic test generation in an operational context2) Analyze existing academic model checking tools (Uppaal, Spin, nusmv?) and extract the desired features for designing a more generic engine that can work with industrial languages applicable to the space domain (SDL, ASN.1)3) Design the process for defining and capturing properties to be verified on a system behavioral model4) Implement the core engine that can analyze models in order verify the given properties and generate test cases in an automatic manner5) Assess the benefits of the proposed workflow and produce recommendations for future developments in the areaSoftware shall be delivered under an ESA Software Community Licence, so that any individuals or entities within ESA Member States can access to it and can provide update to the community of users.;