ESA Open Invitation to Tender AO10416
Open Date: 14/08/2020
Closing Date: 09/10/2020 13:00:00

Status: ISSUED
Reference Nr.: 20.132.05
Prog. Ref.: Technology Developme
Budget Ref.: E/0901-01 – Technology Developme
Special Prov.: BE+DK+FR+DE+IT+NL+ES+SE+CH+GB+IE+AT+NO+FI+PT+GR+LU+CZ+RO+PL+EE+HU
Tender Type: C
Price Range: 200-500 KEURO
Products: Satellites & Probes / System Engineering Software / System Modelling & Simulation / Modelling tools (Model development, Non real-time execution, Code generation, …)
Technology Domains: Space System Software / Advanced Software Technologies / Advanced Software Development Methods and Tools
Establishment: ESTEC
Directorate: Directorate of Tech, Eng. & Quality
Department: Systems Department
Division: Software Systems Division
Contract Officer: Seynaeve, Christophe Rene R.
Industrial Policy Measure: N/A – Not apply
Last Update Date: 14/08/2020
Update Reason: Tender issue

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 MBSSEscope, from data modelling to automatic code generation. However, much more concrete and quantifiable benefitsshall 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:- Identify the workflow, including benefits and limitations for using model checking and automatic test generation in an operational context- Analyse existing academic model checking tools (Uppaal, Spin, nusmv) and extract the desired featuresfor designing a more generic engine that can work with industrial languages applicable to the space domain (SDL, ASN.1)- Design the process for defining and capturing properties to be verified on a system behavioral model- Implement the core engine that can analyse models in order verify the given properties and generate test cases in an automatic manner- 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.