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

Pedro Antonino; Augusto Sampaio; Jim Woodcock

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

Pedro Antonino, Augusto Sampaio, Jim Woodcock

Computer Science

Research output: Working paper › Preprint

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.

Original language	Undefined/Unknown
Publisher	Arxiv (Cornell University)
Publication status	Published - 18 Jul 2022

Keywords

cs.SE
cs.FL

Access to Document

2207.08854v1

Cite this

@techreport{32f1b922a7994d59a5141a666b2c3f88,

title = "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.",

keywords = "cs.SE, cs.FL",

author = "Pedro Antonino and Augusto Sampaio and Jim Woodcock",

year = "2022",

month = jul,

day = "18",

language = "Undefined/Unknown",

publisher = "Arxiv (Cornell University)",

type = "WorkingPaper",

institution = "Arxiv (Cornell University)",

}

TY - UNPB

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

AU - Antonino, Pedro

AU - Sampaio, Augusto

AU - Woodcock, Jim

PY - 2022/7/18

Y1 - 2022/7/18

N2 - 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.

AB - 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.

KW - cs.SE

KW - cs.FL

M3 - Preprint

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

PB - Arxiv (Cornell University)

ER -