The concurrency workbench: a semantics-based tool for the verification of concurrent systems

ABSTRACT

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.

REFERENCES

• 1: K. A. Bartlett , R. A. Scantlebury , P. T. Wilkinson, A note on reliable full-duplex transmission over half-duplex links, Communications of the ACM, v.12 n.5, p.260-261, May 1969 [doi>10.1145/362946.362970]
• 2: B. Bloom , S. Istrail , A. R. Meyer, Bisimulation can't be traced, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.229-239, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73580]
• 3: BOUDOL, G., DE SIMONE, R., AND VERGAMINI, n. Experiment with auto and autograph on a simple case sliding window protocol. INRIA Rep. 870, July 1988.
• 4: C~VLmLERI, J, AND WINS~L, G. CCS wlth priority choice. In Proceedings of the Slxth Annual Symposium on Logw zn Computer Science (Amsterdam, July 1991), Computer Society Press, Los Alamitos, pp. 246-255.
• 5: E. Clarke , D. Long , K. McMillan, Compositional model checking, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.353-362, June 1989, Pacific Grove, California, United States
• 6: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 7: R. Cleaveland, Tableau-based model checking in the propositional mu-calculus, Acta Informatica, v.27 n.9, p.725-747, Sep. 1990
• 8: CLEAVELAND, R. On automatically distinguishlng inequivalent processes. In Computer-Aided Ver~f~cation '90 (Plscataway, JuIy 1991), American Mathematical Society, pp. 463-477. American Mathematical Society, Providence, 1991.
• 9: R. Cleaveland , M. Hennessy, Testing equivalence as a bisimulation equivalence, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.11-23, February 1990, Grenoble, France
• 10: Rance Cleaveland , Matthew Hennessy, Priorities in process algebras, Information and Computation, v.87 n.1-2, p.58-77, July/August 1990 [doi>10.1016/0890-5401(90)90059-Q]
• 11: CLEAVELAND, R., PARROW, J., AND STEFFEN, B. The Concz~rrency Workbench: Operati~g Instructions. Tech. Note 10, Laboratory for Foundations of Computer Science, Univ of Edinburgh, Sept. 1988.
• 12: Rance Cleaveland , Joachim Parrow , Bernhard Steffen, A Semantics Based Verification Tool for Finite State Systems, Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX, p.287-302, June 06-09, 1989
• 13: R. Cleaveland , J. Parrow , B. Steffen, The concurrency workbench, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.24-37, February 1990, Grenoble, France
• 14: CLEAVELAND, R., AND STEFFEN, B. When is 'partial' adequate? A logic-based prooftechnique using partml specifications. In Proceedlngs of the Fifth Annual Symposium on Log~c ~n Computer Science (Philadelphm, June 1990), pp. 440 449. Computer Soclety Press, Los Alamitos, 1990.
• 15: Rance Cleaveland , Bernhard Steffen, A preorder for partial process specifications, Proceedings on Theories of concurrency : unification and extension: unification and extension, p.141-151, September 1990, Amsterdam, The Netherlands
• 16: Rance Cleaveland , Bernhard Steffen, Computing behavioural relations, logically, Proceedings of the 18th international colloquium on Automata, languages and programming, p.127-138, June 1991, Madrid, Spain
• 17: Rance Cleaveland , Bernhard Steffen, A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.48-58, July 01-04, 1991
• 18: CLEAVELAND, R., AND ZWARICO, A. A theory of testmg for rea! t/me. In ProceedznAEs of the Sixth Annual Symposium on Logl, c in Computer Science (Amsterdam, July 1991), pp. 110-119. Computer Society Press, Los Alamitos, 1991.
• 19: DENIcoL~, R., AND HENNESSY, M. C.B. Testing equivalence for processes Theor. Comput. Sci. 34, (1983~, 83-133.
• 20: EMERSON, E. A., AND LEt, C -L. Efficient model checking m ~ragments of the propos~tional Mu-calculus. In Proceed~n~s of the F~rst Annual Symposium on Log~c in Computer Science (Cambridge, June 1986), pp. 267-278. Computer Society Press, Washington, 1986.
• 21: ERNBERG, P., AND FREDLUND, L.-~. Identi~ying some bottlenecks of the concurrency workbench. Tech. Rep. T90002, Swedish Inst. of Computer Science, 1990.
• 22: FERNANDEZ, J.-C. Ald~baran: Une syst~me de v~rification par r~duction de processus commun~cants. Ph.D. Thesis, Universit~ de Grenoble, 1988.
• 23: Lars-åke Fredlund , Bengt Jonsson , Joachim Parrow, An implementation of a translational semantics for an imperative language, Proceedings on Theories of concurrency : unification and extension: unification and extension, p.246-262, September 1990, Amsterdam, The Netherlands
• 24: GLABBEEK, R. VAN, SMOLKA, S. A., STEFFEN, B., AND TOFTS, C. M.N. Reactive, generative, and stratified models of probabilistic processes. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (Philadelphia, June 1990), pp. 130-141. Computer Society Press, Los Alamitos, 1990.
• 25: GOYER, J.H. Communications protocols for the B-H1VE multicomputer. Master's Thesis, North Carolina State Univ., 1991.
• 26: Susanne Graf , Bernhard Steffen, Compositional Minimization of Finite State Systems, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.186-196, June 18-21, 1990
• 27: Jan Friso Groote , Frits Vaandrager, An efficient algorithm for branching bisimulation and stuttering equivalence, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.626-638, July 1990, Warwick University, England
• 28: HAR'EL, Z., AND KURSHAN, R. P. Software for analytical development of communications protocols. AT& T Tech. J. 69, i (Feb. 1990), 45-59.
• 29: Matthew Hennessy, Algebraic theory of processes, MIT Press, Cambridge, MA, 1988
• 30: HmLERSTR"M, M. Verif~cation of CCS-processes. M.Sc. Thesis, Computer Science Dept., Aalborg, Univ., 1987.
• 31: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 32: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 33: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 34: Claus Torp Jensen, The Concurrency Workbench with Priorities, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.147-157, July 01-04, 1991
• 35: B. Jonsson , A. H. Khan , J. Parrow, Implementing a model checking algorithm by adapting existing automated tools, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.179-188, February 1990, Grenoble, France
• 36: B. Jonsson , J. Parrow, Deciding bisimulation equivalences for a class of non-finite-state programs, Proceedings of the 6th Annual Symposium on Theoretical Aspects of Computer Science on STACS 89, p.421-433, February 1989, Paderborn, Germany
• 37: Paris C. Kanellakis , Scott A. Smolka, CCS expressions finite state processes, and three problems of equivalence, Information and Computation, v.86 n.1, p.43-68, May 1990 [doi>10.1016/0890-5401(90)90025-D]
• 38: Kim Guldstrand Larsen, Proof System for Hennessy-Milner Logic with Recursion, Proceedings of the 13th Colloquium on Trees in Algebra and Programming, p.215-230, March 21-24, 1988
• 39: L~s~N, K. G., AND THOMSEN, B. A modal process logic. In Proceedings ofthe Third Annual Symposium on Logic in Computer Science (Edinburgh, July 1988), pp. 203-210. Computer Society Press, Washington, 1988.
• 40: Kim G. Larsen , Arne Skou, Bisimulation through probabilistic testing, Information and Computation, v.94 n.1, p.1-28, Sept. 1991 [doi>10.1016/0890-5401(91)90030-6]
• 41: LEE, C.-H. Implementering av CCS med v~rde"verfdring. SICS Tech. Rep. 1989 (in Swedish).
• 42: Jawahar Malhotra , Robert M. Shapiro , Scott A. Smolka , Alessandro Giacalone, Winston: A Toll for Hierarchical Design and Simulation of Concurrent Systems, Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, p.140-152, July 06-08, 1988
• 43: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 44: Robert Paige , Robert E. Tarjan, Three partition refinement algorithms, SIAM Journal on Computing, v.16 n.6, p.973-989, December 1, 1987 [doi>10.1137/0216062]
• 45: Joachim Parrow, Submodule construction as equation solving in CCS, Theoretical Computer Science, v.68 n.2, p.175-202, Oct. 30, 1989 [doi>10.1016/0304-3975(89)90128-X]
• 46: PARROW, J. Verifying a CSMA/CD-Protocol with CCS. In Proceedings of the Eighth IFIP Symposium on Protocol Speciflcation, Testing, and Veriflcation (Atlantic City, June 1988), North Holland, Amsterdam, 1988. pp. 373-387.
• 47: Jean-Luc Richier , Carlos Rodriguez , Joseph Sifakis , Jacques Voiron, Verification in XESAR of the Sliding Window Protocol, Proceedings of the IFIP WG6.1 Seventh International Conference on Protocol Specification, Testing and Verification VII, p.235-248, May 05-08, 1987
• 48: Ro~, V., AND DE SIMON~, R. Auto/autograph. In Computer-Aided Vertftcation '90(Piscataway, July 1990), American Mathematical Society, Providence, 1991. pp. 477-491.
• 49: Scott A. Smolka , Bernhard Steffen, Priority as extremal probability, Proceedings on Theories of concurrency : unification and extension: unification and extension, p.456-466, September 1990, Amsterdam, The Netherlands
• 50: Bernhard Steffen, Characteristic Formulae, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.723-732, July 11-15, 1989
• 51: STEFFEN, B., AND INGOLFSDOTTIR, A. Characteristic formulae for CCS with divergence. To appear in Theor. Comput. Sci.
• 52: C. Stirling, Modal logics for communicating systems, Theoretical Computer Science, v.49 n.2-3, p.311-347, January 1987 [doi>10.1016/0304-3975(87)90012-0]
• 53: Colin Stirling , David Walker, Local Model Checking in the Modal Mu-Calculus, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 1: Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming, p.369-383, March 13-17, 1989
• 54: WALKER, D. J. Bisimulation equivalence and divergence in CCS. In Proceedings of the Thtrd Annual Symposium on Logic in Computer Sctence (Edinburgh. 1988), pp. 186-192. Computer Society Press, Washington, 1988.
• 55: D. J. Walker, Automated analysis of mutual exclusion algorithms using CCS, Formal Aspects of Computing, v.1 n.3, p.273-292, Jul./Sep. 1989 [doi>10.1007/BF01887209]
• 56: Glynn Winskel, On the compositional checking of validity (extended abstract), Proceedings on Theories of concurrency : unification and extension: unification and extension, p.481-501, September 1990, Amsterdam, The Netherlands

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Programmer workbench**
      D.2.4 Software/Program Verification

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

General Terms:
Design, Reliability, Verification

Keywords:
automatic verification, concurrency, finite-state systems, process algebra