The successful verification of the behaviour of an Autonomous driving (AD) vehicle is fundamental for the commercialization of this new technology. Formal verification can be used to exhaustively verify the correctness of a system, but it requires a formal model to do so. An exact mathematical definition of the model description of the system is required. Manually defining a model is daunting, error-prone, and intractable for large systems. Automata learning is a branch of Machine learning (ML) that automatically creates a formal model by dynamically interacting with the system. In prior research, automata learning algorithms have been shown to learn a formal model from AD software implemented in MATLAB. However, practical challenges were highlighted in addressing the state-space explosion problem and in obtaining suitable abstractions to deal with large systems. To obtain valuable insights to scale up automata learning for industrial use, this thesis investigates the topic of automatically learning an extended finite automata formalism, called register automata. The SL* algorithm, an extension of the L* algorithm, is used to learn a register automata model of AD software from MATLAB code. The new algorithm creates a register automaton that manages to deal with the data dependencies intrinsically created from the case study between the input variables. Some approximations to the original model were made to obtain the desired solution. The obtained results are presented, from establishing the learning interface, validation of the interface, and from learning the case study. Evidence has been shown that similar problems to those highlighted for DFA learning are encountered. Future works have been discussed to address the same topic and to improve the proposed methodology. / Den framgångsrika verifieringen av beteendet hos ett autonomt körande fordon är grundläggande för kommersialiseringen av denna innovativa teknik. Formella metoder kan förutses som den sista tekniken för att uppnå detta mål. Den exakta matematiska definitionen av modellbeskrivningen för systemet behövs. Tidigare verk kunde inte skapa en metod för att automatiskt beskriva beteendemodellen för SUL. Nuvarande Lateral State Manager varierar komplexiteten som förhindrade användningen av ramverk som LearnLib eller den normala L * -algoritmen. Den stora mängden ingångar och den exponentiella tillväxten av den observerbara tabellen är några av orsakerna som gör att standardalgoritmerna misslyckas. Tidigare löstes problemet delvis och introducerade viss abstraktion till SUL. I denna avhandling föreslår vi en metod baserad på en innovativ algoritm: SL *. Den är utvecklad tack vare förlängningen av LearnLib-ramverket RALib. Den nya algoritmen skapar en registerautomat som klarar av att hantera databeroendet som skapats ur studiens fall. För att få en lösning inom acceptabel tid gjorde vi en ungefärlig tillnärmning till den ursprungliga modellen som vi tror inte påverkar det slutliga resultatet och skapar en modell som kan användas för de ändamål den var tänkt för. / La corretta verifica del comportamento di un veicolo a guida autonoma è fondamentale per la commercializzazione di questa tecnologia. Diversi metodi formali possono essere previsti come una possibile tecnica al fine di raggiungere parte di questo vasto obiettivo. Al fine di utilizzare tali metodi è necessaria l’esatta descrizione matematica del modello comportamentale del sistema. Precedenti studi non sono stati in grado di creare automaticamente un metodo per descrivere il comportamento del sistema sotto esame. Il Lateral State Manager presenta varie complessità che hanno impedito l’uso di framework come LearnLib o dell’algoritmo L_. La grande quantità di input e la crescita esponenziale della tabella delle osservazioni sono alcune delle principali cause che portano i comuni algoritmi al fallimento. In precedenza il problema è stato parzialmente risolto introducendo alcune astrazioni al caso di studio. In questa dissertazione proponiamo un metodo basato su un algoritmo innovativo: SL *. Lo stesso è sviluppato grazie all’estensione del framework LearnLib, chiamato RALib. Il nuovo algoritmo crea degli automi basati sui registri che riescono a gestire la dipendenza tra i dati intrinsecamente creati dal caso di studio. Per ottenere una soluzione in tempi accettabili si sono rese necessarie alcune approssimazioni del modello originale che riteniamo non influiscano sul risultato finale, creando un modello che possa essere utilizzato per gli scopi per cui è stato pensato.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:kth-306490 |
| Date | January 2021 |
| Creators | Dei Rossi, Marco |
| Publisher | KTH, Skolan för elektroteknik och datavetenskap (EECS) |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | Italian |
| Type | Student thesis, info:eu-repo/semantics/bachelorThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | TRITA-EECS-EX ; 2021:743 |
Page generated in 0.0022 seconds