Electrum: A Verification Tool Applied To Distributed System Designs
Julien Brunel & David Chemouil
, ONERA DTIS & Federal University of Toulouse (France)
Date: Wednesday, April 17, 2019
Time: 4:00 PM to 5:00 PM
Event Type: Seminar
Host: Daniel Jackson, MIT-CSAIL
Contact: Maria Rebelo, 617-253-5895, firstname.lastname@example.org
Speaker URL: None
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.
Created by Maria Rebelo at Tuesday, April 16, 2019 at 4:46 PM.