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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 3 articles , 1 standard article )

Showing results 1 to 3 of 3.
Sorted by year (citations)

  1. Katara, Mika; Katz, Shmuel: A concern architecture view for aspect-oriented software design (2007) ioport
  2. Kurki-Suonio, R.: Action systems in incremental and aspect-oriented modeling (2003)
  3. Kellomäki, Pertti: A structural embedding of Ocsid in PVS (2001)