Automatic Train Operation (ATO) is an ongoing project, part of the Strategic Program for Railways...

PASSIONS (Software Product Assurance for Autonomous On-Board Software), funded by ESA, coordinated...

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

VALU3S focuses on verification and validation (V&V) of...

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

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.

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

Modeling, verification and safety analysis of critical, highly integrated systems

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.

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

In AWARD, the ES unit is responsible for the intra-logistic planning of a warehouse using...

The Mechanical Automation Integration System is an ambitious project aimed at the development...

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

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.

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.

The ESA AUTOGEF (Dependability Design Approach  for Critical Flight Software) study is a...

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.

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 need for high level of confidence and operational integrity in critical space (software) systems is well recognized in the Space industry and has been addressed so far through rigorous System and Software Development Processes and stringent Verification and Validation regimes.

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

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 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.

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.

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

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.

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.

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)

These are two projects ILAADR – Internal Logistics with Automated Autonomous Delivery and Replenishment and ILEVATOR – intraLogistics Enabled by autonomous Vehicles cooperATing with Operators and Robots both funded by EIT Digital.

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.

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.

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.

SIMS is a industrial project which aims to analyze operational data provided by devices (Oil & Gas, Rail domains) in order to take appropriate corrective actions in terms of preventive maintenance

TRITon is a research and innovation project funded by the project members and the Autonomous Province of Trento (Provincia Autonoma di Trento, PAT) aimed at advancing the state of the art in the management of road tunnels, specifically to improve safety and reduce energy costs.

SafeCer is targeting increased efficiency and reduced time-to-market by composable safety certification of safety-relevant embedded systems. The industrial domains targeted are within automotive and construction equipment, avionics, and rail. SafeCer will also develop certification guidelines and a training example for other domains, thus considerably increasing its market impact.

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.

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.

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.

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.