Design, verification and automatic implementation of correct-by-construction distributed transaction systems in Maude

Liu, Si

Permalink

https://hdl.handle.net/2142/104881 Copy

Description

Title

Design, verification and automatic implementation of correct-by-construction distributed transaction systems in Maude

Author(s)

Liu, Si

Issue Date

2019-04-19

Director of Research (if dissertation) or Advisor (if thesis)

Meseguer, José

Doctoral Committee Chair(s)

Meseguer, José

Committee Member(s)

• Gupta, Indranil
• Agha, Gul
• Ölveczky, Peter

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(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.

Graduation Semester

2019-05

Type of Resource

text

Permalink

http://hdl.handle.net/2142/104881

Copyright and License Information

Copyright 2019 Si Liu

Owning Collections