By the same authors

A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

Title of host publicationFM 2014: Formal Methods
DatePublished - 2014
Pages62-77
PublisherSPRINGER
EditorsCliff Jones, Pekka Pihlajasaari, Jun Sun
Volume8442
Original languageEnglish
ISBN (Print)978-3-319-06409-3

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume8442

Abstract

Based on a characterisation of process networks in the CSP process algebra, we formalise a set of behavioural restrictions used for local deadlock analysis. Also, we formalise two patterns, originally proposed by Roscoe, which avoid deadlocks in cyclic networks by performing only local analyses on components of the network; our formalisation systematises the behavioural and structural constraints imposed by the patterns. A distinguishing feature of our approach is the use of refinement expressions for capturing notions of pattern conformance, which can be mechanically checked by CSP tools like FDR. Moreover, three examples are introduced to demonstrate the effectiveness of our strategy, including a performance comparison between FDR default deadlock assertion and the verification of local behavioural constraints induced by our approach, also using FDR.

Bibliographical note

Self-archiving of Final published version not supported by the publisher.

Projects

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations