Master Thesis: Verification of Systems-of-Systems using Model Checking
Type: Master thesis
Student: Max Kitzing
Supervisor: Prof. Dr. Andreas Harth, Dr. rer. nat. Victor Charpenay
Abstract: The thesis explores the possibility of verifying software with the well-known TLA+ model checker on a complex information system made of of independent component systems, each with its own development schedule and objectives. Specifically, the thesis addresses two research questions: (1) How can low-level implementation code be transformed to a TLA+ specification? (2) How can TLA+ specifications theoretically be abstracted, to prevent scalability issues from arising? The results of the thesis will be tested on elements of the DATEV software code base.