Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Generating diagnostic information for behavioral preorders

Summary

This paper describes a method for generating diagnostic information that explains why a given finite-state system fails to be greater than its specification with respect to the prebisimulation preorder. The information takes the form of a logical formula satisfied by the specification but not by the system and thus may be used by system designers for debugging purposes. Our technique relies on modifying an algorithm for computing the prebisimulation preorder so that information needed for generating these distinguishing formulas is saved appropriately. As a number of other behavioral preorders may be characterized in terms of prebisimulation preorder, our approach may be used as a basis for computing diagnostic information for these relations as well.

This is a preview of subscription content, log in to check access.

References

  1. 1.

    Fifth Annual Symposium on Logic in Computer Science (LICS’90), Philadelphia, June 1990. IEEE Computer Society Press

  2. 2.

    Abramsky S: Observation equivalence as a testing equivalence. Theor Comput Sci 53: 225–241 (1987)

  3. 3.

    Back RJR: Refinement calculus. Part 2: parallel and reactive programs. In: Stepwise refinement of distributed systems. Lect Notes Comput Sci, vol 430. REX Workshop, Mook, The Netherlands, June 1989. Springer, Berlin Heidelberg New York, pp 67–93, 1989

  4. 4.

    Back RJR, Sere K: Stepwise refinement of action systems. In: Mathematics of program construction. Lect Notes Comput Sci, vol 575. Gronningen, The Netherlands, June 1989. Springer, Berlin Heidelberg New York, pp 115–138, 1989

  5. 5.

    Baeten JCM, Weijland WP: Process algebra. Cambridge Tracts in Theoretical Computer Science, vol 18. Cambridge University Press, Cambridge, England, 1990

  6. 6.

    Bergstra JA, Klop JW: Algebra of communicating processes with abstraction. Theoretical Comput Sci 37: 77–121 (1985)

  7. 7.

    Bloom B, Paige R: Computing ready simulations efficiently. In: Proceedings of the North American Process Algebra Workshop, Workshops in Computing. Stony Brook, New York, August 1992. Springer, Berlin Heidelberg New York, pp 119–134, 1992

  8. 8.

    Bolognesi T, Brinksma E: Introduction to the ISO specification language LOTOS. Comput Networks ISDN Syst 14: 25–59 (1987)

  9. 9.

    Brookes SD, Hoare CAR, Roscoe AW: A theory of communicating sequential processes. J Assoc Comput Machinery 31(3): 560–599 (1984)

  10. 10.

    Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ: Symbolic model checking: 1020 states and beyond. In: Fifth Annual Symposium on Logic in Computer Science (LICS ’90) [1], pp 428–439

  11. 11.

    Celikkan U, Cleaveland R: Computing diagnostic tests for incorrect processes. In: Proceedings of the IFIP Symposium on Protocol Specification, Testing and Verification. Lake Buena Vista, Florida, June 1992. North-Holland, pp 263–278, 1992

  12. 12.

    Cleaveland R: On automatically explaining bisimulation inequivalence. In: Clarke EM, Kurshan RP (eds) Computer aided verification (CAV’90). Lect Notes Comput Sci, vol 531. Piscataway, NJ, June 1990. Springer, Berlin Heidelberg New York, pp 364–372, 1990

  13. 13.

    Cleaveland R, Hennessy MCB: Testing equivalence as a bisimulation equivalence. Formal Asp Comput 5: 1–20 (1993)

  14. 14.

    Cleaveland R, Parrow J, Steffen B: The concurrency workbench: a semantics based tool for the verification of finite-state systems. ACM Trans Program Lang Syst 15(1): 36–72 (1993)

  15. 15.

    Cleaveland R, Steffen B: When is ‘partial’ adequate? A logic-based proof technique using partial specifications. In: Fifth Annual Symposium on Logic in Computer Science (LICS ’90) [I], pp 440–449

  16. 16.

    Cleaveland R, Steffen B: Computing behavioural relations, logically. In: Leach Albert J, Monien B, Rodriguez Artalejo M (eds) Automat, Languages and Programming (ICALP ’91). Lect notes Comput Sci, vol 510. Madrid, July 1991. Springer, Berlin Heidelberg New York, pp 127–138, 1991

  17. 17.

    Cleaveland R, Steffen B: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods Syst Design 2: 121–147 (1993)

  18. 18.

    De Nicola R, Hennessy MCB: Testing equivalences for processes. Theor Comput Sci 34: 83–133 (1983)

  19. 19.

    Hennessy MCB: Algebraic theory of processes. MIT Press, Boston, 1988

  20. 20.

    Hennessy MCB, Milner R: Algebraic laws for nondeterminism and concurrency. J Assoc Comput Machinery 32(1): 137–161 (1985)

  21. 21.

    Hoare CAR: Communicating sequential processes. Prentice- Hall, London, 1985

  22. 22.

    Korver H: Computing distinguishing formulas for branching bisimulation. In: Larsen KG, Skou A (eds) Computer aided verification (CAV ’91). Lect Notes Comput Sci, vol 575. Aalborg, Denmark, July 1991. Springer, Berlin Heidelberg New York, pp 13–23, 1991

  23. 23.

    Larsen KG, Godskesen JC, Zeeberg M: TAV - tools for automatic verification. Tech Rep R 89-19. Aalborg University, Aalborg, Denmark, 1989

  24. 24.

    Larsen KG, Thomsen B: Compositional proofs by partial specification of processes. Tech Rep R 87-20. Aalborg University, Aalborg, Denmark, July 1987

  25. 25.

    Larsen KG, Thomsen B: A modal process logic. In: Third Annual Symposium on Logic in Computer Science (LICS ’88) Edinburgh, Scotland, July 1988. IEEE Computer Society Press, pp 203–210, 1988

  26. 26.

    Milner R: Communication and concurrency. Prentice-Hall, London, 1989

  27. 27.

    Stirling C: Modal logics for communicating systems. Theor Comput Sci 49: 311–347(1987)

  28. 28.

    Walker DJ: Bisimulation and divergence in CCS. In: Third Annual Symposium on Logic in Computer Science. Edinburgh, Scotland, July 1988. IEEE Computer Society Press, pp 186–192, 1988

Download references

Author information

Correspondence to Ufuk Celikkan or Rance Cleaveland.

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Celikkan, U., Cleaveland, R. Generating diagnostic information for behavioral preorders. Distrib Comput 9, 61–75 (1995). https://doi.org/10.1007/s004460050010

Download citation

Key words

  • Formal methods
  • Process algebra
  • Verification algorithms
  • Finite-state systems