Open Collections

Compiling distributed system specifications into implementations

University of British Columbia

Distributed systems are notoriously difficult to get right: the inherently asynchronous nature of their execution gives rise to a fundamentally non-deterministic system. Previous work has shown that the use of formal methods to reason about distributed systems is a promising area of research. In particular, model-checking allows developers to verify system models against a correctness specification by performing an exhaustive search over the system's possible executions. However, the transition from a trusted specification to a valid implementation is a manual, error-prone process that could introduce subtle, hard to find bugs. In this work, we aim to bridge this gap by automatically translating a specification into an implementation that refines it. Specifically, we leverage the clear separation between application-specific logic and abstract components in the Modular PlusCal language to define an interface that concrete implementations must follow in order to implement the abstractions. Our evaluation shows that this approach is able to handle complex specifications and generate systems that preserve the correctness properties verified via model-checking.

Text

2019-04-17

Attribution-NoDerivatives 4.0 International

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

Computer Science

University of British Columbia

UBCV

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