Total-Correctness Refinement for Sequential Reactive Systems

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

We introduce a coinductively-defined 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.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication13th International Conference, TPHOLs 2000 Portland, OR, USA, August 14–18, 2000 Proceedings
EditorsMark Aagaard, John Harrison
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Pages320-337
Number of pages18
ISBN (Electronic)978-3-540-44659-0
ISBN (Print)978-3-540-67863-2
DOIs
Publication statusPublished - 2000

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume1869
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Total-Correctness Refinement for Sequential Reactive Systems'. Together they form a unique fingerprint.

Cite this