[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
I am attempting to verify a protocol involving a few interacting
processes. I have been looking at the FORTE tutorial, which has been
very helpful, but I was wondering if anyone could help with some
I am trying to verify some timing properties of this protocol.
The protocol has a number of different, interacting processes. Each
of the processes is effectively a timed DFA. So, for example, when
process 1 is in state 1, it will run for up to t_1, and then make a
transition to state 2.
Now, in order to correctly come up with a transition model for the
overall protocol, we need to model interactions between the different
processes' timings. So, it is not enough to specify the transition
relation in the same style as the cache spec in the FORTE tutorial.
Return to my process 1. A naive formulation of the next_state
relation would be something like this:
p_next(s0, s1) : bool =
( process1_state(state1) = state1 AND
s1 = s0 WITH [process1_state := state2,
elapsed_time := elapsed_time(s0) + t_1])
This is not correct, because it is only valid to update the state this
way if t_1 is less than the time it takes for any of the other
processes to make a state transition.
So, my question is, has anyone developed this kind of specification?
Any suggestions for me?
My tentative thought is to have a clock for each individual process,
and increment them in lockstep. I.e., whenever you increase the
elapsed_time by some delta, all the individual clocks go up by delta;
clocks get reset to zero when a transition is followed. Then I would
write a transition relationship that contains a check for validity.
The check for validity would be of the form:
FORALL p in processes if state(p) = s then clock(p) < transtime(p, s)
I think that the formalization discussed in N. Shankar's paper
"Machine Assisted Verification Using..." might be a good first step
towards doing what I want. Would it be possible for me to get the
theories from that paper?