English

A small-step approach to multi-trace checking against interactions

Logic in Computer Science 2020-09-29 v3 Formal Languages and Automata Theory

Abstract

Interaction models describe the exchange of messages between the different components of distributed systems. We have previously defined a small-step operational semantics for interaction models. The paper extends this work by presenting an approach for checking the validity of multi-traces against interaction models. A multi-trace is a collection of traces (sequences of emissions and receptions), each representing a local view of the same global execution of the distributed system. We have formally proven our approach, studied its complexity, and implemented it in a prototype tool. Finally, we discuss some observability issues when testing distributed systems via the analysis of multi-traces.

Keywords

Cite

@article{arxiv.2009.01777,
  title  = {A small-step approach to multi-trace checking against interactions},
  author = {Erwan Mahe and Boutheina Bannour and Christophe Gaston and Arnault Lapitre and Pascale Le Gall},
  journal= {arXiv preprint arXiv:2009.01777},
  year   = {2020}
}

Comments

long version - 26 pages (23 for paper, 2 for bibliography, and a 1 page annex) - 15 figures (1 in annex)

R2 v1 2026-06-23T18:17:58.125Z