Ocsid

A structural embedding of Ocsid in PVS. We describe a structural embedding of the Ocsid specification language into the logic of the PVS theorem prover. A front end tool is used to manipulate the structural elements of the language, while the expression language is directly borrowed from the theorem prover. The structural embedding allows us to express and verify invariant properties of distributed systems in an abstract form. An invariant can be verified once, and reused multiple times by discharging a set of relatively simple proof obligations.