Skip to Main content Skip to Navigation

Formal Verification of distributed algorithms using PlusCal-2

Abstract : Designing sound algorithms for concurrent and distributed systems is subtle and challenging. These systems are prone to deadlocks and race conditions, and are therefore hard to reproduce. Formal verification is a key technique to model the system and its properties and then perform verification by means of model checking. Formal languages like TLA+ have the ability to describe complicated algorithms quite concisely, but algorithm designers often find it difficult to model an algorithm in the form of formulas. In this thesis, we present PlusCal-2 that aims at being similar to pseudo-code while being formally verifiable. PlusCal-2 improves upon Lamport?s PlusCal algorithm language by lifting some of its restrictions and adding new constructs. Our language is intended for describing algorithms at a high level of abstraction. Finite instances of algorithms described in PlusCal-2 can be verified through the TLC model checker. The second contribution presented in this thesis is a study of partial-order reduction methods using conditional and constant dependency relation. To compute conditional dependency for PlusCal-2 algorithms, we exploit their locality information and present them in the form of independence predicates. We also propose an adaptation of a dynamic partial-order reduction algorithm for a variant of the tlc model checker. As an alternative to partial order reduction based on conditional dependency, we also describe a variant of a static partial-order reduction algorithm for the tlc model checker that relies on constant dependency relation. We also present our results for the experiments along with the proof of correctness
Document type :
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download
Contributor : Thèses Ul Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 12:08:17 PM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM
Long-term archiving on: : Friday, September 14, 2018 - 9:44:02 PM


Files produced by the author(s)


  • HAL Id : tel-01749162, version 1


Sabina Akhtar. Formal Verification of distributed algorithms using PlusCal-2. Other [cs.OH]. Université de Lorraine, 2012. English. ⟨NNT : 2012LORR0014⟩. ⟨tel-01749162v1⟩



Les métriques sont temporairement indisponibles