| dc.description.abstract | Implementation level model checkers haven proven a good tool for identifying
bugs in implementations of distributed algorithms. In recent years many new
model checkers have been developed. These often include new state space reduction
techniques which increase their effectiveness, but they are often locked
to use a specific state space reduction technique and to support specific abstractions.
This makes it hard to compare different state space reduction techniques
and to change between different abstractions.
We propose Go-MC, a modular implementation level model checker for the
Go programming language. Go-MC consists of four modules: the Scheduler,
the State Manager, the Checker and the Failure Manager. Each module can
easily be swapped for different implementations, which makes it easy to change
between 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 utilize
specific frameworks or to mock components of distributed systems. This allows
us to take a modular approach when simulating distributed systems, which will
reduce the number of events in a simulation and thus reduce the size of the
state space. It also makes it possible to efficiently capture events and support
different frameworks. | |
