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.

A reactive system is a system that continuously interacts with its environment. The environment provides an input signal, to which the system reacts with an output signal, and so on ad infinitum. In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. In the classical setting, the set of signals is assumed to be finite. however, this assumption is not realistic to model systems which process sequences of signals accompanied with data from a possibly infinite set (e.g. a client id, a sensor value, etc.), which need to be stored in memory and compared against each other.The goal of this thesis is to lift the theory of reactive system synthesis over words on a finite alphabet to data words. The data domain consists in an infinite set whose structure is given by predicates and constants enriched with labels from a finite alphabet. In this context, specifications and implementations are respectively given as automata and transducers extended with a finite set of registers that they use to store data values. To determine the transition to take, they compare the input data with the content of the registers using the predicates of the domain.In a first part, we consider both the bounded and unbounded synthesis problem; the former additionally asks for a bound on the number of registers of the implementation, along with the specification. We do so for different instances, depending on whether the specification is a nondeterministic, universal (a.k.a. co-non-deterministic) or deterministic automaton, for various domains.While the bounded synthesis problem is undecidable for non-deterministic specifications, we provide a generic approach consisting in a reduction to the finite alphabet case, that is done through automata-theoretic constructions. This allows to reprove decidability of bounded synthesis for universal specifications over (ℕ,=), and to obtain new ones, such as the case of a dense order, or the ability of data guessing, all with a 2-ExpTime complexity.We then move to the unbounded synthesis problem, which is undecidable for specifications given by non-deterministic and universal automata, but decidable and ExpTime-complete for deterministic ones over (ℕ,=) and (ℚ,<). We also exhibit a decidable subclass in the case of (ℕ,<), namely one-sided specifications.In a second part, we lift the reactivity assumption, considering the richer class of implementations that are allowed to wait for additional input before reacting, again over data words. Specifications are modelled as non-deterministic asynchronous transducers, that output a (possibly empty) word when they read an input data. Already in the finite alphabet case, their synthesis problem is undecidable.A way to circumvent the difficulty is to focus on functional specifications, for which any input sequence admits at most one acceptable output. Targeting programs computed by input-deterministic transducers is again undecidable, so we shift the focus to deciding whether a specification is computable, in the sense of the classical extension of Turing-computability to infinite inputs. We relate this notion with that of continuity for the Cantor distance, which yields a decidable characterisation of computability for functional specifications given by asynchronous register transducers over (ℕ,=) and for the superseding class of oligomorphic data domains, that also encompasses $(ℚ,<)$. The study concludes with the case of (ℕ,<), that is again decidable. Overall, we get PSpace-completeness for the problems of deciding computability and refined notions, as well as functionality. / Option Informatique du Doctorat en Sciences / info:eu-repo/semantics/nonPublished