VERIFICATION OF THE FUTUREBUS+ CACHE COHERENCE PROTOCOL

被引：42

作者：

CLARKE, EM

GRUMBERG, O

HIRAISHI, H

JHA, S

LONG, DE

MCMILLAN, KL

NESS, LA

机构：

[1] CARNEGIE MELLON UNIV,SCH COMP SCI,PITTSBURGH,PA 15213

[2] TECHNION ISRAEL INST TECHNOL,DEPT COMP SCI,IL-32000 HAIFA,ISRAEL

[3] KYOTO SANGYO UNIV,DEPT INFORMAT & COMMUN SCI,KYOTO 603,JAPAN

[4] BELLCORE,MORRISTOWN,NJ 07962

来源：

FORMAL METHODS IN SYSTEM DESIGN | 1995年 / 6卷 / 02期

基金：

美国国家科学基金会;

关键词：

THE COMPUTER INDUSTRY; STANDARDS; FUTUREBUS+; MULTIPLE DATA STREAM ARCHITECTURES; INTERCONNECTION ARCHITECTURES; NETWORK PROTOCOLS; PROTOCOL VERIFICATION;

D O I：

10.1007/BF01383968

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We used a hardware description language to construct a formal model of the cache coherence protocol described in the IEEE Futurebus+ standard. By applying temporal logic model checking techniques, we found errors in the standard. The result of our project is a concise, comprehensible and unambiguous model of the protocol that should be useful both to the Futurebus+ Working Group members, who are responsible for the protocol, and to actual designers of Futurebus+ boards.

引用

页码：217 / 232

页数：16

共 13 条

[1]

BRYANT RE, 1986, IEEE T COMPUTERS, V35

[2]

BURCH JR, 1990, 5TH P ANN S LOG COMP

[3]

BURCH JR, 1990, 27TH P ACM IEEE DES

[4]

BURCH JR, 1991, 28TH P ACM IEEE DES

[5] AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].

CLARKE, EM ;

EMERSON, EA ;

SISTLA, AP .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02) :244-263

[6]

CLARKE EM, 1981, LECTURE NOTES COMPUT, V131

[7]

DIXON P, 1988, DEC FUT WORK GROUP M

[8]

LONG D, 1993, THESIS CARNEGIE MELL

[9]

McMillan K., 1992, SYMBOLIC MODEL CHECK

[10]

MCMILLAN KL, 1991, 1991 P INT S SHAR ME

← 1 2 →