TRANSFORM - Design transformation for correct-by-construction design methodology
Reference number | |
Coordinator | Saab AB |
Funding from Vinnova | SEK 3 500 000 |
Project duration | November 2019 - June 2023 |
Status | Completed |
Venture | National Aeronautical Research Program 7 |
Call | Research project in aviation technology - spring 2019 |
Important results from the project
The aviation industry needs efficient systems and software development methods with a formal basis that can guarantee correct behavior. The project took an important step to use design transformations in a formal way within a correct-by-construction design process. The method creates conditions for transforming an abstract, formal and executable system model through stepwise application of formal transformation rules into a physical implementation on a network-based avionics platform.
Expected long term effects
The project has created a method for a construction flow based on transformations. The project has delivered: 1) a new design method that uses transformations to incrementally refine the system model into a form that enables implementation in hardware and software; 2) Definition of contracts for formal transformations and their verification; 3) Prototype of a transformation tool; 4) The methodology and associated tools have been applied in a representative smaller application. The results are promising, but more research is needed to reach a higher degree of maturity.
Approach and implementation
The project builds on project defined within the avionics platform technology cluster that together address computing power, robustness, security and development cost. The developed methodology uses tools and methodology from the NFFP7 project CORRECT which took the initial step for a correct-by-construction design process. The project complements CORRECT with a formal transformation-based methodology with the potential to model and manage trade-offs at a higher level of abstraction and reduce the need for verification at a lower level of abstraction.