Validating Traces of Distributed Programs Against TLA+ Specifications
arxiv(2024)
摘要
TLA+ is a formal language for specifying systems, including distributed
algorithms, that is supported by powerful verification tools. In this work we
present a framework for relating traces of distributed programs to high-level
specifications written inTLA+. The problem is reduced to a constrained model
checking problem, realized using the TLC model checker. Our framework consists
of an API for instrumenting Java programs in order to record traces of
executions, of a collection of TLA+ operators that are used for relating those
traces to specifications, and of scripts for running the model
checker.Crucially, traces only contain updates to specification variables
rather than full values, and it is not necessary to provide values for all
variables. We have applied our approach to several distributed programs,
detecting discrepancies between the specifications and the implementations in
all cases. We discuss reasons for these discrepancies, how to interpret the
verdict produced by TLC, and how to take into account the results of trace
validation for implementation development.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要