Tooling Offline Runtime Verification against Interaction Models: recognizing sliced behaviors using parameterized simulation

By: Erwan Mahe, Boutheina Bannour, Christophe Gaston, Arnault Lapitre, Pascale Le Gall

Abstract

Offline runtime verification involves the static analysis of executions of a system against a specification. For distributed systems, it is generally not possible to characterize executions in the form of global traces given the absence of a global clock. This paper introduces an algorithm that verifies the conformity of partially observed multi-traces against formal specifications called Interactions, akin to Message Sequence Charts. It relies on parameterized simulation to reconstitute unobserved behaviors, addressing the challenge of analyzing distributed systems' executions under partial observation conditions.

Keywords

interaction simulation, co-localization, shared clock, partial observation, multi-trace, slice

Cite as:

Erwan Mahe, Boutheina Bannour, Christophe Gaston, Arnault Lapitre, Pascale Le Gall, “Tooling Offline Runtime Verification against Interaction Models: recognizing sliced behaviors using parameterized simulation”, Journal of Object Technology, Volume 23, no. 2 (March 2024), pp. 2:1-16, doi:10.5381/jot.2024.23.2.a2.