MODELING AND ANALYSIS OF REAL-TIME SYSTEMS IN REWRITING LOGIC

Peter Csaba Ölveczky (University of Oslo)

Rewriting logic was developed by José Meseguer in the late 1980s as a simple and intuitive, yet general and expressive, computational logic for 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.

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 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. Like Maude, Real-Time Maude is characterized by its general and expressive, yet intuitive, specification formalism, and the tool 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.

This modeling flexibility, and the usefulness of Real-Time Maude has been demonstrated on many advanced state-of-the-art applications, including both distributed protocols of different kinds and industrial embedded systems, as well as to model and analyze co-simulation and human multitasking. 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 II 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 lectures

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.

The lectures will be fairly self-contained and high-level, and should therefore be possible to follow for attendees with background in term rewrite systems, e.g., corresponding to that provided by the basic course of ISR.

Exercises

Exercises on both rewriting logic/Maude and real-time systems/Real-Time Maude will be given.

Key references/background

• José Meseguer: Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science 96(1): 73-155 (1992)

• José Meseguer: Twenty years of rewriting logic. The Journal of Logic and Algebraic Programming 81(7-8):721-781 (2012)

• Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Marti-Oliet, José Meseguer and Carolyn L. Talcott: All About Maude, vol. 4350 of Springer LNCS, 2007.

• Clavel et al.: Maude Manual (Version 3.2.1). Available at http://maude.cs.illinois.edu

• Peter Csaba Ölveczky: Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude. Undergraduate Topics in Computer Science, Springer 2017.

• Peter Csaba Ölveczky: Real-Time Maude and Its Applications. Proc. WRLA 2014, vol 8663 of Springer LNCS.

• Peter Csaba Ölveczky, José Meseguer: The Real-Time Maude Tool. Proc. TACAS 2008, vol 4963 of Springer LNCS.