[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] simple state machine with access list



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




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



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