{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/104881"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/104881","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Design, verification and automatic implementation of correct-by-construction distributed transaction systems in Maude","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Liu, Si"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Meseguer, José","Gupta, Indranil","Agha, Gul","Ölveczky, Peter"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019-08-23T19:55:48Z","date_published":"2019-08-23T19:55:48Z","updated_at":"2026-07-22T22:24:42Z","subjects":["Model Checking, Distributed Transaction Systems, Consistency Model, Maude, Formal Specification and Verification, Correct-By-Construction Program Generation"],"languages":["en"],"rights":["Copyright 2019 Si Liu"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/104881","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Meseguer, José","Gupta, Indranil","Agha, Gul","Ölveczky, Peter"]},{"key":"dc:creator","label":"Author","values":["Liu, Si"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2019-08-23T19:55:48Z","2019-04-19","2019-05"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Model Checking, Distributed Transaction Systems, Consistency Model, Maude, Formal Specification and Verification, Correct-By-Construction Program Generation"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2019 Si Liu"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/104881"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-08-22 without embargo terms","The student, Si Liu, accepted the attached license on 2019-04-19 at 09:40.","The student, Si Liu, submitted this Dissertation for approval on 2019-04-19 at 09:44.","This Dissertation was approved for publication on 2019-04-19 at 10:05.","DSpace SAF Submission Ingestion Package generated from Vireo submission #13778 on 2019-08-22 at 14:45:03","Made available in DSpace on 2019-08-23T19:55:48Z (GMT). No. of bitstreams: 2 LIU-DISSERTATION-2019.pdf: 1593967 bytes, checksum: b93b89727d4b1c0a7a7d8ee02716e000 (MD5) LICENSE.txt: 4203 bytes, checksum: 8f296366811378aa94237b8c516e0358 (MD5) Previous issue date: 2019-04-19"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Design, verification and automatic implementation of correct-by-construction distributed transaction systems in Maude"]}]}],"canonical_facts":{"dc:contributor":["Meseguer, José","Gupta, Indranil","Agha, Gul","Ölveczky, Peter"],"dc:creator":["Liu, Si"],"dc:date":["2019-08-23T19:55:48Z","2019-04-19","2019-05"],"dc:description":["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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-08-22 without embargo terms","The student, Si Liu, accepted the attached license on 2019-04-19 at 09:40.","The student, Si Liu, submitted this Dissertation for approval on 2019-04-19 at 09:44.","This Dissertation was approved for publication on 2019-04-19 at 10:05.","DSpace SAF Submission Ingestion Package generated from Vireo submission #13778 on 2019-08-22 at 14:45:03","Made available in DSpace on 2019-08-23T19:55:48Z (GMT). No. of bitstreams: 2 LIU-DISSERTATION-2019.pdf: 1593967 bytes, checksum: b93b89727d4b1c0a7a7d8ee02716e000 (MD5) LICENSE.txt: 4203 bytes, checksum: 8f296366811378aa94237b8c516e0358 (MD5) Previous issue date: 2019-04-19"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/104881"],"dc:language":["en"],"dc:rights":["Copyright 2019 Si Liu"],"dc:subject":["Model Checking, Distributed Transaction Systems, Consistency Model, Maude, Formal Specification and Verification, Correct-By-Construction Program Generation"],"dc:title":["Design, verification and automatic implementation of correct-by-construction distributed transaction systems in Maude"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:42Z"}