THE CONCURRENCY WORKBENCH - A SEMANTICS-BASED TOOL FOR THE VERIFICATION OF CONCURRENT SYSTEMS

被引：200

作者：

CLEAVELAND, R

PARROW, J

STEFFEN, B

机构：

[1] SWEDISH INST COMP SCI, S-16428 KISTA, SWEDEN

[2] RHEIN WESTFAL TH AACHEN, LEHRSTUHL INFORMAT 2, W-5100 AACHEN, GERMANY

[3] UNIV SUSSEX, DEPT COMP SCI, BRIGHTON BN1 9RH, E SUSSEX, ENGLAND

来源：

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 1993年 / 15卷 / 01期

关键词：

AUTOMATIC VERIFICATION; CONCURRENCY; FINITE-STATE SYSTEMS; CONCURRENCY WORKBENCH; PROCESS ALGEBRA;

D O I：

10.1145/151646.151648

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its breadth: a variety of different verification methods, including equivalence checking, preorder checking, and model checking, are supported for several different process semantics. One experience from our work is that a large number of interesting verification methods can be formulated as combinations of a small number of primitive algorithms. The Workbench has been applied to the verification of communications protocols and mutual exclusion algorithms and has proven a valuable aid in teaching and research.

引用

页码：36 / 72

页数：37

共 54 条

[1] A NOTE ON RELIABLE FULL-DUPLEX TRANSMISSION OVER HALF-DUPLEX LINLS [J].

BARTLETT, KA ;

SCANTLEBURY, RA ;

WILKINSON, PT ;

LYNCH, WC .

COMMUNICATIONS OF THE ACM, 1969, 12 (05) :260-+

[2]

BLOOM B, 1988, 15TH P ACM POPL, P229

[3]

BOUDOL G, 1988, INRIA870 REP

[4]

CAMILLERI J, 1991, SIXTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, P246

[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, 1991, 4TH P ANN S LOG COMP, P353

[7]

Cleaveland R., 1992, Computer Aided Verification. 3rd International Workshop CAV '91. Proceedings, P48

[8]

CLEAVELAND R, 1990, LECT NOTES COMPUT SC, V458, P141

[9]

Cleaveland R., 1990, Automatic Verification Methods for Finite State Systems. International Workshop Proceedings, P24

[10]

Cleaveland R., 1990, Automatic Verification Methods for Finite State Systems. International Workshop Proceedings, P11

← 1 2 3 4 5 6 →