Automated model-based testing of railway signalling systems

In the field of human mobility, safety has always been a crucial issue, in particular when dealing with railway transports. This thesis work focuses on a critical aspect of this topic: Railway Signalling Systems, which are a type of Time-Critical Systems and whose correct functioning is fundamental for safety and punctuality purposes. Both the academic and the industrial worlds are facing this topic with the help of model-based approaches, in particular, Rete Ferroviaria Italiana (RFI) is evaluating these methods to design, specify and verify their Railway Signalling Systems in a rigorous way. This thesis faces the issue of testing Railway Signalling Systems utilizing a model-based approach which considers formal models. The topic of testing is crucial because, through it, it is determined whether the system analysed satisfies the specifications given by the model or not. A methodology for performing this kind of testing with an automated procedure has been developed in this thesis by means of three different model-based testing strategies. These strategies are used to generate the test cases considering different approaches: one related to unit testing, one to integrated testing and the third one is a mix of them. The results of the test cases generation procedure are sequences of events which are applied as constraints to the System Under Test in order to verify if the specifications described by the model hold or not. This automated process covers in a pseudoexhaustive way the relevant aspects of the model in a short amount of time. The methodology developed is implemented in a software called Railway systems Signalling Testing Tool (RSTT). RSTT gives to the user the possibility of testing a certain system selecting among the three different testing strategies. Once the test cases are generated and the tests are executed, the tool returns to the user a report containing the verdict of the test and other important informations parsed when evaluating the System Under Test. The result of this thesis is an efficient high-level tool which gives the possibility of testing in an automated way, thanks to the use of formal methods, a certain system.

Nel campo della mobilità degli uomini, la sicurezza è sempre stata una questione cruciale, in particolare riguardo ai trasporti ferroviari. Il lavoro svolto in questa tesi si concentra su un aspetto critico di questo argomento: i sistemi di segnalamento ferroviario, i quali sono un tipo di "Time-Critical Systems" e il cui corretto funzionamento è fondamentale per ragioni di sicurezza e di puntualità. Sia il mondo accademico che quello industriale stanno affrontando questo argomento con l'aiuto di approcci "model-based", in particolare Rete Ferroviaria Italiana (RFI) sta valutando questi metodi per progettare, specificare e verificare i propri sistemi di segnalamento ferroviario in maniera rigorosa. Questa tesi affronta il problema di testare i sistemi di segnalamento ferroviario utilizzando un approccio "model-based" che considera modelli di tipo formale. L'argomento del test è cruciale poichè, attraverso esso, viene determinato se il sistema analizzato soddisfa le specifiche fornite dal modello oppure no. Un metodo per eseguire questo tipo di test con una procedura automatizzata è stato sviluppato in questa tesi per mezzo di tre diverse strategie di test model-based. Queste strategie sono utilizzate per generare i casi di test considerando diversi approcci: uno legato al test di unità, uno al test di integrazione e il terzo è un mix tra i due. I risultati della procedura per la generazione dei casi di test sono delle sequenze di eventi che vengono applicati come dei vincoli al sistema da testare in modo da verificare se le specifiche descritte dal modello sono verificate oppure no. Questo processo automatizzato copre in maniera pseudoesaustiva gli aspetti rilevanti del modello in una quantità di tempo ridotta. Il metodo sviluppato è stato implementato in un software chiamato Railway systems Signalling Testing Tool (RSTT). RSTT dà la possibilità all'utente di testare un certo sistema selezionando tra le tre diverse strategie di testing. Una volta che i casi di test sono stati generati e i test eseguiti, lo strumento restituisce all'utente un report contenente il verdetto del test e altre importanti informazioni analizzate durante la valutazione del sistema da testare. Il risultato finale di questo lavoro di tesi è uno strumento di alto livello che dà la possibilità di testare in maniera automatizzata, attraverso l'uso di metodi formali, un certo sistema.