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

by Peter Ölveczky

Wed, 19 January 2022 at 10:00 am in Salzburg, Austria

Joint work with: Si Liu, Atul Sandur, Jose Meseguer, Qi Wang

Abstract: Developing a reliable distributed system meeting desired performance requirements is a hard and labor-intensive task. Formal specification and analysis of a system \emph{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 \emph{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 \emph{logical} and \emph{performance} properties are automatically transformed into correct-by-construction implementations for which similar performance trends can be shown.