Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs
Author(s)
Liu, Si
Sandur, Atul
Meseguer, Jose
Ölveczky, Peter
Wang, Qi
Issue Date
2019-12
Keyword(s)
Distributed Systems
Formal Specification and Verification
Correct-By-Construction Program Generation
Maude
Abstract
Developing a reliable distributed system meeting desired performance requirements is a hard and very labor-intensive task. Formal specification of a system design and formal analysis can yield provably correct designs as well as reliable performance predictions. But there is still a formality gap between verified designs and distributed implementations. We present a correct-by-construction automatic transformation mapping a formal specification of a system design M in Maude to a distributed implementation D(M) with the same safety and liveness properties as M. 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 obtained in this way. To the best of our knowledge, this is the first time that 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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
