On the Effectiveness of Automatic Test Case Generation for Safety-Critical Software

Software systems for automating safety-critical tasks in application domains like, avionics, railways, automotive, industry 4.0, and healthcare must be highly reliable. In this thesis, we focus on safety-critical software written in Scade, a model-based programming language largely adopted in industry, that we used for developing safety-critical Scade programs for the railway domain. Automated test generation (state-of-the-art) based on symbolic execution and bounded model checking can be beneficial for systematically testing safety-critical software to facilitate test engineers in pursuing the strict testing requirements mandated by the certification standards while controlling the cost of the testing process. At the same time, the development of safety-critical software is often constrained by programming languages or coding conventions that ban linguistic features believed to downgrade the safety of programs, e.g., they do not allow dynamic memory allocation and variable-length arrays, limit the way in which loops are used, forbid recursion, and limit the complexity of control conditions. We leverage state-of-the-art test generators based on symbolic execution and bounded model checking in order to define an original toolchain for generating test cases for Scade programs. We evaluate the effectiveness of our toolchain for automatic test generation with a benchmark of 37 Scade programs developed as part of an onboard signalling unit for high-speed railway systems developed in collaboration with an industrial partner.

I sistemi software per l'automazione di attività safety-critical in domini applicativi (ad esempio avionica, ferrovie, automotive, industria 4.0 e assistenza sanitaria) devono essere altamente affidabili. In questa tesi, ci concentriamo sul software safety-critical scritto in Scade, un linguaggio di programmazione model-based ampiamente adottato nell'industria, da noi utilizzato per lo sviluppo di programmi Scade safety-critical per il dominio ferroviario. La generazione automatica di test (stato dell'arte) basata sull'esecuzione simbolica e sul bounded model checking può essere utile per testare sistematicamente il software safety-critical al fine di facilitare gli ingegneri nel rispettare i severi requisiti di test imposti dagli standard di certificazione, controllando al contempo il costo del processo di testing. Allo stesso tempo, lo sviluppo di software safety-critical è spesso vincolato da linguaggi di programmazione o convenzioni di codifica che vietano caratteristiche del codice che si ritiene riducano la sicurezza dei programmi, ad esempio, non consentono l'allocazione dinamica della memoria e array di lunghezza variabile, limitano il modo in cui vengono utilizzati i cicli, proibiscono la ricorsione e limitano la complessità delle condizioni di controllo. Abbiamo sfruttato generatori di test allo stato dell’arte basati sull’esecuzione simbolica e il bounded model checking al fine di definire una toolchain originale per la generazione di casi test per programmi Scade. Abbiamo valutato l’efficacia della nostra toolchain nel generare i casi di test automaticamente con un benchmark di 37 programmi Scade sviluppati come parte di un sistema di segnalazione di bordo per sistemi ferroviari ad alta velocità sviluppato in collaborazione con un partner industriale.