Functional Requirements and Verification Techniques for the Software Reference Architecture
Funding programme ESA ESTEC
Partners Thales Alenia Space, France, Fondazione Bruno Kessler
Description The main objective of the FoReVer study was to develop methodological, theoretical and technological support for a systematic approach to space avionics system development, across ECSS phases 0, A, B and C.
The focus was to define an integrated methodology and supporting toolset relying on a model-based approach and to introduce formal verification of system properties from the early stages of the development process, allowing checks for the correctness of model refinements and enabling full traceability of design choices along the whole development process.
The target of the study was then the refinement of the avionics system level properties down to the software level reusing software components implemented in the On-Board Software Reference Architecture (OBSW-RA) defined in the context of the SAVOIR initiative for space avionics standardization of ESA. FoReVer takes advantage of the CHESS model-driven toolset (https://www.polarsys.org/chess/) and integrates the OCRA advanced tool developed by FBK to support contract based reasoning and verification of logic-based contracts refinement.
Links Official project website
Intecs The Brainware company