Formally Modelling Database Migrations

Most of my formal methods examples deal with concurrency, because time is evil and I hate it. While FM is very effective for that, it gives people a limited sense of how flexible these tools are. Instead of a distributed system, we’re going to do something different. Lots of business apps store their conceptual model…

Compositional Network Mobility

Mobility is a network capability with many forms and many uses. Because it is difficult to implement at Internet scale, there is a large and confusing landscape of mobility proposals which cannot easily be compared or composed. This paper presents formal models of two distinct patterns for implementing mobility, explaining their generality and applicability. We…

A practical comparison of Alloy and Spin

Because potential users have to choose a formal method before they can start using one, research on assessing the applicability of specific formal methods might be as effective in encouraging their use as work on the methods themselves. This comparison of Alloy and Spin is based on a demanding project that exploited the full capabilities…

State machines with Alloy

This post continues the quest to get Java developers using Alloy, a tool that, in the right hands, is a fantastic way to explore software and hardware designs. Today we will explore a state machine. I ran into a state machine problem at a customer and used Alloy to debug it before I committed it…