On the preservation of properties when changing communication models

DOI10.1007/978-3-031-23101-8_16arXiv2210.06196OpenAlexW4313429636MaRDI QIDQ6169530FDOQ6169530

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)

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.

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

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

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)

Cites Work

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

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)