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

[PVS-Help] access list question with pvs file



Hi,

 

I realize my attempt yesterday at asking my question didn’t have enough

information so I’m sending my pvs file with the question again.

 

I’m trying to construct a machine that keeps a running list of add requests

from arbitrary users modeled as nat IDs. When the machine encounters a

later  access request by that same ID, the access is allowed.  I’m trying

to prove that any given access allowed through to the machine output must

have been preceded by a previous [add ID] machine input, see theorem

 

add_access_order

 

in the attached pvs file.

 

I’m having a hard time trying to prove this.  Thank you for any help with the

proof or with any suggestion for a better model.

 

Long Duong, Ph.D

RedPhone Security

651.204.3372

 

Attachment: test.pvs
Description: Binary data