Skip to main content
SpringerLink
Log in
Book cover

Integrated Model of Distributed Systems

  • Book
  • © 2020

Overview

Authors:
  1. Wiktor B. Daszczuk

    1. Institute of Computer Science, Warsaw University of Technology, Warsaw, Poland

    View author publications

    You can also search for this author in PubMed   Google Scholar

  • Proposes an original formalism, the IMDS, which reflects the natural features of distributed systems
  • General temporal formulas provide automatic verification of deadlocks and distributed termination in several forms
  • Written by an expert on the specification and verification of distributed systems

Part of the book series: Studies in Computational Intelligence (SCI, volume 817)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (12 chapters)

  1. Front Matter

    Pages i-xviii
    Download chapter PDF

  2. Introduction

    • Wiktor B. Daszczuk
    Pages 1-16

  3. Related Work on Deadlock and Termination Detection Techniques

    • Wiktor B. Daszczuk
    Pages 17-29

  4. Integrated Model of Distributed Systems

    • Wiktor B. Daszczuk
    Pages 31-48

  5. Model Checking of IMDS Specifications in the Dedan Environment

    • Wiktor B. Daszczuk
    Pages 49-51

  6. Deadlock Detection Examples: The Dedan Environment at Work

    • Wiktor B. Daszczuk
    Pages 53-85

  7. Using the Dedan Program

    • Wiktor B. Daszczuk
    Pages 87-97

  8. Deadlock Detection in Petri Net Equivalent to IMDS

    • Wiktor B. Daszczuk
    Pages 99-123

  9. Distributed Autonomous and Asynchronous Automata (DA3)

    • Wiktor B. Daszczuk
    Pages 125-137

  10. Fairness in Distributed Systems Verification

    • Wiktor B. Daszczuk
    Pages 139-159

  11. Timed IMDS

    • Wiktor B. Daszczuk
    Pages 161-192

  12. 2-Vagabonds: Non-exhaustive Verification Algorithm

    • Wiktor B. Daszczuk
    Pages 193-218

  13. Conclusions and Further Work

    • Wiktor B. Daszczuk
    Pages 219-226

  14. Back Matter

    Pages 227-238
    Download chapter PDF
Back to top

Keywords

About this book

In modern distributed systems, such as the Internet of Things or cloud computing, verifying their correctness is an essential aspect. This requires modeling approaches that reflect the natural characteristics of such systems: the locality of their components, autonomy of their decisions, and their asynchronous communication. However, most of the available verifiers are unrealistic because one or more of these features are not reflected. Accordingly, in this book we present an original formalism: the Integrated Distributed Systems Model (IMDS), which defines a system as two sets (states and messages), and a relation of  the "actions" between these sets. The server view and the traveling agent’s view of the system provide communication duality, while general temporal formulas for the IMDS allow automatic verification. The features that the model checks include: partial deadlock and partial termination, communication deadlock and resource deadlock. Automatic verification can supportthe rapid development of distributed systems. Further, on the basis of the IMDS, the Dedan tool for automatic verification of distributed systems has been developed.

Authors and Affiliations

  • Institute of Computer Science, Warsaw University of Technology, Warsaw, Poland

    Wiktor B. Daszczuk

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation