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

TL;DR

This paper introduces a formal, small-step method for verifying multi-traces against interaction models in distributed systems, with proofs, complexity analysis, and a prototype tool.

Contribution

It extends previous semantics to check multi-traces, providing a formal approach, complexity study, and implementation for distributed system testing.

Findings

Formal proof of the approach

Complexity analysis of multi-trace checking

Prototype tool implementation

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.