AVerT2: Automated Verification and Testing
| Reference number | |
| Coordinator | Kungliga Tekniska Högskolan - Kungliga Tekniska Högskolan Skolan f elektroteknik & datavetens |
| Funding from Vinnova | SEK 5 970 600 |
| Project duration | November 2021 - November 2024 |
| Status | Completed |
| Venture | Electronics, software and communication - FFI |
| Call | Electronics, software and communication - FFI - June 2021 |
Important results from the project
The goal of deriving the requirements for the software modules from the top-level system requirements was solved, delivering procedures for how to systematically do that. The goal of fully automating the formal verification process was achieved to an almost full extent, delivering a tool release and case study. Follow-up work aims to complete this goal. The goal of enabling the integration of the new technology into the existing software development processes will require some future effort.
Expected long term effects
The project has developed novel competence and technology for the automated formal verification of safety-critical embedded software. It enables the future integration of the technology into the existing software development processes. Another significant effect of the project is that it enables the combination of the new technology with generative AI to produce correct embedded software with considerably less human effort than currently. Our follow-up project FormAI explores this.
Approach and implementation
The project was conducted in a tight collaboration between the group of Mattias Nyberg at Scania and the group of Dilian Gurov at KTH. We had two workshops per year to discuss our progress and plan for the next 6 months. Further, we had weekly meetings to organize the day-to-day work. An important instrument was the use of Masters projects at Scania and KTH to involve talented students in our work. We also had group participation in workshops and seminars of strategic relevance for the project.