AVerT - Automated Verification and Testing
|Coordinator||Scania CV AB|
|Funding from Vinnova||SEK 6 435 238|
|Project duration||November 2018 - November 2021|
|Venture||Electronics, software and communication - FFI|
|End-of-project report||2018-02727 svensk.pdf(pdf, 245 kB) (In Swedish)|
Purpose and goal
The purpose has been to create formal methods and tools for industrial development of safety-critical systems. The ambition was to work in four areas: 1. requirement decomposition 2. deductive verification of C-code 3. verification of Simulink models 4. Automated Learning based Testing Due to IPR reasons, 4 was discontinued, and regarding 3, results were created but these are considered too demanding to maintain because an external tool supplier would be needed. Within 1 and 2, good results have been created and these are further developed within the continuation project AVerT2.
Expected results and effects
The project has mainly created results in the form of methods and tools in two areas: 1. automatic formal verification of source code written in C, 2. structuring of requirements to support a compositional formal verification of large systems, such as a truck. We expect these results to be transferred to Scania and also other companies. There is a great interest in this. However, the results are not yet ready for direct use in industry. Therefore, the continuation project AVerT2 has been created with a focus on packaging the results for industrial use.
Planned approach and implementation
Central to the project has been a doctoral student at KTH. He has partly performed academic research which has resulted in scientific articles, partly worked with the implementation of the tool AnnotationWeaver which is developed within the project, and then also worked with case studies. The project has also had thesis workers, summer workers, and project positions, all of which have contributed to tool development and case studies. The work with case studies has continuously provided feedback on what new research is needed and how the tool needs to be developed.