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 | Ongoing |
| Venture | Electronics, software and communication - FFI |
| Call | Electronics, software and communication - FFI - June 2021 |
Purpose and goal
The aim of the project is to increase the use of formal methods for specification and verification of software components in the automotive industry, by largely automating the process. Through the application of formal methods, confidence in the functional correctness of such systems increases, and consequently vehicle and traffic safety also increases. The goal of the project is to develop a tool chain for writing system specifications, automatically decomposing specifications, automatically verifying software models and code, and to perform technology transfer.
Expected effects and result
The project plans to deliver a framework and tool chain for formal specification and automated verification of software components in embedded systems, as well as case studies. Through these tools and case studies, we facilitate the adoption of formal methods in the industry. The intended users of these results are software designers and engineers at companies developing embedded vehicle software.
Planned approach and implementation
The work is divided into four main work packages. One package focuses on writing requirements and requirements decomposition, two packages on automatic verification, and the last one on practical evaluation and technology transfer. The project is coordinated by KTH, and collaboration between Scania and KTH will take place within all work packages.