Text

  • Studieort Sal U2-024, MDH Västerås och digitalt (Zoom)
Datum
  • 2020-06-15 09:00–11:00

Rong Gu försvarar sin licentiatuppsats i datavetenskap

Rong Gu vid akademin för innovation, design och teknik (IDT), försvarar sin licentiatuppsats i datavetenskap den 15 juni klockan 09:00, sal U2-024, MDH Västerås och digitalt (Zoom).

Titel: “Automatic Model Generation and Scalable Verification for Autonomous Vehicles - Mission Planning and Collision Avoidance”.

Serienummer: 291.

Betygsnämnden utgörs av professor Kim Larsen, Aalborg University, docent Dilian Gurov, KTH, adjungerad professor Marina Walden, Åbo Akademi University.

Professor Kim Larsen, Aalborg University, har utsetts till opponent.

Reserver är professor Thomas Nolte, MDH.

Sammanfattning

Autonoma fordon, exempelvis förarlösa byggfordon, lovar ökad säkerhet och industriell produktivitet genom att automatisera upprepade uppgifter och minska manuella arbetskraftskostnader. Dessa system är vanligtvis involverade i säkerhets- eller uppdragskritiska scenarier, därför kräver de noggrann analys och verifiering. Traditionella tillvägagångssätt som simulering och prototyptestning är begränsade till verifiering av system som samverkar autonomt med en oförutsägbar miljö som förutsätter närvaron av människor och olika platsförhållanden. Metoder för formell verifiering kan vara mer lämpade för att garantera säker drift av autonoma fordon i specifierade oförutsägbara miljöer. Att tillämpa dem innebär emellertid två huvudutmaningar: (i) konstruktion av modellerna av systemen och deras miljö, och (ii) skalning av verifieringen till den uppkomna modellkomplexiteten. Vi tar upp dessa två utmaningar inom ramen av två väsentliga aspekter viddesign av autonoma fordon: uppdragsplanering och undvikande av kollision. Trots att de två aspekterna skiljersig åt är kommunikation mellan dessa två aspekter nödvändig, eftersom informationen som erhålls för att verifiera kollisionsundvikande kan bidra till att förbättra uppdragsplaneringen och vice versa. Att hitta en lösning som hanterar både uppdragsplanering och modellering och verifiering av kollisionsundvikande, samtidigt som den frikopplar delarna för att kunna underhålla dem är en svårighet i dessa utmaningar. En annan handlar om att visa huruvida den föreslagna metoden är tillämpbar och skalbar på komplexa och industriella system.

I den här avhandlingen föreslår vi ett ramverk i två lager för uppdragsplanering och verifiering av autonoma fordon. Ramverket skiljer modelleringen och uppdragsplaneringen i en diskret miljö, från fordonets rörelse i en kontinuerlig miljö, där kollisionsundvikelsealgoritmer baserade på dipolfält är bevisade för att säkerställa säkert beteende. Vi kallar lagret för uppdragsplanering, ”det statiska lagret” och det andra för ”det dynamiska lagret”. På grund av den inneboende skillnaden mellan lagren använder vi olika modellerings- och verifieringsmetoder, nämligen: (i) till det tidsinställda lagret använder vi tidsautomateroch mjukvaran UPPAAL för att beräkna uppdragsplaner för de autonoma fordonen, och (ii) hybridautomater och statistisk modellkontroll med hjälp av UPPAAL Statistical Model Checker för att kontrollera undvikande av kollision och säker drift. Vi skapar modellgenerationsalgoritmer som vi baserar utvecklandet av verktygsstöd för det statiska skiktet på. Verktyget, TAMAA (Timed-Automata-Based Planner for Autonomous Agents), gör det möjligt för designers att konfigurera sina system och miljöer i ett grafiskt användargränssnitt och använda formella metoder och avancerade sökplaneringsalgoritmer för att generera uppdragsplaner automatiskt. TAMAA integrerar också förstärkningslärande för att lindra problemet med exponentiell tillväxt av tillstånd när antalet fordon ökar. Vi skapar en hybridmodell för ramens dynamiska lager och föreslår en mönsterbaserad modelleringsmetod för de inbäddade styrsystemen i autonoma fordonen för att underlätta designen och återanvändning. Vi validerar det föreslagna ramverket och konstruktionsmetoden för ett industriellt användningsfall som involverar autonoma hjullastare, för vilket vi verifierar diverse relevant egenskaper.

Kontaktinformation

Doktorand

Rong Gu

+4621101560

rong.gu@mdh.se