Verifying Multiple TLA⁺ Configurations with Blast

TLA<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">+</sup> is one of the most popular formal methods for designing concurrent and distributed systems. TLA<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">+</sup> specifications can be verified with the TLC model checker, but unfortunately only one user-specified configuration of the system is verified at a time. If configurations are simple (e.g. the number of processes in a concurrent algorithm) it is viable to run TLC for several configurations to gain confidence that the system indeed works correctly for all of them. However, for complex configurations it is difficult to do so, and critical configurations can easily be missed. This paper introduces Blast, a tool that simplifies this task, by enabling the user to easily verify a TLA<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">+</sup> specification for all configurations inside a given scope. Our evaluation using a large benchmark of TLA<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">+</sup> examples, shows that Blast can be effectively used in a wide range of specifications and helped us uncover issues in several of them.