Home >> R&D >> FoReVer



Functional Requirements and Verification Techniques for the Software Reference Architecture

Funding Programme





Fondazione Bruno Kessler (I), Thales Alenia Space (F).

Start Date

January 2012


15 months


The overall objective of the project is to provide a guideline on the systematic approach of verification of (functional and non functional) avionics system level properties around Model Driven Engineering at system, avionics and software level for the Space Flight and the development of technologies, methodologies and the description and implementation of the architectural impact on the SAVOIR-FAIRE Software Reference Architecture to support and ease the verification of properties identified at system, avionics and software level.

The objectives of the activity are in particular:

  1. Taxonomy of functional and non-functional avionics system level properties

  2. Provide an overview of verification methods, languages and tools for system, avionics and software properties

  3. Framework (Methodology and Process) for the verification of avionics system level properties (adequacy, information sources, link to formal verification methods and tools) and a description of a process for stepwise refinement of assumptions (from system down to software) based on an assumption/guarantee relationship. Identify missing gaps at process, methods and tools aspect.

  4. Identification of properties from higher level specification impacting the software system

  5. Derivation of architectural impact of avionics system level property verification on the design of the Software Reference Architecture (identification of design recommendations to ease verification and/or to enforce the properties)

  6. Identification of the associated tool set needed to verify the properties

  7. Performing a case study, demonstrating the General concept and the Software reference architecture related verification using an associated tool set