I’m working on a message protocol between various participants and I’d like to check what happens when a message is dropped, first to show the failure and then to show I’ve fixed it. I believe I’d like to show this in an assertion, as a property of the system, rather than not finding an instance in a run.
I started by trying to show that the various messages line up in an exchange but the generated counterexample I get is to just stop after the first message, which is not very useful.
Suggestions, references to obvious materials, etc?
Thanks all
S
As your description remains a bit vague, it’s not easy to answer. Have you considered checking a liveness property on your protocol? For instance, you may check that every error will be recovered or that if there’s a point in time when errors don’t happen anymore, then your system will reach a desired state (and remain in it). HTH.
Thanks for responding. It’s a bit vague, because I’m not quite sure how to start. So, perhaps I could check that, eventually, every dropped message is associated with (followed by?) a successful message.
I’d suggest two things. First, brainstorm a set of properties that you expect the protocol to satisfy. These don’t need to comprise a complete specification, but they will likely be helpful in understanding what can go wrong. Second, make sure that your model of the protocol itself is loose enough to actually account for how the implementation may behave if messages are dropped etc. So make sure, for example, that the receiver of a message does not have any global knowledge of message order or something like that, which would not be available to it in an implementation.
Thanks. I already have some of this (avoiding global order), but working through the rest. My hope was that I would be able to write checks to produce counterexamples for protocol failures, but I’m struggling to make those non-trivial. More to do…