Introduction to Pragmatic Formal Modeling

submited by

Style Pass

2022-06-21 21:30:10

A formal model is a mathematical description of a system, generally to be implemented in hardware or software. They are useful for two reasons. Firstly, mathematics, unlike English, is precise and unambiguous. Even if this is where you stop, it forces you to understand the system you are describing. Secondly, mathematically based models can be checked. You can describe success criteria, and if they are violated you can see the exact series of steps that led to that. This is particularly useful for distributed systems, from multiple threads on a computer to thousands of computers in a cloud service.

When you think about formal modeling, it’s easy (and intimidating) to jump straight to the most complex use cases. Sure, those algorithm geniuses who design the fundamental algorithms of distributed systems might need it, but what about me? I care about the quality of my work. But I work in industry. Maybe I work in the cloud, coordinating microservices. Maybe I’m a game developer writing the next multiplayer networking library. Maybe I’m building a peer to peer file storage solution. Regardless, the question remains:

For every example on this site, we’re going to try to take a pragmatic approach that mirrors the engineering design lifecycle. We’ll start with UML diagrams and relatively precise descriptions, and then convert them into a formal specification language. Then we’ll see how we can check for design errors, and get concrete examples as to how they occur. Finally we will show how to use the detailed model errors to progressively refine your designs.