Refinement of time

被引：14

作者：

Broy, M ^{[1
]}

机构：

[1] Tech Univ Munich, Inst Informat, D-80290 Munich, Germany

来源：

THEORETICAL COMPUTER SCIENCE | 2001年 / 253卷 / 01期

关键词：

real time; reactive systems; refinement;

D O I：

10.1016/S0304-3975(00)00087-6

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We discuss mathematical models of the timed behaviour of system components. We study reactive system components that relate input-to-output streams. We work out a hierarchy of timing concepts. We distinguish non-timed streams, discrete streams with discrete or with continuous rime, and dense streams with continuous rime. We introduce a notion of a timed system component and formulate requirements for the time flow. We show how to compose timed systems in a modular way. We demonstrate that the introduction of time into a system model as well as the change of the timing model during the system development process can be captured as classical refinement steps. (C) 2001 Elsevier Science B.V. All rights reserved.

引用

页码：3 / 26

页数：24

共 23 条

[11] JOSEPH M, 1992, LECT NOTES COMPUT SC, V600, P315, DOI 10.1007/BFb0031998
[12] KOPETZ H, 1992, INT CON DISTR COMP S, P460, DOI 10.1109/ICDCS.1992.235008
[13] LAMPORT L, 1981, LECTURE NOTES COMPUT, V131, P177
[14] Lynch N., 1996, Formal Aspects of Computing, V8, P499, DOI 10.1007/BF01211907
[15] Forward and backward simulations .2. Timing-based systems
Lynch, N
Vaandrager, F
[J]. INFORMATION AND COMPUTATION, 1996, 128 (01) : 1 - 25
[16] A PROOF OF THE KAHN PRINCIPLE FOR INPUT OUTPUT AUTOMATA
LYNCH, NA
STARK, EW
[J]. INFORMATION AND COMPUTATION, 1989, 82 (01) : 81 - 92
[17] LYNCH NA, 1987, P 6 ACM S PRINC DIST
[18] Melham Thomas F., 1993, HIGHER ORDER LOGIC H
[19] Muller O, 1997, LECT NOTES COMPUT SC, V1201, P273, DOI 10.1007/BFb0014732
[20] THE EXPRESSIVE POWER OF INDETERMINANT DATA-FLOW PRIMITIVES
PANANGADEN, P
SHANBHOGUE, V
[J]. INFORMATION AND COMPUTATION, 1992, 98 (01) : 99 - 131

← 1 2 3 →