You are here


The Mechanical Automation Integration System is an ambitious project aimed at the development of a platform for the automatic control of electroplating plants. We discovered that for this project, the combination of the planning and the scheduling sub-problems was intractable for existing domain-independent planers.  In the project we developed a very efficient domain-dependent planner in which we coded the knowledge gained from extensive discussions with domain experts.

The VMT format is an extension of the SMT-LIBv2 (SMT2 for short) format to represent symbolic transition systems. VMT exploits the capability offered by the SMT2 language of attaching annotations to terms and formulas in order to specify the components of the transition system and the properties to verify.

The COMPASS Project is an international research project for developing a theoretical and technological basis for the system-software co-engineering approach focusing on a coherent set of specification and analysis techniques for evaluation of system-level correctness, safety, dependability and performability of on-board computer-based aerospace systems. These techniques shall significantly improve the reliability of modern and future space missions.

The ESA AUTOGEF (Dependability Design Approach  for Critical Flight Software) study is a direct follow-on  of the ESA TRP COMPASS (Correctness, Modelling  and Performance of Aerospace Systems).

AUTOGEF aims to demonstrate that synthesis  approaches can allow for effective automated FDIR development in accordance with the dependability requirements, through the implementation of an add-on
to the COMPASS tool.

The FAME Project is an international research project for developing an FDIR (Fault-Detection, Fault-Isolation and Recovery) development and Verification & Validation process.

The global objective of this study is to identify a dedicated FDIR Development and V&V Process in order to address the issues and shortcomings in the current industrial FDIR development practices and to allow for the consistent and timely FDIR conception, development, and Verification & Validation.

HASDEL (Hardware Software Dependability for Launchers) is an ESA project, conducted by a consortium coordinated by Airbus Defence and Space with FBK and RWTH, aiming at analysing the specific needs of launcher systems in the domain of RAMS (Reliability, Availability, Maintainability and Safety) analysis and at extending the COMPASS (Correctness, Modelling and Performance of Aerospace Systems) toolset with these specific needs

The Innovative Rover Operations Concepts – Autonomous Planning (IRONCAP) is an ESA study project to explore and define the concepts and interactions needed to control and plan the activities of an interplanetary rover. Its aim is to develop a prototype system to support the science and engineering planning of an interplanetary rover using stateof-the-art methods and techniques in planning and scheduling combined with existing and/or developing ground segment systems and technologies. 

In the framework of the European Space Agency's Networking/Partnering Initiative (NPI) a PhD research project was organized by ESA and the Embedded Systems Unit of FBK on the topic of model-based tools to support formal design of fault management architectures. The work was performed by the PhD student Benjamin Bittner, under supervision of Alessandro Cimatti and Marco Bozzano on FBK side and Marcel Verhoef on ESA side.

CITADEL will build on the MILS technology accomplishments of D-MILS and Euro-MILS, and perform the research and development necessary to create adaptive MILS systems.
We propose to use adaptive MILS in new and evolving adaptive systems contexts having strategic focus within the EU, such as Critical Infrastructures and the Internet of Things, where adaptability is a crucial ingredient for the safety and security of future systems, and where the rigorous construction and verification made possible by MILS holds particular promise.

A joint scientific study, funded by Evidence, will investigate the formal verification of safety properties of embedded software.