I've been wanting to learn TLA+ for a while now, and I finally had a chance to do it thanks to a seminar series held by Professor Murat Demirbas. In this article, I will talk about my experience with formal methods and TLA+, and I will also share some of the things I've learnt that I think will be very useful when writing your specifications.
By the end of this article, I hope that you will:
Have a basic understanding of formal methods and model checking
Understand how TLA+ can improve algorithm and system design
Have some intuition on what it takes to write a spec in TLA+
Want to learn some TLA+.
As always, let's start with the problem we're trying to solve.
What problem do formal methods help solve?
English is considered a very ambiguous language. When we build a complex system, we need an unambiguous specification (also known as "spec"). Formal methods use math to define a rigorous system model. After we have written the code for the model, we can then also use it to verify some properties.
The benefits of formal methods are twofold:
Unambiguous specification of our systems and algorithms
Verification of properties for these models
An example of a property that can be verified is that no execution can result in a deadlock. This would be very difficult to prove in a test, especially if it spans multiple systems.
We can also verify that an algorithm is correct by writing some properties as invariants. An invariant is simply a predicate that should always hold true. Invariants are sometimes used in asserts.
We can define correctness and liveness properties. For example, we could verify that eventually some property will hold, such as that our new sorting algorithm eventually sorts its input.
Formal methods allow you to explore different designs and optimize performance while maintaining confidence that the system is doing the right thing.
Top comments (0)