On the preservation of properties when changing communication models

DOI10.1007/978-3-031-23101-8_16MaRDI QIDQ6169530zbMATH OpenOpenAlexFDO

Authors Olav Bunte, Louis C. M. van Gool, T. A. C. Willemse

Publication date 14 August 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2210.06196

zbMATH Keywords

confluenceasynchronous communicationcommunication modelsproperty preservation

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: In a system of processes that communicate asynchronously by means of FIFO channels, there are many options in which these channels can be laid out. In this paper, we compare channel layouts in how they affect the behaviour of the system using an ordering based on splitting and merging channels. This order induces a simulation relation, from which the preservation of safety properties follows. Also, we identify conditions under which the properties reachability, deadlock freedom and confluence are preserved when changing the channel layout.

Recommendations

• Channel Properties of Asynchronously Composed Petri Nets
• Distributed Computing – IWDC 2005
• Publication:3479512
• First-order axioms for asynchrony
• Compatibility properties of synchronously and asynchronously communicating components

Cites work

• scientific article; zbMATH DE number 1569128 (Why is no real title available?)
• A hierarchy of communication models for message sequence charts
• Efficient property preservation checking of model refinements
• Non axiomatisability of positive relation algebras with constants, via graph homomorphisms
• On the diversity of asynchronous communication
• Property preserving abstractions for the verification of concurrent systems
• Temporal-logic property preservation under Z refinement
• Time, clocks, and the ordering of events in a distributed system
• Verification of flat FIFO systems
• Verification: Theory and Practice

Cited in

(1)

• On the Power of Attribute-Based Communication

This page was built for publication: On the preservation of properties when changing communication models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6169530)