Introduction.- Part I: Equational Specifications and Their Analysis.- Equational Specification in Maude.- Operational Semantics of Equational Specifications.- Termination.- Confluence.- Equational Logic.- Models of Equational Specifications.- Part II: Specification and Analysis of Distributed Systems in Maude.- Modeling Distributed Systems in Rewriting Logic.- Executing Rewriting Logic Specifications in Maude.- Concurrent Objects in Maude.- Modeling Communication in Maude.- Modeling and Analyzing Transport Protocols.- Distributed Algorithms.- Analyzing a Cryptographic Protocol.- System Requirements.- Formalizing and Checking Requirements.- Real-Time and Probabilistic Systems.- Appendix A: Mathematical Preliminaries.

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.