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

[PVS-Help] simple state machine with access list



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