Peter Csaba Olveczky

Formal specification and analysis of real-time systems in Real-Time Maude

Peter Csaba Ölveczky (Oslo University)

Slides of lecture 1 and lecture 2. Maude file.

Rewriting logic was developed by José Meseguer in the late 80ies as a computation logic for concurrent/distributed systems. In rewriting logic, data types are specified as algebraic equational specifications (i.e., as a terminating and confluent term rewrite system), and a system’s dynamic behaviors are specified by (not necessarily terminating or confluent) rewrite rules. Rewriting turned out to be a simple and intuitive, yet very general and flexible, computation logic in which many other models of concurrency, including concurrent objects, could be naturally represented.
Maude is a specification language and high-performance analysis tool for rewriting logic. It provides rewriting for simulation, reachability analysis, and explicit-state LTL and LTLR temporal logic model checking. Maude has more recently been equipped with symbolic analysis methods, such as narrowing and rewriting combined with SMT solving. Maude also uses the fact that rewriting logic is a reflective logic to provide meta-programming features.
Maude has been applied to a wide range of state-of-the-art applications, including: network/transport protocols, web browser security and computer security in general, biochemical systems, cyber-physical systems, and so on. Maude has also been a useful semantic framework that has provided a formal semantics and formal analysis methods to many programming and modeling languages.
Real-Time Maude is a tool that extends Maude to support the executable formal modeling and analysis of real-time systems. Real-Time Maude is characterized by its general and expressive, yet intuitive, specification formalism, and offers a spectrum of formal analysis methods, including: rewriting for simulation purposes, search for reachability analysis, and both untimed and metric temporal logic model checking. Real-Time Maude is particularly suitable for specifying real-time systems in an object-oriented style, and its flexible formalism makes it easy to model different forms of communication.
This modeling flexibility, and the usefulness of Real-Time Maude for both simulation and model checking, has been demonstrated on many advanced state-of-the-art applications, including both distributed protocols of different kinds and industrial embedded systems. Furthermore, Real-Time Maude’s expressiveness has also been exploited for defining the formal semantics of MDE languages for real-time/embedded systems, including Ptolemy discrete-event models, a subset of the avionics modeling standard AADL, and a timed extension of the MOMENT2 model transformation framework. Real-Time Maude thereby provides formal model checking capabilities for these languages for free, and such analysis has been integrated into the tool environment of a number of modeling languages.

Outline of the lecture

The first 60 minutes give an introduction to rewriting and the Maude tool and some of its applications. The rest of the course introduces Real-Time Maude and its timed analysis methods, discusses completeness issues, and gives an overview of applications of Real-Time Maude.

Exercises or experiments

Exercises to be solved using Maude and Real-Time Maude.

Bibliographical references

  1. José Meseguer: Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science 96(1): 73-155 (1992)
  2. José Meseguer: Twenty years of rewriting logic. The Journal of Logic and Algebraic Programming 81(7-8):721-781 (2012)
  3. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, Joséé Meseguer and Carolyn L. Talcott: All About Maud, vol. 4350 of Springer LNCS, 2007.
  4. José Meseguer: Symbolic Reasoning Methods in Rewriting Logic and Maude. Proc. WoLLIC 2018, vol. 10944 of Springer LNCS, 2018.
  5. Peter Csaba Ölveczky: Designing Reliable Distributed Systems – A Formal Methods Approach Based on Executable Modeling in Maude. Undergraduate Topics in Computer Science, Springer 2017.
  6. Grigore Rosu: Matching Logic. Logical Methods in Computer Science 13(4) (2017)
  7. Grigore Rosu: K: A Semantic Framework for Programming Languages and Formal Analysis Tools. Dependable Software Systems Engineering 2017: 186-206
  8. Peter Csaba Ölveczky: Real-Time Maude and Its Applications. Proc. WRLA 2014, vol 8663 of Springer LNCS.
  9. Peter Csaba Ölveczky, José Meseguer: The Real-Time Maude Tool. Proc. TACAS 2008, vol 4963 of Springer LNCS.

Comments are closed.