Generating correct-by-construction distributed implementations from formal maude designs
By
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.
BibTeX
@inproceedings{10.1007/978-3-030-55754-6_2,
author = "Liu, Si and Sandur, Atul and Meseguer, Jos\'{e} and
\"{O}lveczky, Peter Csaba and Wang, Qi",
title = "Generating Correct-by-Construction Distributed
Implementations from Formal Maude Designs",
address = "Berlin, Heidelberg",
booktitle = "NASA Formal Methods: 12th International
Symposium, NFM 2020, Moffett Field, CA, USA, May 11–15, 2020,
Proceedings",
doi = "10.1007/978-3-030-55754-6_2",
ee = "https://doi.org/10.1007/978-3-030-55754-6_2",
isbn = "978-3-030-55753-9",
location = "Moffett Field, CA, USA",
numpages = "19",
pages = "22–40",
publisher = "Springer-Verlag",
year = "2020",
}