Automatiskt bedömning av autonoma fordoners korrekthet - Auto-CAV

Syfte och mål

Projektet syftade till att etablera formella metoder som ett effektivt verktyg i utvecklingen av säkerhetskritisk programvara för automatiserade fordon. Det övergripande målet var att ta itu med utmaningarna i utvecklingen och verifieringen av säkra automatiserade körsystem och därigenom bidra till att uppnå säkrare fordon och förbättrad trafiksäkerhet. Resultaten och insikterna från projektet dokumenteras i flera akademiska publikationer inklusive en licentiatavhandling och en doktorsavhandling.

Resultat och förväntade effekter

Flera formella metoder för att modellera, specificera och verifiera automatiserade körsystem utvärderas. Insikter i hur de utvärderade metoderna skiljer sig och vilka utmaningar det innebär dokumenteras och publiceras. Formella modelleringsriktlinjer och metoder för att identifiera och åtgärda subtila modelleringsfel utvecklas. Ett systematiskt tillvägagångssätt för att automatiskt få formella modeller utvecklas och valideras av ett proof of concept. En strategi för användningen av formella artefakter i säkerhetsargumentet för automatiserade körsystem publiceras.

Upplägg och genomförande

Projektet har drivits som ett industridoktorandprojekt i samarbete med Zenseact (tidigare Zenuity) och Chalmers tekniska högskola. Forskningen är motiverad av industriella behov och därför är problemformuleringar, forskningsfrågor, metoder och resultat nära kopplade till industriell forskning och utveckling av automatiserade körsystem. En betydande del av forskningsmetoden i detta projekt involverar matematisk modellering och matematiska bevis.