Formell verifiering med AI
| Diarienummer | |
| Koordinator | Prover Technology AB |
| Bidrag från Vinnova | 1 712 432 kronor |
| Projektets löptid | mars 2019 - februari 2022 |
| Status | Avslutat |
Syfte och mål
Inom ramen för projektet har vi utvecklat en prototyp av en produkt för formell verifiering som använder maskininlärning för att effektivisera analysen. Målet har varit att prototypen ska ge kraftigt förbättrade prestanda. Den största prestandaökningen har vi fått i sökandet av motmodeller för fallerande säkerhetskrav. Där kan den typiska vinsten vara av storleksordningen 5x för stora system (i vissa fall upp till 100x). Projektets omfång har begränsat möjligheterna att lägga ner så mycket arbete på ökad automatisering som vi önskat, men det är ett viktigt fokusområde framöver.
Resultat och förväntade effekter
Vid utvecklingen av prototypen har vi fokuserat på att använda maskininlärning för att hitta bättre strategier för vår bevismotor. Vi har under projektets gång fokuserat på tillämpningar inom järnväg och tunnelbana, men eftersom prestandaförbättringarna är generiska så går det utmärkt att tillgodogöra sig dessa även vid analys av andra typer av system, som t.ex. IoT eller självkörande bilar. Det har dock inte funnits utrymme för att utvärdera dessa områden inom ramen för projektet. Projektet har gett oss goda insikter i hur maskininlärning kan användas inom formell verifiering.
Upplägg och genomförande
Projektets upplägg har varit rimligt även om arbetet sedan fick en mer iterativ karaktär; i mitten av projektet pågick alla tre faserna samtidigt. Fas 1 hade ett större omfång än planerat och många idéer behövde testas i prototypen för att förstå om de skulle förkastas eller inte. Framför allt är det tid och resurser som har varit (och är) begränsande faktorer, och det finns fortfarande många uppslag vi vill utforska i framtiden. Mängden datorresurser som projektet förväntades kräva var för lågt skattat vid projektstart, men kunde ändå hanteras hjälpligt under projektets gång.