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.
PDF | DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn