Electrum: A Verification Tool Applied To Distributed System Designs

Speaker: Julien Brunel & David Chemouil , ONERA DTIS & Federal University of Toulouse (France)

Date: Wednesday, April 17, 2019

Time: 4:00 PM to 5:00 PM

Public: Yes

Location: 32-G882

Event Type: Seminar

Room Description:

Host: Daniel Jackson, MIT-CSAIL

Contact: Maria Rebelo, 617-253-5895, mr@csail.mit.edu

Relevant URL:

Speaker URL: None

Speaker Photo:
None

Reminders to: seminars@csail.mit.edu

Reminder Subject: TALK: Electrum: A Verification Tool Applied To Distributed System Designs

Until now, designers of distributed systems and algorithms who want to verify the correctness of their work have had to choose between a variety of unsatisfactory options: (1) theorem provers, which offer complete confidence but tend to require considerable expertise and effort; (2) model checkers, which offer complete automation, but cannot handle complex data structures and configurations; and (3) tools such as Alloy, which are automated and handle complex data structures but do not provide temporal properties.

Electrum is a new tool based on Alloy that combines Alloy’s ability to check complex structures with a model checker’s ability to check temporal properties. It provides a logic with connectives from linear temporal logic (with past) and primed variables à la TLA+ that augments the relational constraint language of Alloy. The analysis of models can be translated into both a SAT-based bounded model-checking problem, and to an LTL-based unbounded model-checking problem.

Electrum has proved to be useful to model and verify dynamic systems with rich configurations. In this talk, we’ll illustrate its use on an application to Chord, a scalable distributed hash table (DHT) developed at MIT. Because Chord combines data structures, asynchronous communications, concurrency, and robustness, it is an interesting challenge target for formal specification and verification.

In this talk, we will present Electrum briefly, and then report on analyzing the correctness of Chord using Electrum, on small instances of networks. We will explain how the analysis found problems not discovered in previous work. We explain how we fixed all these issues and provided a version of the protocol for which we were not able to find any counterexamples using our method.

Research Areas:

Impact Areas:

This event is not part of a series.

Created by Maria Rebelo Email at Tuesday, April 16, 2019 at 4:46 PM.