Model Checking of Fault-tolerant Distributed Algorithms

Master Thesis Topics

  • Bounded Model Checking for Fault-tolerant Distributed Algorithms

Fault-tolerant distributed algorithms are not the ones that can be easily analysed with software model checkers. One reason for that is reach non-determinism exposed in system executions. The simplest example is a non-deterministic choice of an element from a set as written in the process code. Another example is the non-determinstic scheduling policy, that is, at each step the scheduler can pick an arbitrary process to continue the execution. Finally, when the faults come into play, they dramatically change executions in the system. Recently, we discovered a theoretically efficient way to apply bounded model checking to an important class of fault-tolerant algorithms. Our preliminary experiments showed that this technique allows us to verify the algorithms that were too large for the standard model checkers. We have many ideas of an efficient implementation of this technique. We believe that experimental results with such a tool may result in several publications at prestigious international conferences. To implement the tool, one should be familiar with (or willing to learn) SAT, SMT, and OCaml.

[Contact: Igor KonnovJosef Widder

  • 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]

Latest News

FORSYTE organizes CAV 2018

The FORSYTE group is co-organizing the 30th International Conference on Computer Aided Verification (CAV), which will take place in Oxford from July 14-17, 2018, as part of the Federated Logic Conference (FLoC). CAV is the leading conference on theory and practice of computer-aided formal verification for hardware and software systems. The paper submission deadline is […]

Continue reading

FMSD Special Issue in Memoriam Helmut Veith

In memory of Helmut Veith, the founder of the FORSYTE research group, the current issue of the Journal on Formal Methods in System Design is a Special Issue in Memoriam Helmut Veith. Helmut unexpectedly passed away in March 2016; he was a brilliant researcher, inspiring collaborator, passionate mentor, generous friend, and valued member of the […]

Continue reading

Helmut Veith Stipend 2017: Deadline Extension (November 30)

The application deadline for the Helmut Veith Stipend 2017 has been extended to November 30. The stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. We encourage all female master’s students attending (or planning to attend) […]

Continue reading

Helmut Veith Stipend 2017

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

Full news archive