Open Collections

Corresponding formal specifications with distributed systems

University of British Columbia

As the need for computing resources grows, providers are increasingly relying on distributed systems to render their services. However, distributed systems are hard to design and implement. As an aid for design and implementation, formal verifica- tion has seen a growing interest in industry. For example, Amazon uses Temporal Logic of Actions plus (TLA⁺) and PlusCal specification languages and tool chain to formally verify manually created specifications of their web services [8]. Nevertheless, there is currently no tool to automatically establish a correspon- dence between a PlusCal specification with a concrete implementation. Further- more, PlusCal was not designed with modularity in mind, so a large PlusCal spec- ification cannot be decomposed into smaller ones for ease of modification. This thesis proposes an extension to PlusCal, named Modular PlusCal, as well as a compiler, named PGo, which compiles Modular PlusCal and PlusCal specifications into Go programs. Modular PlusCal introduces new constructs, such as archetypes and mapping macros, to provide isolation and, as a result, modularity. By auto- matically compiling PlusCal and Modular PlusCal specifications into distributed system implementations, PGo reduces the burden on programmers trying to ensure the correctness of their distributed systems.

Text

2019-04-18

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/69795

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by-nc-nd/4.0/