Compiling distributed system specifications into implementations
department or school: Science, Faculty of
department or school: Computer Science, Department of
data provider: DSpace
degree campus: UBCV
creator: Costa, Renato Mascarenhas
issued: 2019-04-17T16:27:02Z
issued: 2019
related degree: Master of Science - MSc
degree grantor: University of British Columbia
description: 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.
aggregated CHO: https://circle.library.ubc.ca/rest/handle/2429/69745
note: Compiling Distributed System Specifications intoImplementationsbyRenato Mascarenhas CostaB. Computer Science, University of SaËo Paulo, 2012A THESIS SUBMITTED IN PARTIAL FULFILLMENTOF THE REQUIREMENTS FOR THE DEGREE OFMaster of ScienceinTHE FACULTY OF GRADUATE AND POSTDOCTORALSTUDIES(Computer Science)The University of British Columbia(Vancouver)April 2019c© Renato Mascarenhas Costa, 2019The following individuals certify that they have read, and recommend to the Fac-ulty of Graduate and Postdoctoral Studies for acceptance, the thesis entitled:Compiling Distributed System Specifications into Implementationssubmitted by Renato Mascarenhas Costa in partial fulfillment of the requirementsfor the degree of Master of Science in Computer Science.Examining Committee:Ivan Beschastnikh, Computer ScienceSupervisorRonald Garcia, Computer ScienceSupervisory Committee MemberiiAbstractDistributed systems are notoriously difficult to get right: the inherently asynchronousnature of their execution gives rise to a fundamentally non-deterministic system.Previous work has shown that the use of formal methods to reason about distributedsystems is a promising area of research. In particular, model-checking allows de-velopers to verify system models against a correctness specification by performingan exhaustive search over the systemâs possible executions. However, the transi-tion from a trusted specification to a valid implementation is a manual, error-proneprocess that could introduce subtle, hard to find bugs.In this work, we aim to bridge this gap by automatically translating a speci-fication into an implementation that refines it. Specifically, we leverage the clearseparation between application-specific logic and abstract components in the Mod-ular PlusCal language to define an interface that concrete implementations mustfollow in order to implement the abstractions. Our evaluation shows that this ap-proach is able to handle complex specifications and generate systems that preservet…
has type: Thesis/Dissertation
date issued: 2019-05
is shown at: 10.14288/1.0378287
language: eng
degree discipline: Computer Science
provider: Vancouver : University of British Columbia Library
publisher: University of British Columbia
rights: Attribution-NoDerivatives 4.0 International
rights URI: http://creativecommons.org/licenses/by-nd/4.0/
scholar level: Graduate
type: Text
identifier URI: http://hdl.handle.net/2429/69745