Go-MC - An implementation level model checker for Go
Master thesis
Permanent lenke
https://hdl.handle.net/11250/3084901Utgivelsesdato
2023Metadata
Vis full innførselSamlinger
- Studentoppgaver (TN-IDE) [823]
Sammendrag
Implementation level model checkers haven proven a good tool for identifyingbugs in implementations of distributed algorithms. In recent years many newmodel checkers have been developed. These often include new state space reductiontechniques which increase their effectiveness, but they are often lockedto use a specific state space reduction technique and to support specific abstractions.This makes it hard to compare different state space reduction techniquesand to change between different abstractions.
We propose Go-MC, a modular implementation level model checker for theGo programming language. Go-MC consists of four modules: the Scheduler,the State Manager, the Checker and the Failure Manager. Each module caneasily be swapped for different implementations, which makes it easy to changebetween different abstractions and scheduling techniques.
Go-MC also uses Event Managers to control the execution of the algorithm.Event Managers are flexible and custom implementations can be made to utilizespecific frameworks or to mock components of distributed systems. This allowsus to take a modular approach when simulating distributed systems, which willreduce the number of events in a simulation and thus reduce the size of thestate space. It also makes it possible to efficiently capture events and supportdifferent frameworks.