© 2019 Strange Loop
What if you could find complex bugs in systems without ever having looked at any of the code, without running the code, without cloning the code, or even knowing what language the code is written in or where its git repo lives? What if you could validate the correctness of an architectural proposal before writing code?
While this might sound impossible, it's in fact quite doable, and happening every day!
Tools called "model checkers" can be used to model and analyze the architecture/design of a system. Model checkers can simulate every possible sequence of operations your system might ever encounter, and check if desired properties always hold. And if a property doesn't hold, the model checker will show you an exact sequences of operations that violates it.
Benefit can be had both in the early design stages of a project, or if you're a newcomer trying to get up-to-speed on an existing system. Examples of both will be shown.
This talk will describe the model checker Alloy (http://alloytools.org). I'll show how we used it to invalidate a large amount of work by one group (before multiple teams started to try integrating with that work). I'll also show how we employed it to find a highly subtle security flaw in another group's project, without ever looking at a single line of code from either group. In both cases, we did this simply by talking to teams about the architecture of their systems, and translating those designs into formal specifications.