Designing Software with Complex Configurations

TL;DR

The paper investigates how lightweight formal methods can be applied to software with complex configurations, using the Echo distributed protocol as a running example. It compares $TLA^+$ and Alloy (including Alloy~6) as complementary approaches: $TLA^+$ provides explicit transition-system modeling and strong invariants via the TLC model-checker, while Alloy~6 offers symbolic, relational modeling and rich scenario exploration for large configuration spaces. The findings show that $TLA^+$ scales poorly across many configurations but excels for simple, clearly defined setups, whereas Alloy~6 handles complex configurations more effectively through symbolic back-ends, at the cost of slower liveness verification in some cases. Collectively, these lightweight formal methods enable cost-effective, early validation of software designs beyond traditional testing, with practical applicability to real-world, configuration-rich systems.

Abstract

In this paper I discuss how can lightweight formal methods be used to specify and verify software with complex configurations (for example, distributed protocols that work on specific network configurations). More specifically, I briefly present two popular formal methods - TLA+ and Alloy - and discuss the pros and cons of both in this particular context.

Figures (5)

• Figure 1: Minimal run in a complete network with 4 nodes
• Figure 2: Buggy configuration
• Figure 3: Relational logic
• Figure 4: Example network configurations
• Figure 5: Interactive scenario exploration