Applied Formal Methods at ONERA: An Experience Report
摘要
ONERA is a french national research center developing methods and studies related to the aerospace domain, including physical simulations, event processing, and formal methods. It also produces many software tools at many level of maturity, ranging from prototypes for simple studies, to industrial level software tools in the context of collaborations with industrial partners like Airbus or SAFRAN. While these tools are developed by domain experts, which ensures the quality of their results, their implementation could benefit from expertise in computer-science and formal methods, to help ensure a design consistent with their expected maintainability, evolution and properties. To illustrate this statement, we present in this paper two recent projects at ONERA where formal methods were actively used in the design of new scientific tools or in the maintenance of existing ones. In particular, we discuss the context of these projects, where formal methods were used, for what purpose and with what results. We also propose a report on some of the dynamics that were used to develop fruitful and long-lasting collaborations between formal methods and experts of very different scientific fields.