ADA Software Model Checking

The work presented in this thesis uses model checking to prove the absence/existence of concurrency problems in an industrial machine's software written in the Ada programming language. The aim is to develop a methodology to: (1) automatically generate a formal model of the Ada code (2) apply model checking on the generated model to prove the absence/existence of deadlocks/livelocks (3) automatically generate traceability from the model back to the Ada code.