Comparing a concrete execution trace with an Alloy Model

Question

I'm using Alloy to model a system. I would like to check the implemented system matches the Alloy model by comparing log traces from a concrete execution of the actual system with the model.

The way I see this working is:

1. Add logs to the implemented system at points that correspond to the high level concepts modelled in Alloy, such as "Receptionist checks in guest G1"
2. Pre-process these into a form understood by Alloy
3. Give this to Alloy (or some other tool) and say 'Does this model admit this trace?' (this question)

This would be run over the operational logs of the system (or maybe subsets if performance is a problem) and continuously validate that the system was operating 'to spec'.

Is that possible / reasonable?

Answer 1

Possible yes.

Reasonable I'm not quite sure. To me, Alloy shine at finding unknown unknowns, i.e. pitfalls, in your specifications.

Once the specification is fool-proofed using Alloy analysis, I don't see the point of encumbering your program with unnecessary translations and analysis steps. It's not only error prone, but you might also find yourself limited with the scalability of the analyzer if the traces you want to validate are substantial... But again, it's doable. So if you want it, sure, do it ... :-)

Answer 2

I'm using Alloy to model a system. I would like to check the implemented system matches the Alloy model by comparing log traces from a concrete execution of the actual system with the model.

Yes, I think that is a bit of work but it should be doable. I would be very interested in getting this to work. I have been thinking about this for a long time.

Loïc argues correctly that Alloy shines in finding solutions but to keep this manageable, Alloy must keep the scope small. Although this is true, Alloy is also a specification language. The timing issue is only in finding a solution. However, the problem you sketch is different, you already have the solution in the log. Each event specifies a transition in the state.

If you're familiar with the Alloy Evaluator then you should be aware that once you have a solution, you can run any Alloy code on that instance. Inside Alloy, there is a full set of classes to simulate an instance and run Alloy code against it.

So I think you can start with an initial instance and use your log event to create a secondary instance and then use Alloy to verify this is a valid transition. This will be very fast and I do not see why this could not handle a very large number of objects. Surely thousands and with a bit of caching wizardry millions.

We are currently working hard on Alloy 6, which will be integrate Electrum, where we will have full temporal logic that will make the rules easier to express.

I've been looking for a customer for a long time that would like to develop the necessary code to bridge Alloy & the trenches. If this works as I think it can work, it would be very interesting for the software industry.