University of Twente Student Theses
ADA Software Model Checking
Krishnamurthy, Ramesh (2021) ADA Software Model Checking.
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