Designing Reliable Distributed Systems

A Formal Methods Approach Based on Executable Modeling in Maude

  • Peter Csaba Ölveczky

Part of the Undergraduate Topics in Computer Science book series (UTICS)

Table of contents

  1. Front Matter
    Pages i-xviii
  2. Peter Csaba Ölveczky
    Pages 1-8
  3. Equational Specifications and Their Analysis

    1. Front Matter
      Pages 9-9
    2. Peter Csaba Ölveczky
      Pages 11-58
    3. Peter Csaba Ölveczky
      Pages 59-66
    4. Peter Csaba Ölveczky
      Pages 67-84
    5. Peter Csaba Ölveczky
      Pages 85-91
    6. Peter Csaba Ölveczky
      Pages 93-108
    7. Peter Csaba Ölveczky
      Pages 109-124
  4. Specification and Analysis of Distributed Systems in Maude

    1. Front Matter
      Pages 125-125
    2. Peter Csaba Ölveczky
      Pages 127-144
    3. Peter Csaba Ölveczky
      Pages 145-154
    4. Peter Csaba Ölveczky
      Pages 155-182
    5. Peter Csaba Ölveczky
      Pages 183-198
    6. Peter Csaba Ölveczky
      Pages 199-210
    7. Peter Csaba Ölveczky
      Pages 211-232
    8. Peter Csaba Ölveczky
      Pages 233-248
    9. Peter Csaba Ölveczky
      Pages 249-262
    10. Peter Csaba Ölveczky
      Pages 263-282
    11. Peter Csaba Ölveczky
      Pages 283-298
  5. Back Matter
    Pages 299-313

About this book


This classroom-tested textbook provides an accessible introduction to the design, formal modeling, and analysis of distributed computer systems. The book uses Maude, a rewriting logic-based language and simulation and model checking tool, which offers a simple and intuitive modeling formalism that is suitable for modeling distributed systems in an attractive object-oriented and functional programming style.

Topics and features:

  • Introduces classical algebraic specification and term rewriting theory, including reasoning about termination, confluence, and equational properties
  • Covers object-oriented modeling of distributed systems using rewriting logic, as well as temporal logic to specify requirements that a system should satisfy
  • Provides a range of examples and case studies from different domains, to help the reader to develop an intuitive understanding of distributed systems and their design challenges
  • Examples include classic distributed systems such as transport protocols, cryptographic protocols, and distributed transactions, leader election, and mutual execution algorithms
  • Contains a wealth of exercises, including larger exercises suitable for course projects, and supplies executable code and supplementary material at an associated website

This self-contained textbook is designed to support undergraduate courses on formal methods and distributed systems, and will prove invaluable to any student seeking a reader-friendly introduction to formal specification, logics and inference systems, and automated model checking techniques.

Dr. Peter Csaba Ölveczky is a Professor in the Department of Informatics at the University of Oslo, Norway.




Abstract Data Types Algebraic and Order-Sorted Specification Communication and Cryptographic Protocols Confluence and Termination Equational and Rewriting Logic Inductive Theorems Model Checking Object-Oriented Modeling Quick-Sort and Merge-Sort Reachability Analysis Simplification and Path Orderings Simulation Temporal Logic Term Rewriting System

Authors and affiliations

  • Peter Csaba Ölveczky
    • 1
  1. 1.University of OsloOsloNorway

Bibliographic information

Industry Sectors
Chemical Manufacturing
Finance, Business & Banking
IT & Software
Consumer Packaged Goods
Energy, Utilities & Environment