Title: Formal Specification and Analysis of Distributed Systems using Maude

Abstract. Rewriting logic is a powerful and general, yet simple and intuitive, logic for specifying dynamic systems, and is particularly suitable to specify distributed computer systems in an object-oriented style.

Maude is a programming/modeling language and high-performance analysis tool for rewriting logic. Data types are defined by equational specifications (which operationally can be seen as rich term rewrite systems), while dynamic behaviors are specified by (possibly conditional) rewrite rules. Maude models can then be subjected to: simulation by rewriting; reachability analysis by search; temporal logic model checking; and various forms of theorem proving using associated tools. 

Maude has been successfully applied to a wide range of sophisticated systems, including: transport protocols, cloud-based distributed transaction systems, biological systems, human cognition, programming and modeling language semantics and analysis, electronic contracts, cyber-physical systems, and so on.

This talk gives an introduction to specification and analysis in Maude. It also briefly touches upon some applications of Maude, and extensions to real-time and probabilistic systems.

Title: Design and Validation of Cloud Storage Systems using Maude

Abstract. Today’s large cloud-based applications (e.g., Gmail, Telegram, etc.) store and manipulate enormous amounts of data, that, furthermore, must  be available all the time.  In addition, such applications must be both correct and have high performance.

To deal with large amounts of data while offering high availability and  throughput and low latency, cloud computing systems rely on distributed, partitioned, and replicated data stores. Such cloud storage systems are complex software artifacts that are very hard to design, analyze, and implement.

I argue that Maude, together with a statistical model checker such as PVeStA, should be a suitable tool to model and formally analyze both the correctness and the performance of complex cloud storage designs early in the development process. This is not only useful to arrive at correct designs, but also to very early compare the expected performance of different design choices.

I give an overview of the application of Maude to a wide range of state-of-the-art cloud transaction systems, such as Apache Cassandra, Google’s Megastore, UC Berkeley’s RAMP transactions, and variations of these.  I discuss how the model-based performance estimates relate to real implementations, and also how a correct design can be automatically transformed into a correct-by-construction distributed implementation that can execute real workloads (e.g., YCSB workloads).

Finally, I briefly summarize the experiences of the use of a different formal method for similar purposes by engineers at Amazon Web Services.