论文标题
针对互动的多条跟踪检查的小步骤方法
A small-step approach to multi-trace checking against interactions
论文作者
论文摘要
交互模型描述了分布式系统的不同组件之间的消息交换。我们以前已经为交互模型定义了小步操作语义。本文通过提出一种检查多轨相对于交互模型的有效性的方法来扩展这项工作。多迹线是迹线的集合（排放和接收的序列），每个迹线代表分布式系统的相同全局执行的局部视图。我们已经正式证明了我们的方法，研究了它的复杂性，并在原型工具中实现了它。最后，在通过多轨道分析测试分布式系统时，我们讨论了一些可观察性问题。
Interaction models describe the exchange of messages between the different components of distributed systems. We have previously defined a small-step operational semantics for interaction models. The paper extends this work by presenting an approach for checking the validity of multi-traces against interaction models. A multi-trace is a collection of traces (sequences of emissions and receptions), each representing a local view of the same global execution of the distributed system. We have formally proven our approach, studied its complexity, and implemented it in a prototype tool. Finally, we discuss some observability issues when testing distributed systems via the analysis of multi-traces.
