A Pattern-based deadlock-freedom analysis strategy for concurrent systems
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.
Cite
@article{arxiv.2207.08854,
title = {A Pattern-based deadlock-freedom analysis strategy for concurrent systems},
author = {Pedro Antonino and Augusto Sampaio and Jim Woodcock},
journal= {arXiv preprint arXiv:2207.08854},
year = {2022}
}