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.
Within the project, serveral case studies have been investigated, including the Weel Braking System (WBS) case study from the AIR6110 standard and the Triple Modular Generator (TMG) case study. The case studies have been analyzed using the FBK tools, including the nuXmv model checker, the xSAP safety analysis platform, and the ocra tool for contract-based design.
