Holistisk Syntes och Verifiering för Trygga och Säkra Autonoma Fordon

Fordonsindustrin är en av de viktigaste industrierna i Sverige. I och med utvecklingen av AI-teknologier, implementeras automatiskt körning ("autonomous driving", AD) gradvis i moderna fordon, såsom autopilot i Tesla-bilar. Men oavsett vad företagen hävdar kräver de nuvarande AD-funktionerna faktiskt full eller aktiv övervakning av mänskliga förare, vilket gör att lösningen inte är helt autonom. Ett av hindren som hindrar förverkligandet av AD är säkerhet och trygghet. I ett helt autonomt fordon kan man inte räkna med mänskliga förare för att hantera extraordinära situationer, vilket innebär att AD-kontrollanterna måste ta fullt ansvar för eventuella mjukvaru- eller hårdvarufel. Men trots det avgörande ansvaret och höga betydelsen av AD-kontrollanter är de vanligaste teknikerna antingen en enkel cykel av försök-fel-försök eller beroende av manuell analys, t.ex. felträdsanalys.

Dessutom har säkerhetsproblem dykt upp under de senaste åren, och problemet har blivit ännu värre i samband med AD-fordon eftersom de flesta av dem är sammankopplade eller anslutna till molnservrar. En säkerhetsattack på fordonets kontrollprogramvara eller inbyggda databas skulle påverka systemets säkerhet. Därför är samdesign och verifiering av säkra AD-styrenheter ett akut behov för bilindustrin. Det finns dock många utmaningar i syntesen och verifieringen av säkra och säkra AD-kontrollanter och målet för detta projekt är att övervinna dessa utmaningar. Kortfattat är utmaningarna som tas upp i projektet i) heterogenitet hos AD-kontrollanter, ii) samkonstruktion av säkerhets- och säkerhetsfunktioner, iii) syntes av AD-kontrollanter och iv) pålitlig maskininlärning i AD. För att möta dessa utmaningar kommer vi att föreslå ett ramverk som tar syntesen och verifieringen av säkra AD-kontrollanter i beaktande på ett holistiskt sätt.

Ramverket kommer att baseras på de senaste formella metoderna ("state-of-the-art", SOTA), såsom probabilistisk modellkontroll, och de mest avancerade maskininlärningsteknikerna, såsom stora språkmodeller (LLM). Ramverket kommer att ytterligare integrera de befintliga verktyg som används i de industriella partnerna, såsom felträdsanalys, och SOTA-verktygen/-metoderna, som kommer att förbättra prestandan för de befintliga verktygen och kvaliteten på AD-funktionerna som används i deras produkter. Det viktigaste är att forskningsresultaten från detta projekt kommer att främja SOTA i följande aspekter: i) algoritmerna för kontrollsyntes och verifiering kommer att vara skalbara för industriella problem, som inte är helt lösta av formella metoder, ii) ramverket som införlivar algoritmerna kommer att stödja samdesign och verifiering av säkerhet för systemet, och iii) gapet mellan forskningsfältet av formella metoder och praktiker som har begränsad kunskap om formella metoder kommer att överbryggas av vårt LLM-drivna verktyg i sammanhanget av AD-kontrollersyntes och verifiering.

Projektmål

Projektets mål är att övervinna de största utmaningarna med syntes och verifiering av säkra och säkra AD-kontroller, som finns i den nuvarande fordonsindustrin i Sverige.

OB1. En systematisk utvärdering av de avancerade teknikerna för syntes och verifiering, för att få fram deras styrkor och svagheter i utvecklingen av säkra och säkra AD-kontrollanter. OB2. Ett ramverk för syntes och verifiering av säkra och säkra AD-kontrollanter. Ramverket måste kunna känna igen olika modelleringsspråk och stödja formell verifiering av dessa modeller, och databasen för AD-kontrollanter måste ha en säkerhetsgaranti. OB3. En metodik för att realisera säkra och säkra ML-utbildade AD-kontrollanter. Vi siktar på att utveckla en ny metodik som kombinerar de senaste verktygen/metoderna (identifierade i OB1) och de befintliga verktygen/metoderna som används i industriella sammanhang. OB4. En utvärdering av ramverket (OB2) som införlivar den nya metodiken (OB3) genom fallstudier och experiment i industriella miljöer.