Advertisement

Analyzing concurrent systems using the Concurrency Workbench

  • Rance Cleaveland
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 693)

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.

Unable to display preview. Download preview PDF.

References

  1. 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. 2.
    Bertsekas, D. and Gallager, R. Data Networks. Prentice-Hall, Englewood Cliffs, 1987.Google Scholar
  3. 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. 4.
    Bruns, G. and Anderson, S. “The Formalisation and Analysis of a Communications Protocol.” Submitted for publication.Google Scholar
  5. 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. 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. 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. 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. 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. 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. 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. 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. 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. 14.
    DeNicola, R. and Hennessy, M.C.B. “Testing Equivalences for Processes.” Theoretical Computer Science, v. 34, pp. 83–133, 1983.Google Scholar
  15. 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. 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. 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. 18.
    Goyer, J.H. Communications Protocols for the B-HIVE Multicomputer. Master's Thesis, North Carolina State University, 1991.Google Scholar
  19. 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. 20.
    Hennessy, M.C.B. Algebraic Theory of Processes. MIT Press, Boston, 1988.Google Scholar
  21. 21.
    Hoare, C.A.R. Communicating Sequential Processes. Prentice-Hall, London, 1985.Google Scholar
  22. 22.
    Holzmann, G. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, 1991.Google Scholar
  23. 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. 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. 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. 26.
    Milner, R. Communication and Concurrency. Prentice Hall 1989.Google Scholar
  27. 27.
    Moller, F. “The Edinburgh Concurrency Workbench (Version 6.0).” Technical Note LFCS-TN-34, University of Edinburgh, 1991.Google Scholar
  28. 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. 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. 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. 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. 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

Authors and Affiliations

  • Rance Cleaveland
    • 1
  1. 1.Department of Computer ScienceNorth Carolina State UniversityRaleighUSA

Personalised recommendations