TESTING AND VERIFICATION METHODS FOR SAFETY CRITICAL SYSTEMS

This dissertation is the results of the experience at General Electric Transportation Systems (GETS). The Company is a railway signaling manufacturer that develops embedded platforms for railway signaling systems. The safety critical nature of these applications makes the verification activities extremely crucial to ensure dependability and to prevent failures. At the end of 2008 GETS decided to introduce new verification and testing methods inside the company processes to ensure higher code safety and cost effectiveness at same time. Traditionally in the railway context the unit test was the main technique adopted to detect design errors and ensure the correctness of the components before the final integration and validation phase. Testing activities normally require high costs and at the same time do not ensure that the software is completely free from errors. In the same context the need to evaluate functional correctness of applications before the final integration and validation phase persuaded the Company to investigate the applicability of Model Checking technique to verify railway applications. In this domain and with these research objectives collaboration between GETS and the Computer Engineering Department (D.S.I) of the University of Florence started. This work reports the results obtained during this collaboration going through methods, process, results of experimentations in the verification and testing domain of safety critical applications.