TY - GEN
T1 - Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs
AU - Liu, Si
AU - Sandur, Atul
AU - Meseguer, José
AU - Ölveczky, Peter Csaba
AU - Wang, Qi
N1 - Funding Information:
Acknowledgments. We thank the anonymous reviewers for helpful comments on a previous version of this paper. This work has been partially supported by NRL under contract N00173-17-1-G002, and the National Science Foundation under grant NSF CCF 16-17401.
Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85089723351&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85089723351&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-55754-6_2
DO - 10.1007/978-3-030-55754-6_2
M3 - Conference contribution
AN - SCOPUS:85089723351
SN - 9783030557539
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 22
EP - 40
BT - NASA Formal Methods - 12th International Symposium, NFM 2020, Proceedings
A2 - Lee, Ritchie
A2 - Jha, Susmit
A2 - Mavridou, Anastasia
PB - Springer
T2 - 12th International Symposium on NASA Formal Methods, NFM 2020
Y2 - 11 May 2020 through 15 May 2020
ER -