Return to site

Using TLA+ to Catch Bugs Before They Exist

Bugs in software are common, seemingly inevitable. But when software flies planes and drives cars, bugs are not just an inconvenience, they could actually put people’s lives in danger. In a high-stakes situation with no room for error, is there a way to bug-proof software before it’s implemented in the real world?

Code reviews are one way to find bugs, but they catch errors downstream, after the software has been written. Errors detected in a code review lead to patches and workarounds, which bulk up a program and introduce more complexity and, ironically enough, increased potential for error.

Want to catch bugs before they’re written into (digital) stone? A high-level language called TLA+ can help you model and verify the correctness of the software design, before you spend the money developing the actual software.

TLA+, which stands for Temporal Logic of Actions, is a formal specification that mandates what must go right with the software. TLA+ is not code, which is deliberate; but rather math-like, and it has a tool you could use during the planning phase to check your models and help you avoid the pitfalls of thinking only in your favorite programming language.

When using TLA+, serious effort must be put into design, modelling, and documentation. But all of that effort to model a system, especially a concurrent one, and to describe its behaviors pays off when you catch design flaws before having written a line of code.

Is your software development project a good candidate for using TLA+? Here are a few considerations to help you decide:

  • If the software malfunctions or does not work as anticipated, would it cause any harm or damage? A web application that manages a routine administrative operation probably would not generate serious consequences in the event things don’t always work as expected. However, any sort of software that moves or propels objects in the physical world certainly could.

  • How important is it that your software program be flawless? If it is going to be used as a pillar of your business, or the base upon which other applications are developed, then the time required to verify it with TLA+ can be considered a good investment. If the program is relatively independent and not going to be integrated or adopted by a variety of users, then perhaps such extensive verification is not as necessary.

  • Does your software require concurrent or distributed sub-systems? If so, it would be a good idea to take a serious look into TLA+ to help manage this complexity.

If you’ve got questions about using TLA+ or PlusCal on any of your projects, contact the computer scientists at XorFox for a free consultation!

All Posts

Almost done…

We just sent you an email. Please click the link in the email to confirm your subscription!