Model Checking for Formal Verification of Space Systems
Programme
TDE
Programme Reference
T702-601SW
Prime Contractor
N7 Space
Start Date
End Date
Status
Contracted
Country
Poland

Objectives
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
Description
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 context
2) 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 model
4) Implement the core engine that can analyze models in order verify the given properties and generate test cases in an automatic manner
5) Assess the benefits of the proposed workflow and produce recommendations for future developments in the area
Software 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.
;
Application Domain
Generic Technologies
Technology Domain
2 - Space System Software
Competence Domain
3-Avionic Systems
Keywords
40-Design to Produce
Initial TRL
TRL 2
Target TRL
TRL 3
Achieved TRL
TRL 3