Would Alloy be the right tool?

I’m working on an application that includes a policy module that makes a decision based on a stream of events. Over time, it will received various notifications and make decisions, some of which are based on time elapsing–if I haven’t heard anything in 6 days after event X then do Y. Of course there could be multiple overlapping waiting periods with various obscure interactions, hence the interest in a bit of model-checking.

I’ve heard some say that this is not Alloy’s strong point, and that it’s better for flushing out structure.



I think it will likely depend on whether you want to explore subtle aspects of a conceptual design, for example exploring ways in which different kinds of notification patterns are formulated, or if instead you want to check simpler properties of a more concrete design. Alloy might be good for the former; for the latter, you probably want a model checker that handles timing (unless you can discretize it in a simple way).

Thanks for responding. I think in principle the timing issues could be modelled in Alloy as it’s just “logical” days, so perhaps as a sequence. The largest range will be about 15, so not a big deal. The main concern of the people implementing this is to catch obscure combinations that end badly, and cases that should never happen. There are likely to be enough installations to flush out whatever we haven’t caught (and, of course, if they’d thought of this a month ago it would be much easier…).