Date of Award

3-27-2019

Document Type

Thesis

Degree Name

Master of Science (MS)

Department

Computer Science

First Advisor

Peiyi Tang

Abstract

TLA+ is a mathematically precise specification language based on set theory. We provide a reusable TLA+ module for specifying asynchronous message-passing systems. The syntax and semantics of the TLA+ language are introduced. An example algorithm is translated from pseudocode to TLA+ to show the new module's use. TLC is used to model-check the translated algorithm. An established parallel algorithm for detecting strongly connected components of a graph is translated to PlusCal, a pseudolanguage that can be mechanically translated into TLA+, then a formal correctness proof is given. This algorithm is one proposed to improve the efficiency of liveness checking in TLC.

Download

Share

COinS