The objective of the project is to propose and demonstrate a genericVerification and Validation methodology based on the usage of theSystem-level Simulation Facilities, specifically targeted at spaceautonomous systems using...Read More
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
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.
In AWARD, the ES unit is responsible for the intra-logistic planning of a warehouse using...Read More
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 needsRead More
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
S3MS (Security of Software and Services for Mobile Systems) is a European research project focused on the security issue of mobile systems.Read More
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
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
The ESA AUTOGEF (Dependability Design Approach for Critical Flight Software) study is a...Read More
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
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
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
FoReVer – Functional Requirements and Verification Techniques for the Software Reference Architecture
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.Read More
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
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
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
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.Read More
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
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.Read More
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
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
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
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 maintenanceRead More
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.Read More
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.Read More
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
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
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