Files in this item



application/pdfLIU-DISSERTATION-2019.pdf (2MB)
(no description provided)PDF


Title:Design, verification and automatic implementation of correct-by-construction distributed transaction systems in Maude
Author(s):Liu, Si
Director of Research:Meseguer, José
Doctoral Committee Chair(s):Meseguer, José
Doctoral Committee Member(s):Gupta, Indranil; Agha, Gul; Ölveczky, Peter
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Model Checking, Distributed Transaction Systems, Consistency Model, Maude, Formal Specification and Verification, Correct-By-Construction Program Generation
Abstract:Designing, verifying, and implementing highly reliable distributed systems is at present a hard and very labor-intensive task. Cloud-based systems have further increased this complexity due to the desired consistency, availability, scalability, and disaster tolerance. This dissertation addresses this challenge in the context of distributed transaction systems (DTSs) from two complementary perspectives: (i) designing DTSs with high assurance such that they satisfy desired correctness and performance requirements; and (ii) transforming verified system designs into correct-by-construction distributed implementations. Regarding correctness requirements, we provide an object-based framework for formally modeling DTSs in Maude, explain how such models can be automatically instrumented to record relevant events during a run, formally define a wide range of consistency properties on such histories of events, and implement a tool which fully automates the entire specification instrumentation and model checking process. Regarding performance requirements, we propose a general, though not yet automated, method that transforms the untimed, non-probabilistic, and nondeterministic formal Maude models of DTSs into probabilistic rewrite theories, explain how we can monitor the system executions of such probabilistic theories, and shows how we can evaluate the performance of the DTS designs based on the recorded log for different performance parameters and workloads by statistical model checking. To bridge the formality gap between verified designs and distributed implementations we present a correct-by-construction automatic transformation mapping a verified formal specification of an actor-based distributed system design in Maude to a distributed implementation enjoying the same safety and liveness properties as the original formal design. Two case studies, applying this automatic transformation to state-of-the-art DTSs analyzed within the same formal framework for both logical and performance properties, show that high-quality implementations with acceptable performance and meeting performance predictions can be automatically generated in this way.
Issue Date:2019-04-19
Rights Information:Copyright 2019 Si Liu
Date Available in IDEALS:2019-08-23
Date Deposited:2019-05

This item appears in the following Collection(s)

Item Statistics