Getting it Right the First Time: An Introduction to Alloy Modeling
Most software flaws come from one of two places. When the code doesn’t match our expectations, it could be that the code is wrong. Most software correctness techniques - types, tests, etc - are used to check the code. But it could instead be that the code is correct and our expectations are wrong: there’s a fundamental error in our design. These errors, called specification errors, are some of the most subtle and dangerous bugs. They can span multiple independent programs, occur in convoluted race conditions, or depend on physical phenomena. Our regular tools simply can’t find them.
Instead, we can find them by designing better. By writing your blueprint in a specification language, you can directly test your conception of the system. Automatic tools, such as model checkers and SAT solvers, then explore the entire design space to see if it actually has the properties you want. And since it works on the design itself, we can fix issues before we’ve written a single line of code.
In this workshop, attendees will learn how the basics of one such specification language, called Alloy, and how to apply it to real-world business problems. We will cover everything from data modeling to microservice architectures. By the end of this class attendees should be able to write their own basic specs and use them to identify issues in their software designs.
Who should attend this masterclass: People interested in testing, design, or formal methods
Academic level: Intermediate / Advanced
What is the take away from this masterclass: Attendees will learn how to use Alloy, how to do formal specification, and how to find issues with systems before making them.
