Advertisement

Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock

  • A. W. Roscoe
  • P. H. B. Gardiner
  • M. H. Goldsmith
  • J. R. Hulance
  • D. M. Jackson
  • J. B. Scattergood
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1019)

Abstract

We have given details of how FDR2's compression works, and some simple examples of how it can expand the size of problem we can automatically check. At the time of writing we have not had time to carry out many evaluations of this new functionality on realistic-sized examples, but we have no reason to doubt that compression will allow comparable improvements in these.

It is problematic that the successful use of compression apparently takes somewhat more skill than explicit model-checking. Only by studying its use in large-scale case studies can we expect to assess the best ways to deal with this — by automated tactics and transformation, or by design-rule guidance to the user. In any case much work will be required before we can claim to understand fully the capabilities and power of the extended tool.

Keywords

Normal Form Transition System Operational Semantic Visible Action Label Transition System 
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.

References

  1. [1]
    S.D. Brookes and A.W. Roscoe, An improved failures model for communicating processes, in Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985), 281–305.Google Scholar
  2. [2]
    J.R. Burch, E.M. Clarke, D.L. Dill and L.J. Hwang, Symbolic model checking: 1020 states and beyond, Proc. 5th IEEE Annual Symposium on Logic in Computer Science, IEEE Press (1990).Google Scholar
  3. [3]
    E.M. Clarke, D.E. Long and K.L.MacMillan, Compositional Model Checker, Proceedings of LICS 1989.Google Scholar
  4. [4]
    R. Cleaveland and M.C.B. Hennessy, Testing Equivalence as a Bisimulation Equivalence, FAC 5 (1993) pp 1–20.Google Scholar
  5. [5]
    R. Cleaveland, J. Parrow and B. Steffen, The Concurrency Workbench: A semantics-based verification tool for finite state systems, ACM TOPLAS Vol. 15, N. 1, 1993, pp. 36–72.Google Scholar
  6. [6]
    Formal Systems (Europe) Ltd., Failures Divergence Refinement User Manual and Tutorial, version 1.4 1994.Google Scholar
  7. [7]
    J.-C. Fernandez An implementation of an efficient algorithm for bisimulation equivalence., Science of Computer Programming 13: 219–236, 1989/1990.Google Scholar
  8. [8]
    S.Graf and B. Steffen, Compositional Minimisation of Finite-State Systems, Proceedings of CAV1990 (LNCS 531).Google Scholar
  9. [9]
    J.F. Groote and F. Vaandrager, An efficient algorithm for branching bisimulation and stuttering equivalence, Proc. 17th ICALP, Springer-Verlag LNCS 443, 1990.Google Scholar
  10. [10]
    C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall 1985.Google Scholar
  11. [11]
    L. Jategoankar, A Meyer and A.W. Roscoe, Separating failures from divergence, in preparation.Google Scholar
  12. [12]
    R. Kaivola and A Valmari The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic in Proc CONCUR. '92 (LNCS 630).Google Scholar
  13. [13]
    P.C. Kanellakis and S.A. Smolka, CCS expressions, Finite state processes and three problems of equivalence, Information and Computation 86, 43–68 (1990).Google Scholar
  14. [14]
    K.L. McMillan, Symbolic Model Checking, Kluwer, 1993.Google Scholar
  15. [15]
    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
  16. [16]
    K. Melhorn Graph Algorithms and NP Completeness, EATCS Monographs on Theoretical Computer Science, Springer-Verlag 1984.Google Scholar
  17. [17]
    J. Richier, C. Rodriguez, J. Sifakis and J. Voiron, Verification in XE-SAR of the Sliding Window Protocol, Proc. of the 7th IFIP Symposium on Protocol Specification, Testing, and Verification, North-Holland, Amsterdam, 1987.Google Scholar
  18. [18]
    A.W. Roscoe, Unbounded Nondeterminism in CSP, in ‘Two Papers on CSP', PRG Monograph PRG-67. Also Journal of Logic and Computation 3, 2 pp. 131–172 (1993).Google Scholar
  19. [19]
    A.W. Roscoe, Model-checking CSP, in A Classical Mind: Essays in Honour of C.A.R. Hoare, A.W. Roscoe (ed.) Prentice-Hall 1994.Google Scholar
  20. [20]
    A.W. Roscoe, CSP and determinism in security modelling to ap pear in the proceedings of 1995 IEEE Symposium on Security and Privacy.Google Scholar
  21. [21]
    A.W. Roscoe, Modelling and verifying key-exchange protocols using CSP and FDR, to appear in the proceedings of CSFW8 (1995), IEEE Press.Google Scholar
  22. [22]
    A.W. Roscoe, J.C.P. Woodcock and L. Wulf, Non-interference t hrough determinism, Proc. ESORICS 94, Springer LNCS 875, pp 33–53.Google Scholar
  23. [23]
    V. Roy and R. de Simone, Auto/Autograph, In Proc. Computer-Aided Verification '90, American Mathematical Society, Providence, 1991.Google Scholar
  24. [24]
    J.B. Scattergood, A basis for CSP tools, To appear as Oxford University Computing Laboratory technical monograph, 1993.Google Scholar
  25. [25]
    A. Valmari and M. Tienari An improved failures equivalence for finitestate systems with a reduction algorithm, in Protocol Specification, Testing and Verification XI, North-Holland 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • A. W. Roscoe
    • 1
    • 2
  • P. H. B. Gardiner
    • 2
  • M. H. Goldsmith
    • 2
  • J. R. Hulance
    • 2
  • D. M. Jackson
    • 2
  • J. B. Scattergood
    • 1
    • 2
  1. 1.Oxford University Computing LaboratoryOxford
  2. 2.Formal Systems (Europe) LtdOxford

Personalised recommendations