AVerT2: Automatiserad verifiering och testning
| Diarienummer | |
| Koordinator | Kungliga Tekniska Högskolan - Kungliga Tekniska Högskolan Skolan f elektroteknik & datavetens |
| Bidrag från Vinnova | 5 970 600 kronor |
| Projektets löptid | november 2021 - november 2024 |
| Status | Avslutat |
| Utlysning | Elektronik, mjukvara och kommunikation - FFI |
| Ansökningsomgång | Elektronik, mjukvara och kommunikation - FFI - juni 2021 |
Viktiga resultat som projektet gav
Målet att härleda kraven för programvarumodulerna från systemkraven på högsta nivån löstes, och levererade procedurer för hur man systematiskt kan göra det. Målet att helt automatisera den formella verifieringsprocessen uppnåddes i nästan full utsträckning, vilket gav en verktygsrelease och fallstudie. Uppföljningsarbete syftar till att uppnå detta mål. Målet att möjliggöra integrationen av den nya tekniken i de befintliga mjukvaruutvecklingsprocesserna kommer att kräva en del framtida arbete.
Långsiktiga effekter som förväntas
Projektet har utvecklat ny kompetens och teknologi för automatiserad formell verifiering av säkerhetskritisk inbyggd programvara. Detta möjliggör framtida integration av tekniken i befintliga processer för mjukvaruutveckling. En annan betydande effekt av projektet är att det möjliggör kombinationen av den nya tekniken med generativ AI för att producera korrekt inbyggd programvara med betydligt mindre mänsklig insats än för närvarande. Vår uppföljningsprojekt FormAI utforskar detta.
Upplägg och genomförande
Projektet genomfördes i ett tätt samarbete mellan Mattias Nybergs grupp på Scania och Dilian Gurovs grupp på KTH. Vi hade två workshop per år för att diskutera våra framsteg och planera för de kommande 6 månaderna. Vidare hade vi veckomöten för att organisera det dagliga arbetet. Ett viktigt instrument var användningen av masterprojekt på Scania och KTH för att involvera studenter i vårt arbete. Vi hade också gruppdeltagande i workshops och seminarier av strategisk relevans för projektet.