University of Twente Student Theses


ADA Software Model Checking

Krishnamurthy, Ramesh (2021) ADA Software Model Checking.

[img] PDF
Abstract: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.
Item Type:Essay (Master)
TNO, Eindhoven, The Netherlands
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Embedded Systems MSc (60331)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page