Formal Methods for Space Systems Engineering

The size and complexity of software in space systems is increasing exponentially, and this trend complicates its validation within the context of the overall system. With funding from the European Space Agency (ESA), we study and develop formal methods and tools for the rigorous design and validation of space systems.

Early Design Validation

In [MMK10], we proposed a Semantic Web Architecture for Model Based Safety Engineering of space systems. This research was funded by the ESA Greek Task Force (AO/1-5819/08/NL/CB) and was coordinated in collaboration with Gnomon Informatics S.A., TNI Europe Ltd Ellidiss and Thales Alenia Space - France as industrial partner.


The COMPASS consortium consisting of RWTH Aachen University, Fondazione Bruno Kessler and Thales Alenia Space - France developed in a parallel project a (semi-)automated model-driven validation approach and tool, for the analysis of requirements related to functional correctness, safety, dependability and performance. We participated in a large pilot project using the COMPASS toolset, which took place in ESA for a spacecraft in development. The results of this collaboration concern with the spacecraft early design validation and were published in [BCK14]. 

Schedulability Analysis Techniques & Tools for Cached and Multicore Processors

ESA has also funded a research and development study (AO/1-7646/13/NL/JK) in response to a need to understand how to make best use of the future multicore processors and to mitigate the risks, due to the software complexity inherent to their use in relation to the actual space system. Members of the DSG group coordinate this study within a consortium led by the Information Technologies Institute at the Centre for Research & Technology Hellas, including the Distributed and Complex Systems team at the VERIMAG Research Center (Grenoble), Aeroflex Gaisler AB (Goteborg) and the industrial partnership of Elecnor Deimos (Madrid). External engineering services and tools are provided by Rapita Systems Ltd (York).

In this study, we will utilize ESA's model-based techniques for distributed systems in the TASTE toolchain, and the RT-BIP component framework for rigorous system design to:

  • formally validate multicore systems' schedulability (related problems, e.g. interference on shared resources)
  • support deployment on multicore system nodes
  • automatically synthesize code from a validated system model
  • provide means to integrate various models of computation and scheduling approaches
  • support mixed-criticality scheduling.

Contact persons: Prof. Panagiotis Katsaros

Home | Projects | Publications | Partners | Related Links | News | People | Contact copyright � 2012 DSG group