How to use Alloy to find faults in software architecture

Question

I'm having lots of fun learning Alloy, and am excited to apply it to some software projects I am working on.

In the past, I've used lightweight formal methods informally, if it were, to write in first order logic some of the invariants that I expect the system to have. I've never used this to find defects, only to focus my design and testing on the properties that are critical.

I'd like to go beyond that now, and actually use Alloy to find faults in the architecture. How can I do this? The approach I've been taking is:

1. Strip the architecture down to some kernel (eg remove use sets instead of more complicated data structures, use sig instead of more detailed enumerations)
2. Codify an invariant as an assert
3. check and run

However, while learning alot about Alloy, this hasn't helped me improve my architecture. In the process of simplifying my model, it seems the invariants I encode are simplified accordingly, and naturally hold.

For example, there was a bug in the architecture which we encountered only through prototyping and testing. The bug had to do with assuming if we have n items in a sequence, we can break them up into groups of m and process each m-group sequentially. (n happens to be much larger than m.) The problem is of course that m doesn't necessarily divide n, and thus the last group may be too small. This is a design level defect completely expressible in logic, precisely the type of defect Alloy is designed for. Yet, my Alloy model didn't find it. It simply abstracted away the integer size (see advice given in Why does Alloy tell me that 3 >= 10? to avoid using numbers), partitioned n into disjoint groups, and ran beautifully.

In other words, it almost seems that to make sure your model includes enough detail to capture the defect, you almost need to know about the defect in advance.

How do you then use Alloy for reviewing software architectures?

PS I understand that there are many cases where you don't have this problem. For instance, when reviewing a spec for a distributed system, and wanting to show invariants. My challenge here is applying Alloy to help with implementation, not to review a protocol or spec or state machine or other logical construct.

Answer 1

Alloy is not best suited to reason about numbers, or strings. So , your model will often fail to detect faults related to the format of a given string or the value of a given integer fields.

Now, what Alloy is great for, is to reason about relations, and constraints over those relations. Checking assertion is one way of assuring yourself that a given property holds, so you are right, using solely this technique, you might have the feeling that you need to know about the defect in advance.

I thus prefer to this approach the use of the run command that simply give you a bunch of instances satisfying the constraints of your model. Here, you will check by yourself if the series of instances generated "make sense" in the context of what you are modelling. And you will probably witness that some of your constraints are too restrictive or not restrictive enough, thus allowing you to enhance your model.