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 条

[31]

Hopcroft J. E., 1979, INTRO AUTOMATA THEOR

[32]

Jensen C. T., 1992, Computer Aided Verification. 3rd International Workshop CAV '91. Proceedings, P147

[33]

JONSSON B, 1989, LECT NOTES COMPUT SC, V349, P421

[34]

JONSSON B, 1990, LECT NOTES COMPUT SC, V407, P179

[35] CCS EXPRESSIONS, FINITE STATE PROCESSES, AND 3 PROBLEMS OF EQUIVALENCE [J].

KANELLAKIS, PC ;

SMOLKA, SA .

INFORMATION AND COMPUTATION, 1990, 86 (01) :43-68

[36] BISIMULATION THROUGH PROBABILISTIC TESTING [J].

LARSEN, KG ;

SKOU, A .

INFORMATION AND COMPUTATION, 1991, 94 (01) :1-28

[37]

LARSEN KG, 1988, LECT NOTES COMPUT SC, V299, P215

[38]

Larsen U, 1988, Eur J Popul, V3, P203, DOI 10.1109/LICS.1988.5119

[39]

LEE CH, SICS1989 TECH REP

[40]

MALHOTRA J, 1988, 1988 P WORKSH SPEC V, P140

← 1 2 3 4 5 6 →