💾 Archived View for dcreager.net › papers › Cirstea2024.gmi captured on 2024-06-16 at 12:27:53. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2024-05-10)
-=-=-=-=-=-=-
Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, Stephan Merz. “Validating Traces of Distributed Programs Against TLA+ Specifications”. arXiv preprint.
CSP would be a good language for property tests
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.
Contains a very good Related Work section that I need to trawl for more references in this space.