Current projects

COMPASTA

The goal of COMPASTA is to integrate the COMPASS toolset with TASTE. COMPASS is a toolset for...

Read More

AIPlan4EU

Automated Planning and Scheduling is a central research area in AI that has been studied since the...

Read More

HUBCAP

The HUBCAP project aims at establishing a cloud-based center of innovation and collaboration among...

Read More

Bosch-FBK collaboration

A joint scientific study, funded by Bosch, will investigate the application of safety contracts and safety assessment techniques based on formal methods to the design process of Bosch with the goal of demonstrating their usefulness and suitability in the automotive domain.

Read More

X.Loader 4.0

Design and development of a robotic manipulator. Recognizing objects within boxes, planning...

Read More

Autonomous Reasoning Engine for Subsea Robotic System

This project is part of a key workstream activity of the company financing this activity which aims at changing the paradigm of underwater inspections and interventions via a fleet of next-generation drones and advanced ancillary equipments.

Within this project the ES unit will design and develop the Autonomous Reasoning Engine for the subsea robotic platform of the company:

Planning and scheduling for onboard autonomy and for on-ground mission planning
Plan validation (on-board and on-ground)
Plan execution and monitoring
The deployed solutions will allow for on-ground and on-line autonomy functionalities.

Read More

UAV-RETINA

Unmanned Air Vehicles (UAVs) are used to help in search and rescue of people lost in natural...

Read More

CITADEL

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.

Read More

Catsy – Catalogue of System Properties

The CATSY (Catalogue of System and Software Properties) project aims to improve the early verification and validation (V&V) activities by providing new methods to formalise requirements and validate the formal properties.

Read More

HASDEL – Hardware-Software Dependability for Launchers

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

Read More

PhD Collaboration with European Space Agency

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.

Read More

EURAILCHECK ERA – Formalization and Validation of ETCS

The European Train Control System (ETCS) is a control system for the interoperability of the railways across Europe. The EuRailCheck project was promoted by the European Railway Agency for the development of a methodology and tools for the formalization and validation of the ETCS specifications. Within the project, we achieved three main results. First, we developed a methodology for the formalization and validation of the ETCS specifications.

Read More

OMC-ARE – On board Model Checking Autonomous Resoning Engine

The project aims at proposing an approach to on-board autonomy, based on model-based reasoning. The approach integrates many important functionalities (such as plan generation, plan execution and monitoring, fault detection identification and recovery (FDIR), and run-time diagnosis) in a uniform framework.

Read More

COCONUT – A Correct-by-Construction Workbench for Design and Verification of Embedded Systems

The project focuses on the definition of a formal framework based on a tight integration of design and verification through all refinement steps of an embedded platform design flow, from specifications to logic synthesis and software compilation. In particular, it is intended to propose a modelling and verification flow to enhance and speed-up embedded platform design and configuration with particular regard to application fields related to mixed continuous/discrete models, like for example networked multimedia and sensor network managing.

Read More

FAME – FDIR Development and Verification & Validation Process

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.

Read More

CASTORONE

The project was financed by an oil-and-gas company for the realization of a planner for a pipelaying vessel. The task of the planner is to organize the work onboard the pipelaying ship where precise timing and ordering of operations are needed for the construction of an undersea pipe. Within this project we designed a domain-dependent planner to cope with huge size of the planning problems to be addressed. The resulting planner leverages the structure of the ship to quickly find plans for nominal and off-nominal situations.

Read More

IRONCAP – Innovative Rover Operations Concept – Autonomous Planning

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.

Read More

Verification Modulo Theories

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.

Read More

D-MILS

Modern critical systems bear great responsibilities and face escalating challenges. Distributed...

Read More

COMPASS – Correctness, Modeling and Performance of Aerospace Systems

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.

Read More

PROSYD – PROperty based SYstem Design

The goal of the PROSYD project is to significantly increase the competitiveness and efficiency of the European IT industry through the establishment of a standard, integrated property-based paradigm for the design of electronic systems. This paradigm will integrate and unify the many phases of system development, including requirement definition, design, implementation, and verification, into one coherent design flow, building on the emerging standard property specification language PSL/Sugar, which has been recently selected as a basis for an IEEE standard.

Read More

Closed projects

AMASS

AMASS (Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems) will create and consolidate the de-facto European-wide open tool platform, ecosystem, and self-sustainable community for assurance and certification of Cyber-Physical Systems (CPS) in the largest industrial vertical markets including automotive, railway, aerospace, space, energy.

Read More

Formal Comparative Analysis for the Automated Air Traffic Control Design

In the next 20 years the airspace traffic will increase by 4 times, and current technology cannot guarantee an acceptable level of safety, reliability, and security. NASA is evaluating different options to design a more advanced and capable Air Traffic Control System. Such a huge project requires a wide range of different analysis, including political and environmental impact, cost analysis, usability, safety and reliability analysis, and so on.

The collaboration between NASA and FBK focused on the application of formal techniques to analyze the Automated Air Traffic Control design space, in order to evaluate and compare different design options. In collaboration with NASA experts, we focused on the problem of Functional Allocation, i.e., how to delegate separation of aircraft between on-board and on-ground components. We identified several design choices and trade-offs that lead to a design space with more than 1600 solutions. By applying a compositional design approach, each of them was exhaustively analyze in terms of properties satisfaction, safety assessment and reliability. The results were discussed and validated by NASA and highlighted novel and well-known issues.

(More details and materials on the project are available on the dedicated website)

Read More

Compass3 – Consolidation of COMPASS tools

The objective of the project is to produce a new release of the COMPASS toolset, to be referred to as COMPASS 3.0, which integrates, harmonizes and updates selected features from previous projects (COMPASS, AUTOGEF, FAME and HASDEL), with the aim to resolve the compatibility problem.

Read More

ISAAC – Improvement of Safety Activities on Aeronautical Complex systems

The ISAAC project aims to increase the capability and efficiency of safety and systems engineers to perform safety assessments resulting in secure systems. The proposed methodology, built on formal method techniques, is an integrated part of a model-based development process where safety and reliability aspects are examined in the early steps of development.

Read More

VELOS – Verifica Logica di Sicurezza

Velos (Verifica Logica di Sicurezza) is a project aimed to apply formal methods to verification and validation of Logica di Sicurezza (LdS), software designed to monitor and control railway systems.

Read More

ACube

Improving the quality of life for the elderly and disabled through technological progress. That is the goal of project Acube. The project’s goal is to study technologies for monitoring complex environments that can be applied in areas such as assisted living homes to help personnel, as well as to support the independence and safety of users.

Read More

MISSA – More Integrated and cost efficient Systems Safety Assessment

The MISSA project aims at developing new procedures, based on formal methods, to support safety analysis and verification of complex systems. The ultimate goal of the project is the reduction of development costs and the optimization of the production chain. To reach this goal, MISSA will focus on the following dimensions: design and installation optimization, assessment of a systems organic architecture against the safety requirements, detailed system architecture and design, and a software infrastructure that facilitates the exchange of information.

Read More

ESACS – Enhanced Safety Assessment for Complex Systems

The unavoidable increase in the complexity of systems means that there must be a suitable boost in the capability of safety engineers to maintain safety levels.

ESACS intended to develop an environment and a safety method to help safety engineers in the assessment of complex systems, so that there will be no detriment to the safety of systems due to their increase in complexity.

Read More