modeling - 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?

question from:https://stackoverflow.com/questions/65884708/comparing-a-concrete-execution-trace-with-an-alloy-model

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 ... :-)