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

TL;DR

The paper tackles offline runtime verification for distributed systems lacking a global clock by modeling executions as generalized multi-traces and leveraging parameterized simulation to fill in unobserved behavior against a formal Interactions language. It introduces co-localizations and a new coreg_r operator to express concurrent regions, along with a refined operational semantics, enabling robust analysis of partially observed traces. A bounded-simulation ORV algorithm operating on a finite analysis graph can determine slice conformance to an interaction, with the HIBOU toolkit providing encoding, exploration, and analysis capabilities. Experiments show that the approach can identify many slices and illustrate trade-offs between completeness and termination under partial observation, with limitations acknowledged where more extensive simulation would be needed. The work advances practical ORV for distributed systems by enabling non-synchronizing observation architectures and by delivering a tangible tool for design-time verification and debugging.

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. To account for this, we model executions as collections of local traces called multi-traces, with one local trace per group of co-localized actors that share a common clock. Due to the difficulty of synchronizing the start and end of the recordings of local traces, events may be missing at their beginning or end. Considering such partially observed multi-traces is challenging for runtime verification. To that end, we propose an algorithm that verifies the conformity of such traces against formal specifications called Interactions (akin to Message Sequence Charts). It relies on parameterized simulation to reconstitute unobserved behaviors.

Figures (19)

• Figure 1: Trace collection
• Figure 2: An example of an interaction
• Figure 3: Pruning an interaction
• Figure 4: Follow-ups of the interaction from Fig.\ref{['fig:interaction_example']}
• Figure 5: Illustrating multi-trace analysis algorithm adapted (to co-localizations) from a_small_step_approach_to_multi_trace_checking_against_interactions.

Theorems & Definitions (43)

• Definition 1: Multi-traces
• Definition 2: Slices
• Definition 3
• Definition 4: Pruning
• Definition 5: Execution
• Definition 6
• Theorem 1
• proof
• Theorem 2
• proof