针对交互模型的离线运行时验证工具化：使用参数化仿真识别切片行为
Tooling Offline Runtime Verification against Interaction Models : recognizing sliced behaviors using parameterized simulation
AI总结：
针对分布式系统中因缺少全局时钟和记录不同步导致的部分观测多轨迹问题，提出基于参数化仿真的算法，依据 Interactions 规范重构未观测行为并验证一致性。
摘要：
离线运行时验证涉及根据规范对系统执行进行静态分析。对于分布式系统，由于不存在全局时钟，通常无法以全局轨迹的形式刻画执行情况。为考虑这一点，我们将执行建模为称为多轨迹的局部轨迹集合，每个共享公共时钟的同地参与者组对应一条局部轨迹。由于难以同步局部轨迹记录的开始和结束，事件可能在其开始或结束处缺失。对运行时验证而言，考虑这种部分观测的多轨迹具有挑战性。为此，我们提出一种算法，根据称为 Interactions（交互，类似于消息序列图）的形式化规范验证此类轨迹的一致性。该算法依赖参数化仿真来重构未观测到的行为。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
