Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs

Si Liu, Atul Sandur, José Meseguer, Peter Csaba Ölveczky, Qi Wang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Developing a reliable distributed system meeting desired performance requirements is a hard and labor-intensive task. Formal specification and analysis of a system design can yield correct designs as well as reliable performance predictions. In this paper we present a correct-by-construction automatic transformation mapping such a verified formal specification of a system design in Maude to a distributed implementation satisfying the same safety and liveness properties. Two case studies applying this transformation to state-of-the-art distributed transaction systems show that high-quality implementations with acceptable performance and meeting performance predictions can be automatically generated. In this way, formal models of distributed systems analyzed within the same formal framework for both logical and performance properties are automatically transformed into correct-by-construction implementations for which similar performance trends can be shown.

Original languageEnglish (US)
Title of host publicationNASA Formal Methods - 12th International Symposium, NFM 2020, Proceedings
EditorsRitchie Lee, Susmit Jha, Anastasia Mavridou
PublisherSpringer
Pages22-40
Number of pages19
ISBN (Print)9783030557539
DOIs
StatePublished - 2020
Event12th International Symposium on NASA Formal Methods, NFM 2020 - Moffett Field, United States
Duration: May 11 2020May 15 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12229 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Symposium on NASA Formal Methods, NFM 2020
CountryUnited States
CityMoffett Field
Period5/11/205/15/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs'. Together they form a unique fingerprint.

Cite this