Designing Reliable Distributed Systems

A Formal Methods Approach Based on Executable Modeling in Maude

Peter Csaba Olveczky (Autor)

Buch | Softcover

313 Seiten

2018 | 1st ed. 2017
Springer London Ltd (Verlag)
978-1-4471-6686-3 (ISBN)

Artikel merken

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.

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.

Erscheint lt. Verlag	22.2.2018
Reihe/Serie	Undergraduate Topics in Computer Science
Zusatzinfo	6 Illustrations, color; 11 Illustrations, black and white; XVIII, 313 p. 17 illus., 6 illus. in color.
Verlagsort	England
Sprache	englisch
Maße	155 x 235 mm
Themenwelt	Informatik ► Grafik / Design ► Digitale Bildverarbeitung
	Mathematik / Informatik ► Informatik ► Netzwerke
	Mathematik / Informatik ► Informatik ► Software Entwicklung
	Mathematik / Informatik ► Informatik ► Theorie / Studium
Schlagworte	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 • Software engineering • temporal logic • Term Rewriting System
ISBN-10	1-4471-6686-8 / 1447166868
ISBN-13	978-1-4471-6686-3 / 9781447166863
Zustand	Neuware