Model Checking Distributed Algorithms

Master Thesis Topics

• An Interactive Spin (NuSMV) Debugger

  Model checkers usually support interactive model execution using either random simulation or simulation guided by a counterexample. This mode is designed as a backend to a sophisticated graphical user interface, which as a rule is postponed for a future implementation. Thus a user is left with a choice of debugging a model of a concurrent program (or of a distributed algorithm) mentally or with a help of an awkward interactive text interface. The goal of this work is to develop an interactive debugger for a well-known model checker like Spin on top of an established IDE, e.g. Eclipse. The debugger should support common features such as breakpoints, next step, run to a specified location, display of current variables, display of processes instruction counters. However, the debugger should support two more features that are not present in the traditional debuggers of sequential programs. These are a backward step of a model and a non-deterministic choice between several steps.

  [Contact: Igor Konnov, Josef Widder] 

• A Translator of Distributed Algorithms to Spin (NuSMV, UPPAAL) with Support for User Provided Abstractions

  Currently, if one wants to verify or simulate a distributed algorithm in a model checker, e.g. Spin, NuSMV, UPPAAL, she has to perform all the translation from one description to another manually by choosing proper abstractions. Though some abstractions could be non-trivial and require human ingenuity, usually people start with a well-known set of techniques. Thus, there is a need in a translation tool that receives a distributed algorithm written in a fixed language on its input as well as a set of abstraction annotations and then translates the algorithm into the language of Spin (NuSMV, UPPAAL) by applying the abstractions. The goal of this work is to provide the distributed algorithms community with a tool that performs the first step of model extraction in an automatic way.

  [Contact: Igor Konnov, Josef Widder]