Skip to main content
main-content
Top

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.

Table of Contents

Chapter 1. Introduction

Abstract
Our society increasingly depends on large and complex computer systems. Our cars, airplanes, banks, power plants, social interactions, shopping activities, etc., are all controlled and/or mediated to a large extent by computer systems.
Peter Csaba Ölveczky

Equational Specifications and Their Analysis

Frontmatter

Chapter 2. Equational Specification in Maude

Abstract
This chapter describes how data types can be defined in Maude as equational specifications. Section 2.1 introduces specification and execution in Maude with some simple “Hello World!” examples specifying the natural numbers and the Boolean values. Section 2.2 defines many-sorted equational specifications and explains how Maude computes with equations.
Peter Csaba Ölveczky

Chapter 3. Operational Semantics of Equational Specifications

Abstract
Chapter 2 shows how to write equational specifications in Maude, but without explaining their precise meaning. This chapter, and Chapter 7, defines the meaning (or semantics) of equational specifications in different ways.
Peter Csaba Ölveczky

Chapter 4. Termination

Abstract
Termination (the absence of infinite computations) is a crucial property for both equational specifications and programs in general. Maude requires equational specifications to be terminating, but does not check it (for reasons that will be apparent). We must therefore be able to analyze whether or not a specification is terminating.
Peter Csaba Ölveczky

Chapter 5. Confluence

Abstract
This chapter explains how to check whether a terminating specification is confluent, which ensures that the result of evaluating an expression is independent of the choice of which equation is applied to a term, and where the selected equation is applied.
Peter Csaba Ölveczky

Chapter 6. Equational Logic

Abstract
This chapter explains how we can reason about whether two expressions are “logically equivalent” in a specification E. We consider two different notions of what it means that two terms t and u (which may contain variables) are logically equivalent:
Peter Csaba Ölveczky

Chapter 7. Models of Equational Specifications

Abstract
The introduction to this book says that the point of formal modeling is to define a mathematical model of a computer system.
Peter Csaba Ölveczky

Specification and Analysis of Distributed Systems in Maude

Frontmatter

Chapter 8. Modeling Distributed Systems in Rewriting Logic

Abstract
This chapter introduces rewriting logic , which can be used to model dynamic systems and to reason about concurrent change in a distributed system.
Peter Csaba Ölveczky

Chapter 9. Executing Rewriting Logic Specifications in Maude

Abstract
This chapter introduces some ways in which a rewriting logic model of a dynamic system can be analyzed by execution in Maude.
Peter Csaba Ölveczky

Chapter 10. Concurrent Objects in Maude

Abstract
A distributed system can be naturally modeled as an object system by modeling each component of the system as an object. The components may communicate with each other by sending and receiving messages. The state of a system can therefore be represented as a multiset of objects and messages traveling between the objects.
Peter Csaba Ölveczky

Chapter 11. Modeling Communication in Maude

Abstract
Chapter 10 explained how a concurrent system can be represented as a multiset of concurrent objects. This chapter shows how different forms of communication between such objects can be modeled in rewriting logic.
Peter Csaba Ölveczky

Chapter 12. Modeling and Analyzing Transport Protocols

Abstract
This chapter illustrates how (Full) Maude can be used to model and analyze a series of protocols for achieving reliable ordered communication on top of an underlying unreliable transmission medium.
Peter Csaba Ölveczky

Chapter 13. Distributed Algorithms

Abstract
This chapter shows how Maude can be used to formally model and analyze a number of textbook distributed algorithms; that is, algorithms (or protocols) in which a number of nodes use message passing communication to achieve a common goal.
Peter Csaba Ölveczky

Chapter 14. Analyzing a Cryptographic Protocol

Abstract
Web services such as email, photo, social networks, internet commerce, and online banking require that entities authenticate themselves. Scrooge McDuck must be sure that he (it?) is communicating with the bank, and not with some bad guy with a look-a-like web page. Likewise, when the bank gets the request “transfer 5 gazillions from my account to the Beagle Boys” from “Scrooge,” the bank must be sure that it is communicating with Scrooge and not with the Beagle Boys.
Peter Csaba Ölveczky

Chapter 15. System Requirements

Abstract
The previous chapters of this book explained how the behaviors of a system can be specified mathematically. Such a system specification must be complemented by a requirement specification defining the properties that the system must satisfy.
Peter Csaba Ölveczky

Chapter 16. Formalizing and Checking Requirements

Abstract
Chapter 15 discusses classes of requirements that a distributed system may have to satisfy.
Peter Csaba Ölveczky

Chapter 17. Real-Time and Probabilistic Systems

Abstract
The previous chapters abstract away timed and probabilistic aspects of distributed systems.
Peter Csaba Ölveczky
Additional information