By Konstantin Amelichev under supervise of Oleg Sukhoroslov
During the testing of distributed systems, it is crucial to examine all possible states that the system can get into. This research uses model checking as a formal method to test distributed systems within the context of the "Distributed Systems" course assignments. The simulations are conducted using the DSLab framework. We propose various optimizations for model checking, including the DependencyResolver module, as well as the introduction of two special workflows: Instant and Collect modes. These methods have successfully discovered over 10 previously unknown bugs in the archive of assignment solutions.
Keywords: Model checking, distributed systems, automated software testing, discrete event simulation.