作者
Rance Cleaveland, Joachim Parrow, Bernhard Steffen
发表日期
1993/1/1
期刊
ACM Transactions on Programming Languages and Systems (TOPLAS)
卷号
15
期号
1
页码范围
36-72
出版商
ACM
简介
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.
引用总数
学术搜索中的文章
R Cleaveland, J Parrow, B Steffen - ACM Transactions on Programming Languages and …, 1993