Total-correctness refinement for sequential reactive systems

Abstract

We introduce a coinductively-defmed refinement relation on sequential non-deterministic reactive systems that guarantees total correctness. It allows the more refined system to both have less non-determinism in its outputs and to accept more inputs than the less refined system. Data reification in VDM is a special case of this refinement. Systems are considered at what we have called fine and medium levels of granularity. At the fine-grain level, a system's internal computational steps are described. The fine-grain level abstracts to a medium-grain level where only input/output and termination behaviour is described. The refinement relation applies to medium grain systems. The main technical result of the paper is the proof that refinement is respected by contexts constructed from fine grain systems. In other words, we show that refinement is a precongruence. The development has been mechanized in PVS to support its use in case studies.