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

[PVS-Help] access list question with pvs file



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




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



Attachment: test.pvs
Description: Binary data