Efficient Interaction-Based Offline Runtime Verification of Distributed Systems with Lifeline Removal
arxiv(2024)
摘要
Runtime Verification (RV) refers to a family of techniques in which system
executions are observed and confronted to formal specifications, with the aim
of identifying faults. In Offline RV, observation is done in a first step and
verification in a second, on a static artifact collected during observation. In
this paper, we define an approach to offline RV of Distributed Systems (DS)
against interactions. Interactions are formal models describing communications
within a DS. DS are composed of subsystems deployed on different machines and
interacting via message passing. Therefore, observing executions of a DS
entails logging a collection of local execution traces, one for each subsystem,
that we call a multi-trace. A major challenge in analyzing multi-traces is that
there are no practical means to synchronize the ends of observations of all
local traces. We address this via an operation, called lifeline removal, which
we apply on-the-fly on the specification during verification once a local trace
has been entirely analyzed. This operation removes from the interaction the
specification of actions occurring on the subsystem that is no-longer observed.
This may allow further execution of the specification via removing deadlocks
due to the partial orders of actions. We prove the correctness of the resulting
RV algorithm and introduce two optimization techniques which we also prove
correct. We implement a Partial Order Reduction (POR) technique via the
selection of a one-unambiguous action (as a unique first step to a
linearization) which existence is determined via another use of the lifeline
removal operator. Additionally, Local Analyses (LOC) i.e., the verification of
local traces, can be leveraged during the global multi-trace analysis to prove
failure more quickly. Experiments illustrate the application of our RV approach
and the benefits of our optimizations.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要