Interaction-based Offline Runtime Verification of Distributed Systems
Proceedings of the Fundamentals of Software Engineering Conference (FSEN)
by Erwan Mahe; Boutheina Bannour; Christophe Gaston; Arnault Lapitre (Université Paris-Saclay, CEA List), and Pascale Le Gall (Université Paris-Saclay, CentraleSupéle) 
Interactions are formal models describing asynchronous communications within a distributed system. They can be drawn in the fashion of sequence diagrams and associated with an operational semantics in the style of process algebras. In this paper, we propose an algorithm for offline runtime verification against interactions. Our algorithm deals with observability issues e.g. that some subsystems may not be observed or that some events may not be observed when the end of monitoring on different subsystems cannot be synchronized. We prove the algorithm’s correctness and assess the performance of an implementation