Integrated Model of Distributed Systems

1. Front Matter

   Pages i-xviii

   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

    PDF

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.

• Computational Intelligence
• IMDS
• Integrated Model of Distributed Systems
• Distributed Systems
• Dedan Program
• Specification and Automatic Verification

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

  Wiktor B. Daszczuk

Policies and ethics