A joint scientific study by the Trentino based Research Center and the aerospace giant has been presented in San Francisco during the most important world conference in the area of formal verification and validation.
(v.l.) Researchers at Fondazione Bruno Kessler (FBK) in Trento have conducted a joint scientific study with Boeing on the topic of safety assessment based on formal mathematical models, which has been presented at the most important world conference in the area of formal verification, CAV 2015, last July 2016 in San Francisco.
The strategic collaboration of the Trentino based research center with the international aerospace giant arose from the expertise in the field of formal verification of the Embedded Systems Unit led by Alessandro Cimatti at FBK’s Center for Information and Communication Technology, directed by Paolo Traverso.
The study was conducted as part of the Unit’s activities on model-based safety assessment (MBSA) activities, which also enabled the participation in European Space Agency projects and further paved the way for pioneer industrial applications. In 2014, FBK and Boeing signed a five-year strategic cooperation agreement. In the context of this agreement, Boeing funded a joint research and development project, whose 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.
The first scientific study, which will be presented in San Francisco, will specifically cover aircraft braking systems for landing operations. “The work” says FBK researcher Marco Bozzano, who carried out the study with Alessandro Cimatti, Anthony Fernandes Pires and Stefano Tonetta and, for Boeing, with David Jones, Greg Kimberly, Tyler Petri and Richard Robinson, “involved analyzing, through mathematical models, all possible scenarios in the design stage and proceeding to their verification, with the use of automated resolution software.
This provides the traditional engineering work with additional guarantees regarding the proper operation of the systems involved in all the scenarios of interest.”
In the field of formal verification, FBK has developed and owns the intellectual property of many tools and technologies, including the reliability analysis system called xSAP and the correctness analysis system called nuXmv.