|
Hi, I’ve recently started using PVS and am trying to solve
a simple access list construction inside a state machine. In
particular, I’m using a state machine which I got from this web page http://www.cs.ru.nl/~erikpoll/Teaching/PVS/machine.pvs with the internal state being a list which I model as a
sequence with a size field attached to it. What I’m trying to build
is a state machine that keeps a running list of all the input “add” requests
and later allow an “access” request if that same user ID exists as the [# ID, op := add
#] pair in the state list. I’m trying to prove in general that every input access
request which the machine will allow to pass through must have been preceded by an
earlier input add, but I’m finding it very hard to prove this in PVS. Thanks for your help, Long Duong, Ph.D RedPhone Security 651.204.3372 |