Automatically Learning Register Automata from MATLAB Code : A case study in autonomous driving

Abstract: 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.