AVerT2: Automated Verification and Testing

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 results and effects:

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.

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.