WRLA 2024

1. New advances in Maude 3.4

by Francisco Durán, University of Málaga, Spain.

Maude is a High-Performance Logical Framework providing specification, programming, and verification of systems written in Rewriting Logic. This tutorial will report on the new features available in Maude 3.4.

2. NuITP: A New Theorem Prover for Maude Specifications

by Francisco Durán, University of Málaga, Spain.

NuITP is an inductive theorem prover for Maude equational specifications that combines powerful state-of-the-art techniques such as narrowing, equality predicates, constructor variant unification, order-sorted congruence closure, ordered rewriting, strategy-based rewriting, and several others in order to reason about Maude equational programs. This tutorial will introduce the main features of the tool through various examples.

3. The CafeInMaude tool set

by Adrian Riesco, Universidad Complutense de Madrid, Spain.

CafeOBJ is a specification language that has been used for verifying a wide variety of systems. In recent years, CafeInMaude, a CafeOBJ interpreter implemented in Maude, has served as the underlying platform for developing various formal tools to enhance the verification experience. Specifically, we have implemented: (i) the CafeInMaude Proof Assistant (CiMPA), an inductive theorem prover for CafeOBJ specifications; (ii) the CafeInMaude Proof Generator (CiMPG), which generates CiMPA scripts from proof scores; and (iii) the CafeInMaude Proof Generator & Fixer-Upper (CiMPG+F), which generates CiMPA scripts from scratch. We summarize the main features of these tools, the benchmarks used to evaluate them, and their future challenges.

4. Design and Validation of Cloud Storage Systems using Maude

by Peter Ölveczky, University of Oslo, Norway.

Today's large cloud-based applications (e.g., Gmail, Facebook, 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.

This talk summarizes work done in the context of UIUC's Center for Assured Cloud Computing to apply 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.

5. Formal Model Engineering of Distributed Cyber-Physical Systems in AADL using Maude

by Kyungmin Bae, Pohang University of Science and Technology, South Korea.

Formal model engineering, equipping industrial modeling tools with automatic formal analysis capabilities, is a promising way of integrating formal methods into the model development process. However, supporting formal model engineering for cyber-physical systems (CPSs) introduces several challenges. These include the high expressiveness of industrial modeling languages, the difficulty of exhaustive model-checking analysis due to asynchronous behaviors, and the intricate mix of advanced control programs with continuous behaviors typical in many CPSs.

This talk outlines our approach to supporting efficient formal model engineering for synchronous CPS designs using the industrial CPS modeling standard AADL. We have identified a suitable sublanguage of AADL, called Synchronous AADL, that can naturally define the synchronous designs of CPSs, including those with continuous behaviors. We have defined the formal semantics of Synchronous AADL in rewriting logic and developed the HybridSynchAADL tool, an extension of the OSATE tool environment for AADL with automatic formal analysis capabilities via Maude and SMT solving.

Our approach effectively addresses the challenges by leveraging the expressive power of Maude for control programs, integrating Maude and SMT solving for analyzing continuous behaviors, and focusing on synchronous designs to enhance analysis efficiency. Additionally, we show how synchronizers, such as PALS, TTA, and MSYNC, can verify the correctness of distributed CPS implementations based on their synchronous designs. We summarize our experiences on applications such as industrial avionics control systems, airplane turning algorithms, and collaborating drones.