# Analyzing concurrent systems using the Concurrency Workbench

Chapter

First Online:

## Abstract

This paper presents a case study illustrating the different analytical facilities provided by the Concurency Workbench, an automatic verification tool for finite-state systems. The system we consider is the Alternating Bit Protocol, a communications protocol designed to ensure error-free data transfer over lossy media. Using the Workbench we investigate several features of the protocol, and we isolate a crucial property (the assumption of which is unstated in the protocol definition) that media must have in order for the protocol to be deadlock-free.

## Keywords

Model Checker Visible Action Process Algebra Concurrent System Automatic Verification
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

## Preview

Unable to display preview. Download preview PDF.

## References

- 1.Bartlett, K.A., Scantlebury, R.A., and Wilkinson, P.T. “A Note on Reliable Full-Duplex Transmission over Half-Duplex Links.”
*Communications of the ACM*12, n. 5, pp. 260–261, May 1969.Google Scholar - 2.Bertsekas, D. and Gallager, R.
*Data Networks*. Prentice-Hall, Englewood Cliffs, 1987.Google Scholar - 3.Brookes, S.D., Hoare, C.A.R., and Roscoe, A.W. “A Theory of Communicating Sequential Processes.”
*Journal of the ACM*, v. 31, n. 3, July 1984, pp. 560–599.Google Scholar - 4.Bruns, G. and Anderson, S. “The Formalisation and Analysis of a Communications Protocol.” Submitted for publication.Google Scholar
- 5.Celikkan, U. and Cleaveland, R. “On Computing Diagnostic Information for Preorder Checking.” To appear in
*Proceedings of the 1992 Workshop on Computer-Aided Verification*.*Lecture Notes in Computer Science*. Springer-Verlag, Berlin, 1993.Google Scholar - 6.Celikkan, U. and Cleaveland, R. “Computing Diagnostic Tests for Incorrect Processes.” With U. Celikkan. To appear in
*Proceedings of the Twelfth International Symposium on Protocol Specification, Testing and Verification*.Google Scholar - 7.Clarke, E.M., Emerson, E., and Sistla, A.P. “Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications.”
*A CM Transactions on Programming Languages and Systems*, v. 8, n. 2, pp. 244–263, 1986.Google Scholar - 8.Cleaveland, R. “On Automatically Distinguishing Inequivalent Processes.” In
*Computer-Aided Verification '90*, pp. 463–477. American Mathematical Society, Providence, 1991. Also Lecture Notes in Computer Science 531, Springer-Verlag, Berlin, 1991.Google Scholar - 9.Cleaveland, R., Parrow, J. and Steffen, B. “A Semantics-Based Tool for the Verification of Finite-State Systems.” In
*Proceedings of the Ninth IFIP Symposium on Protocol Specification, Testing and Verification*, June 1989, pp. 287–302. North-Holland, Amsterdam, 1990.Google Scholar - 10.Cleaveland, R., Parrow, J. and Steffen, B. “The Concurrency Workbench.” In
*Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems*, pp. 24–37. Lecture Notes in Computer Science 407, Springer-Verlag, Berlin, 1989.Google Scholar - 11.Cleaveland, R., Parrow, J. and Steffen, B. “The Concurrency Workbench: A Semantics-Based Tool for the Verification of Finite-State Systems.” Technical Report 91–26, North Carolina State University, 1991. To appear in
*ACM TOPLAS*.Google Scholar - 12.Cleaveland, R. and Steffen, B. “Computing Behavioural Relations, Logically.” In
*Proceedings International Colloquium on Automata, Languages and Programming*. Lecture Notes in Computer Science 510, Springer-Verlag, Berlin, 1991.Google Scholar - 13.Cleaveland, R. and Steffen, B. “A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus.” In
*Proceedings of Computer-Aided Verification '91*, Lecture Notes in Computer Science 575. Springer-Verlag, Berlin, 1992.Google Scholar - 14.DeNicola, R. and Hennessy, M.C.B. “Testing Equivalences for Processes.”
*Theoretical Computer Science*, v. 34, pp. 83–133, 1983.Google Scholar - 15.Fernandez, J.-C.
*Aldébaran: Une Système de Vérification par Réduction de Processus Communicants*. Ph.D. Thesis, Université de Grenoble, 1988.Google Scholar - 16.van Glabbeek, R. and Weijland, P. “Branching Time and Abstraction in Bisimulation Semantics.” In
*Information Processing 89*, pp. 613–618. North-Holland, Amsterdam, 1989.Google Scholar - 17.Godskesen, J.C., Larsen, K.G., and Zeeberg, M. “TAV—Tools for Automatic Verification.” Technical Report R89-19, Aalborg University, 1989.Google Scholar
- 18.Goyer, J.H.
*Communications Protocols for the B-HIVE Multicomputer*. Master's Thesis, North Carolina State University, 1991.Google Scholar - 19.Har'el, Z. and Kurshan, R.P. “Software for Analytical Development of Communications Protocols.”
*AT&T Technical Journal*, v. 69, n. 1, pp. 45–59. February, 1990.Google Scholar - 20.Hennessy, M.C.B.
*Algebraic Theory of Processes*. MIT Press, Boston, 1988.Google Scholar - 21.Hoare, C.A.R.
*Communicating Sequential Processes*. Prentice-Hall, London, 1985.Google Scholar - 22.Holzmann, G.
*Design and Validation of Computer Protocols*. Prentice-Hall, Englewood Cliffs, 1991.Google Scholar - 23.Larsen, K.G. “Proof Systems for Hennessy-Milner Logic with Recursion.” In
*Proceedings of CAAP*, Lecture Notes in Computer Science 299, Springer-Verlag, Berlin, 1988.Google Scholar - 24.Larsen, K.G. and Thomsen, B. “Compositional Proofs by Partial Specification of Processes.” Report R 87-20, University of Aalborg, July 1987.Google Scholar
- 25.Malhotra, J., Smolka, S.A., Giacalone, A. and Shapiro, R. “Winston: A Tool for Hierarchical Design and Simulation of Concurrent Systems.” In
*Proceedings of the Workshop on Specification and Verification of Concurrent Systems*, University of Stirling, Scotland, 1988.Google Scholar - 26.Milner, R.
*Communication and Concurrency*. Prentice Hall 1989.Google Scholar - 27.Moller, F. “The Edinburgh Concurrency Workbench (Version 6.0).” Technical Note LFCS-TN-34, University of Edinburgh, 1991.Google Scholar
- 28.Park, D.M.R. “Concurrency and Automata on Infinite Sequences.” In
*Proceedings of the 5*^{th}*GI Conference*, Lecture Notes in Computer Science 104. Springer-Verlag, Berlin, 1981.Google Scholar - 29.Parrow, J. “Verifying a CSMA/CD-Protocol with CCS.” In
*Proceeding of the Eighth IFIP Symposium on Protocol Specification, Testing, and Verification*, pp. 373–387. North-Holland, Amsterdam, 1988.Google Scholar - 30.Richier, J., Rodriguez, C., Sifakis, J., and Voiron, J., “Verification in XESAR of the Sliding Window Protocol.” In
*Proceedings of the Seventh IFIP Symposium on Protocol Specification, Testing, and Verification*. North-Holland, Amsterdam, 1987.Google Scholar - 31.Roy, V. and de Simone, R. “Auto/Autograph.” In
*Computer-Aided Verification '90*, pp. 477–491. American Mathematical Society, Providence, 1991.Google Scholar - 32.Walker, D.J. “Bisimulation Equivalence and Divergence in CCS.” In
*Proceedings of the Third Annual Symposium on Logic in Computer Science*, 1988, pp. 186–192. Computer Society Press, Los Alamitos, 1988.Google Scholar

## Copyright information

© Springer-Verlag Berlin Heidelberg 1993