AVerT - Automated Verification and Testing

Syfte och mål

Syftet har varit att skapa formella metoder och verktyg för industriell utveckling av säkerhetskritiska system. Ambitionen var att arbeta inom fyra områden: 1. requirement decomposition 2. deductive verification of C-code 3. verification of Simulink models 4. Automated Learning based Testing on Vehicle Simulators Pga rättighetsskäl utgick det sista, och angående 3, så skapades resultat men dessa bedöms för krävande att förvalta ty en extern verktygsleverantör skulle behövas. Inom 1 och 2 har skapats bra resultat och dessa utvecklas vidare inom fortsättningsprojektet AVerT2.

Resultat och förväntade effekter

Projektet har i huvudsak skapat resultat i form av metoder och verktyg inom två områden: 1. automatisk formell verifiering av källkod skriven i C, 2. strukturering av krav för att stödja en kompositionell formell verifiering av stora system, tex en lastbil. Vi förväntar oss att dessa resultat kommer överföras till Scanias verksamhet och även andra företag. Det finns ett stort intresse för detta. Dock är inte resultaten ännu färdiga att direkt användas i industrin. Därför har fortsättningsprojektet AVerT2 skapats med fokus på packetering av resultaten för industriell användning.

Upplägg och genomförande

Central i projektet har varit en doktorand vid KTH. Han har dels forskat vilket resulterat i vetenskapliga artiklar, dels jobbat med implementation av verktyget AnnotationWeaver som utvecklas inom projektet, och sen också jobbat med case studies. Projektet har även haft exjobbare, sommarjobbare och projektanställningar som alla bidragit till verktygsutveckling och fallstudier. Arbetet med fallstudier har löpande gett feedback om vilken ny forskning som behövs samt hur verktyget behöver utvecklas.