AN OLD-FASHIONED RECIPE FOR REAL-TIME

被引：95

作者：

ABADI, M

LAMPORT, L

机构：

[1] Digital Equipment Corp., Palo Alto, CA

来源：

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 1994年 / 16卷 / 05期

关键词：

COMPOSITION; CONCURRENT PROGRAMMING; LIVENESS PROPERTIES; REAL TIME; SAFETY PROPERTIES; TEMPORAL LOGIC; ZENO;

D O I：

10.1145/186025.186058

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Traditional methods for specifying and reasoning about concurrent systems work for rear-time systems. Using TLA (the temporal logic of actions), we illustrate how they work with the examples of a queue and of a mutual-exclusion protocol. In general, two problems must be addressed: avoiding the real-time programming version of Zeno's paradox, and coping with circularities when composing real-time assumption/guarantee specifications. Their solutions rest on properties of machine closure and realizability.

引用

页码：1543 / 1571

页数：29

共 19 条

[1] THE EXISTENCE OF REFINEMENT MAPPINGS [J].

ABADI, M ;

LAMPORT, L .

THEORETICAL COMPUTER SCIENCE, 1991, 82 (02) :253-284

[2] COMPOSING SPECIFICATIONS [J].

ABADI, M ;

LAMPORT, L .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1993, 15 (01) :73-132

[3]

ABADI M, 1992, 86 DIG EQ CORP SYST

[4] DEFINING LIVENESS [J].

ALPERN, B ;

SCHNEIDER, FB .

INFORMATION PROCESSING LETTERS, 1985, 21 (04) :181-185

[5] APPRAISING FAIRNESS IN LANGUAGES FOR DISTRIBUTED-PROGRAMMING [J].

APT, KR ;

FRANCEZ, N ;

KATZ, S .

DISTRIBUTED COMPUTING, 1988, 2 (04) :226-241

[6]

Bernstein A., 1981, Operating Systems Review, V15, P1, DOI 10.1145/1067627.806585

[7]

CHANDY KM, 1988, PARALLEL PROGRAM DES

[8]

DEBAKKER J, 1992, LECTURE NOTES COMPUT, V600

[9]

Dill David L., 1988, THESIS CARNEGIE MELL

[10]

FISCHER M, 1985, ARE YOU E MAIL MESSA, V18, P56

← 1 2 →