A Pattern-based deadlock-freedom analysis strategy for concurrent systems

TL;DR

This paper introduces a systematic method combining system decomposition and pattern-based local analysis to verify deadlock freedom in concurrent systems, supported by a prototype tool and practical case studies.

Contribution

It presents a novel approach that integrates behavioral pattern adherence with local analysis for deadlock verification, enhancing scalability and automation.

Findings

Effective deadlock analysis demonstrated on example systems

Prototype tool supports automated verification process

Method reduces state-space explosion issues

Abstract

Local analysis has long been recognised as an effective tool to combat the state-space explosion problem. In this work, we propose a method that systematises the use of local analysis in the verification of deadlock freedom for concurrent and distributed systems. It combines a strategy for system decomposition with the verification of the decomposed subsystems via adherence to behavioural patterns. At the core of our work, we have a number of CSP refinement expressions that allows the user of our method to automatically verify all the behavioural restrictions that we impose. We also propose a prototype tool to support our method. Finally, we demonstrate the practical impact our method can have by analysing how it fares when applied to some examples.