AVerT - Automated Verification and Testing

Important results from the project

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 long term 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.

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.