The TLA+ Toolbox
Markus Alexander Kuppe (Microsoft Research), Leslie Lamport (Microsoft, Research), Daniel Ricketts (Oracle Corporation)
TL;DR
The paper presents the TLA+ Toolbox, a formal specification environment with novel cloud integration and profiling features aimed at industrial engineers, enhancing scalability and debugging capabilities.
Contribution
It introduces CloudTLC for cloud-based model checking and a Profiler for debugging, along with detailed architecture for community contribution and learning.
Findings
CloudTLC enables scalable model checking via cloud computing.
The Profiler assists in debugging and identifying state space issues.
The Toolbox's architecture supports community contributions.
Abstract
We discuss the workflows supported by the TLA+ Toolbox to write and verify specifications. We focus on features that are useful in industry because its users are primarily engineers. Two features are novel in the scope of formal IDEs: CloudTLC connects the Toolbox with cloud computing to scale up model checking. A Profiler helps to debug inefficient expressions and to pinpoint the source of state space explosion. For those who wish to contribute to the Toolbox or learn from its flaws, we present its technical architecture.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.