University of Twente Student Theses

Login

ADA Software Model Checking

Krishnamurthy, Ramesh (2021) ADA Software Model Checking.

[img] PDF
2MB
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)
Clients:
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:https://purl.utwente.nl/essays/86146
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page