User Group Meeting

PVS Specification and Verification System

Dave Stringer-Calvert
Email: dave_sc@csl.sri.com

Refinement of state-based systems in PVS:
A uniform Approach based on Final Coalgebras

Harald Ruess
SRI International, Computer Science Laboratory, Menlo Park, CA, 94025
e-mail: ruess@csl.sri.com

We propose a formal model of non-deterministic transition systems based on coinductively defined sequences. Such a model describes both terminating and non-terminating systems in a uniform and, as we claim, natural way. The definition of a trace is based on the notion of "invariance" and we introduce the dual notion of "coinvariance" to formulate liveness properties. This approach does not only yield a certain "proof economy" but also enables us, for example, to generalize well-known techniques for proving termination (based on well-founded orderings) to establish liveness.

Next, we introduce a suitable notion of refinement: it requires that every trace of the concrete machine contains a subtrace which corresponds to some trace of the abstract machine. Moreover, our concept of refinement integrates a fairness condition in order to guarantee preservation of termination. This general concept of refinement is itself refined to 1) the usual one-to-one refinement, 2) transition refinement, which allows for "stuttering" steps of the concrete machine, and 3) a refinement notion on "visible" states. For each of these refinements we develop sufficient local criteria. The usefulness and practicality of our approach is demonstrated by refining a constrained shortest path problem to a variant of the algorithm of Moore and Ford.

All our developments have been formalized and proven using the PVS system.