[MA] Verification of Systems-of-Systems using Model Checking

Start: 01.10.2020

End: 20.05.2021

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.