Lecture Notes for an Introductory Course on Formal Modeling and Analysis of Distributed Systems using Maude

By Peter Csaba Ölveczky

These (still somewhat unfinished) notes comprise the lecture notes for an introductory course on formal modeling and analysis using the state-of-the-art formal language and tool Maude.

These notes can serve as a basic and too long introduction to Maude, and do not assume any previous knowledge of algebraic specification (or anything else for that matter, except some experience in programming). They are intended for a first taste of formal methods for third-year students at the Department of Informatics, University of Oslo.

The course is not just a tutorial on Maude, and must therefore include some theory. These theoretical parts focus on classic term rewriting theory, in particular on termination (and, to a lesser degree, on confluence), including the theory of simplification orderings.
The most parts deal with systems specification and analysis by specifying and executing systems in Maude.

The notes are full of exercises, both small and large.

The Lecture Notes

I am the copyright holder of these notes. You may freely use them for your own pleasure, but are not allowed to repost them without my explicit permission. In particular, all web references to the material should point to the page you are currently reading.

I will update the notes every now and then. In particular, I have to write the missing chapters!

Last update: January 15, 2010.

The lecture notes in pdf format

Feedback

I would appreciate it very much if anyone (except the INF 3230 students, who are supposed to read these notes!) who uses these notes to any extent, would notify me at peterol@ifi.uio.no.

Needless to say, any feedback on these notes is highly appreciated.

Outline of the Contents

These notes are divided into two parts:
  1. Equational specification:
    1. signatures, terms, equations, order-sorted specifications of all the usual data types (numbers, lists, multisets, binary trees, etc.)
    2. operational semantics: term rewriting (called reduction in these notes, in order not to confuse it with "rewriting" in a rewriting logic sense or with "simplification" as in "simplification orderings")
      • the reduction ("rewriting") relation
      • termination: "weight-based" orderings and simplification orderings, and their theory
      • confluence
      • equational attributes in Maude
      • example: quicksort
      • note that, while mentioning it, the course does not treat Knuth-Bendix completion in any detail
    3. equational logic: definition, deduction, (un)decidability results, Birkhoff's Theorem, inductive theorems and induction over data types
    4. Major-league omission: unfortunately, universal algebra and algebraic semantics of equational specifications turned out to be beyond the scope of this course, how matter how important, and no matter how much I wanted these topics included
  2. Rewriting logic for the modeling of distributed systems in Maude, and their analysis:
    1. dynamic systems: extremely simplified models of the life of a person/population, the Super Bowl, an entire NFL round, the coffee bean game, etc.
    2. rewriting logic: rewrite rules, definition of the logic, concurrent steps in rewriting logic, frozen operators
    3. execution in Maude: the commands rew, frew, and search
    4. object-oriented specification in (core) Maude and in Full Maude, the usual examples and the dining philosophers, subclasses
    5. Modeling communication:
      • different kinds of communication: asynchronous (through message passing), synchronous (through object collaboration), ordered/unordered, unicast/multicast, links, loss/duplication of messages (both with and without links), etc.
      • examples: the "separation" problem, the alternating bit protocol, the sliding window protocol
    6. Case study: the two-phase commit protocol in distributed databases
    7. "Properties": invariants and their analysis, other kinds of temporal properties (note: temporal logic and temporal logic model checking is, unfortunately, beyond the scope of this course)
    8. Case study from the security protocols world: modeling and analysis of the benchmark Needham-Schroeder public-key authentication protocol, including a minuscule introduction to the principles of cryptography and cryptographic protocols
While I think that the course covers a reasonable amount of ground, considering that it starts from scratch, there is so much more that could be included (but is not!) in such a course, including, in particular:
  1. reflection and meta-programming
  2. temporal logic and temporal logic model checking
  3. advanced security and communications protocols case studies
  4. extensions such as Real-Time Maude for specifying and analyzing real-time and hybrid systems
  5. Mobile Maude
  6. modeling cells and biological reactions using Maude
  7. modeling probabilistic systems
Many of these topics are instead treated in the follow-up course INF 5130.

peterol@ifi.uio.no