WRLA 2024

Luxembourg city. Photo by Manu on Unsplash

Workshop Program

Day 1 (Saturday, April 6)

Time Content
8:45 - 9:00 Opening
9:00 - 10:00
Session 1
Francisco Durán.
New advances in Maude 3.4 (invited tutorial).
10:00 - 10:30 Break
10:30 - 12:00
Session 2
Jose Meseguer.
Equivalence, and Property Internalization and Preservation for Equational Programs.
Canh Minh Do and Kazuhiro Ogata.
Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude.
Carlos Olarte, Carlos Ramirez, Camilo Rocha and Frank Valencia.
Unified Opinion Dynamic Modeling as Concurrent Set Relations in Rewriting Logic.
12:00 - 14:00 Lunch
14:00 - 16:00
Session 3
Francisco Durán.
NuITP: A New Theorem Prover for Maude Specifications (invited tutorial).
Kyungmin Bae, Santiago Escobar, Raúl López-Rueda, Jose Meseguer and Julia Sapiña.
Verifying Invariants by Deductive Model Checking.
Rubén Rubio, Narciso Marti-Oliet, Isabel Pita and Alberto Verdejo.
Specifying fairness constraints and model checking with non-intensional strategies.
16:00 - 16:30 Break
16:30 - 18:00
Session 4
Adrian Riesco.
The CafeInMaude tool set (invited tutorial).
Duong Dinh Tran and Kazuhiro Ogata.
Verifying safe memory reclamation in concurrent programs with CafeOBJ.

Day 2 (Sunday, April 7)

Time Content
9:00 - 10:00
Session 5
Peter Ölveczky.
Design and Validation of Cloud Storage Systems using Maude (invited tutorial).
10:00 - 10:30 Break
10:30 - 12:00
Session 6
Michael Lienhardt.
The hrewrite library: a term rewriting engine for automatic code assembly.
Geunyeol Yu and Kyungmin Bae.
A Flexible Framework for Integrating Maude and SMT Solvers Using Python.
Santiago Escobar, Narciso Marti-Oliet and Rubén Rubio.
Towards a strategy language for narrowing in Maude.
12:00 - 14:00 Lunch
14:00 - 16:00
Session 7
Kyungmin Bae.
Formal Model Engineering of Distributed Cyber-Physical Systems in AADL
using Maude (invited tutorial)
Tajana Ban Kirigin, Jesse Comer, Max Kanovich, Andre Scedrov and Carolyn Talcott.
Time-Bounded Resilience.
Carlos Olarte and Peter Csaba Ölveczky.
Timed Strategies for Real-Time Rewrite Theories.
16:00 - 16:30 Break
16:30 - 17:30
Session 8
Peter Ölveczky.
Teaching an Advanced Maude-based Formal Methods Course in Oslo.
Kazuhiro Ogata.
Teaching Functional Programming and Program Verification in CafeOBJ at JAIST.
17:30 - 17:45 Closing

Invited tutorial information

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.