Deadlock and Termination Detection using IMDS Formalism and Model Checking. Version 2

TL;DR

This paper introduces a formalism called IMDS combined with model checking to effectively detect local deadlocks and termination issues in distributed systems, overcoming limitations of traditional global state-based methods.

Contribution

The paper presents IMDS, a dual-view formalism for distributed systems, and integrates it with model checking to facilitate local deadlock and termination detection.

Findings

IMDS allows expressing local features of subsystems.

It differentiates deadlock from termination.

The approach detects various deadlock types in distributed systems.

Abstract

Modern model checking techniques concentrate on global properties of verified systems, because the methods base on global state space. Local features like partial deadlock or process termination are not easy to express and check. In the paper a description of distributed system in an Integrated Model of Distributed Systems (IMDS) combined with model checking is presented. IMDS expresses a dualism in distributed systems: server view and agent view. The formalism uses server states and messages. A progress in computations is defined in terms of actions consuming and producing states and messages. Distributed actions are totally independent and they do not depend on global state. Therefore, IMDS allows the designer to express local features of subsystems. In this model it is easy to describe various kinds of deadlock (including partial deadlock) and to differentiate deadlock from termination. The integration of IMDS with model checking is presented. Temporal formulas testing various kinds of deadlock (in communication or over resources) and termination are proposed.