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.
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 language | English |
---|---|
Title of host publication | Theorem Proving in Higher Order Logics |
Subtitle of host publication | 13th International Conference, TPHOLs 2000 Portland, OR, USA, August 14–18, 2000 Proceedings |
Editors | Mark Aagaard, John Harrison |
Place of Publication | Berlin, Heidelberg |
Publisher | Springer |
Pages | 320-337 |
Number of pages | 18 |
ISBN (Electronic) | 978-3-540-44659-0 |
ISBN (Print) | 978-3-540-67863-2 |
DOIs | |
Publication status | Published - 2000 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Berlin Heidelberg |
Volume | 1869 |
ISSN (Print) | 0302-9743 |