Corresponding formal specifications with distributed systems
department or school: Science, Faculty of
department or school: Computer Science, Department of
data provider: DSpace
degree campus: UBCV
creator: Do, Minh Nhat
issued: 2019-04-18T18:02:14Z
issued: 2019
related degree: Master of Science - MSc
degree grantor: University of British Columbia
description: 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.
aggregated CHO: https://circle.library.ubc.ca/rest/handle/2429/69795
note: Corresponding formal specificationswith distributed systemsbyMinh Nhat DoB. Eng, Nanyang Technological University, 2014A 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©Minh Nhat Do, 2019The following individuals certify that they have read, and recommend to the Fac-ulty of Graduate and Postdoctoral Studies for acceptance, the thesis entitled:Corresponding formal specificationswith distributed systemssubmitted by Minh Nhat Do in partial fulfillment of the requirements for the de-gree of Master of Science in Computer Science.Examining Committee:Ivan Beschastnikh, Computer ScienceSupervisorWilliam Bowman, Computer ScienceSupervisory Committee MemberiiAbstractAs the need for computing resources grows, providers are increasingly relying ondistributed systems to render their services. However, distributed systems are hardto design and implement. As an aid for design and implementation, formal verifica-tion has seen a growing interest in industry. For example, Amazon uses TemporalLogic of Actions plus (TLA+) and PlusCal specification languages and tool chainto 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. Thisthesis proposes an extension to PlusCal, named Modular PlusCal, as well as acompiler, named PGo, which compiles Modular PlusCal and PlusCal specificationsinto Go programs. Modular PlusCal introduces new constructs, such as archetypesand mapping macros, to provide isolation and, as a result, modularity. By auto-matically compiling PlusCal and Modular PlusCal specific…
note: "18 }19 }Figure 4.15: Configuration file for PGo4.2.1 Configuration parsingThe configuration parsing stage parses command line arguments and the configu-ration file. Figure 4.14 shows the command line arguments accepted by PGo. Ifthe programmer turns on compilation from Modular PlusCal to PlusCal, the pathto the configuration file is not required. The configuration file is expected to be avalid JSON object with attributes shown in Figure 4.15. We now overview each ofthe configuration parameters, starting with build.BuildThe build object is required. The output_dir attribute is required and must bean existing path. The programmer must provide either dest_file or dest_package36attribute; if both are provided, dest_package takes precedence. The dest_file at-tributes specifies the name of the output file. The dest_package attribute specifiesthe name of the output Go package.NetworkingThe networking object is optional. If it is not specified, PGo produces a multi-threaded Go program as output. The optional enabled attribute specifies whethernetworking is enabled. The state attribute specifies the configuration for the net-worked state strategy. If the state object is present, enabled is overridden to be true.The strategy attribute specifies which state strategy to use. PGo currently sup-ports state-server and etcd, with state-server being the default. The endpointsattribute specifies the etcd endpoints to connect to. The endpoints attribute is re-quired if strategy is etcd. The peers attribute specifies the peer endpoints to con-nect to. The optional timeout attribute specifies the network timeout in seconds,which defaults to three seconds.ConstantsThe constants object is optional. It contains key-value pairs whose key is the nameof the constant, encoded as a JSON string, and whose value is a TLA+ expression,also encoded as a JSON string.4.2.2 Type inferenceSince Go, the target language, is a statically typed language, PGo introduces a typesystem for effective compilatio…
has type: Thesis/Dissertation
date issued: 2019-05
is shown at: 10.14288/1.0378335
language: eng
degree discipline: Computer Science
provider: Vancouver : University of British Columbia Library
publisher: University of British Columbia
rights: Attribution-NonCommercial-NoDerivatives 4.0 International
rights URI: http://creativecommons.org/licenses/by-nc-nd/4.0/
scholar level: Graduate
type: Text
identifier URI: http://hdl.handle.net/2429/69795