Over 90% of web-based front-end interfaces are written in JavaScript.
Given its prevalence, the support for advanced functionalities in JavaScript that can guarantee
high performance is crucial. The Technical Committee 39 (TC39) is currently in the process of
extending the language to support shared memory, which will improve the performance of multithreaded programs and
provide better support for multiprocessor and multicore
systems.
This project is oriented to provide an automated approach to evaluate the correctness of the JS engines implementing such extension. The technique consists of formalizing the axiomatic memory model and a representation of the candidate JavaScript program using the language of Satisfiability Modulo Theories (SMT). This formal representation is then analyzed using the CVC4 SMT solver to compute all possible models of the formula, i.e., a representation of the set of valid memory model interpretations.
In the next 20 years the airspace traffic will increase by 4 times, and current technology is not going to be able to guarantee an acceptable level of safety, reliability, and security.
The NextGen project aims to solve this problem, and define a more advanced an capable Air Traffic Control System. Such a huge project requires a wide set of different analysis, including political and environmental impact, cost analysis, useability, safety and reliability analysis, and so on. The project that we present here provides an overview of the formal analysis applied to the Automated Air Traffic Control Designs, in order to evaluate the different possible approaches.
The strategic collaboration of FBK with the Boeing Company arose from the expertise in the field of formal verification of the Embedded Systems Unit.
A joint scientific study, funded by Boeing, was conducted as part of the Unit's activities on model-based safety assessment (MBSA) and contract-based safety assessment (CBSA) activities. The purpose is to investigate the application of safety assessment techniques based on formal models to the design process of Boeing, with the goal of demonstrating their usefulness and suitability for improving the overall development and supporting aircraft certification.
In MISSA (More Integrated Systems Safety Assessment) we aim to develop methods and tools to help safety engineers to collect, navigate, and manage information, structure their arguments, express their ideas, and most importantly find solutions to problems in an efficient, auditable and exhaustive way.
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. The methodology is based on a three-phases approach that goes from the informal analysis of the requirements, to their formalization and validation. Second, we developed a set of support tools, covering the various phases of the methodology. Third, we formalized a realistic subset of the specification in an industrial setting. The results of the project were positively evaluated by domain experts from different manufacturing and railway companies.
Fatal defects in the control system of the Ariane-5 rocket and the Mars Pathfinder have led to headlines in newspapers all over the world. To detect such flaws in an early stage of the design, the European Space Agency intends to develop techniques that assist design engineers in software tools that help the engineers to find bugs in a fully automated manner.
In this project a model-based approach to system-software co-engineering is taken, specifically tailored to critical on-board systems for the space domain. For this, the consortium develops an integrated toolset based on a newly developed modelling language.
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.