Technical Report
Refinement Principles Supporting the Transition from Asynchronous to Synchronous Communication
Author(s): Ketil Stølen
Year: 1995
Number: TUM-I9537
Editor:
CR Classification:
CR General Terms:
Keywords:
Abstract:We present three refinement principles supporting the transition from system specifications based on (unbounded) asynchronus communication to system specifications based on (bounded) synchronous communication. We refer to these principles as partial, total and conditional refinement, respectively. We distinguish between two synchronization techniques, namely synchronization by hand-shake and synchronization by real-time constraints. Partial refinement supports synchronization by hand-shake with respect to safety properties. Total refinement supports synchronization by hand-shake with respect to both safety and liveness properties. Finally, conditional refinement supports both synchronization by hand-shake and by real-time constraints. We discuss, relate and show the use of these principles in a number of small examples.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@techreport{ TUM-I9537,
author = {Ketil St\olen},
title = {Refinement Principles Supporting the Transition from Asynchronous to Synchronous Communication},
number = {TUM-I9537},
institution = {Technische Univerit\"at M\"unchen},
year = {1995},
url = {http://www4.informatik.tu-muenchen.de/reports/TUM-I9537.html},
abstract = {We present three refinement principles supporting the transition from system specifications based on (unbounded) asynchronus communication to system specifications based on (bounded) synchronous communication. We refer to these principles as partial, total and conditional refinement, respectively. We distinguish between two synchronization techniques, namely synchronization by hand-shake and synchronization by real-time constraints. Partial refinement supports synchronization by hand-shake with respect to safety properties. Total refinement supports synchronization by hand-shake with respect to both safety and liveness properties. Finally, conditional refinement supports both synchronization by hand-shake and by real-time constraints. We discuss, relate and show the use of these principles in a number of small examples. },
CRClassification = {},
CRGenTerms = {}
}
]]>