Friday May 25'th 13.00 - 15.00
An Introductory Tutorial to Rewriting Logic and Maude
Peter Ölveczky, University of Oslo
Rewriting logic is a formal model of concurrency that was developed in the early
1990ies by José Meseguer. It is characterized by its general and expressive, yet simple
and intuitive, formalism. In rewiring logic, the static parts of a system (data types,
functions) are defined by an algebraic equational specification, and the system's
local transitions are defined by labeled conditional rewrite rules of the form
l: t -> t' if cond. In particular, rewriting logic provides a simple model for object-based
distributed systems, with multiple class inheritance, dynamic object and message
creation and deletion, etc.
Maude is a high-performance simulation, reachability, and temporal logic model checking
tool for rewriting logic. Because of the generality and expressiveness of rewriting logic, it
and Maude have been applied to a wide range of large applications. Some
of those application areas include:
- Semantic framework in which many programming languages (including the most
complete for semantics for C) and domain-specific modeling languages can be
given a formal semantics.
- Endowing such programming and modeling languages with formal analysis capabilities.
- Modeling and formal analysis of large state-of-the-art distributed systems, including
wireless sensor networks, large multicast protocols, as well as a "killer app" in which
parts of the Internet Explorer was formalized and where Maude analysis uncovered several
previously unknown security flaws (which delayed the release of the browser by months).
This talk is intended to be a practical introductory tutorial to Maude, where I start from
scratch and try to provide the basics to Maude modeling and analysis. I therefore do
not assume any familiarity with algebraic specification or term rewriting.
Friday June 1'st 13.00 - 15.00
Formal Specification and Analysis of Real-Time Systems in Real-Time Maude
Peter Ölveczky, University of Oslo
Real-Time Maude is a tool that extends the rewriting-logic-based Maude
system 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 temporal
logic model checking. Our tool is particularly suitable to specify
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 in advanced
state-of-the-art applications, including scheduling and wireless
sensor network algorithms, communication protocols,
and in finding several bugs in embedded car software that were not
found by standard model checking tools employed in industry.
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 MOMENT2. Real-Time Maude thereby
provides formal model checking capabilities for these languages.
This talk gives a high-level overview of Real-Time Maude and some of