Using compositional preorders in the verification of sliding window protocol

  • Roope Kaivola
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


The main obstacle to automatic verification of temporal logic properties of finite-state systems is the state explosion problem. One way to alleviate this is to replace components of a system with smaller ones and verify the required properties from the smaller system. This approach leads to notions of compositional property-preserving equivalences and preorders. Previously we have shown that the NDFD preorder is the weakest preorder which is compositional w.r.t. standard operators and preserves nexttime-less linear temporal logic properties. In this paper we describe a case study where NDFD preorder was used to verify semiautomatically both safety and liveness properties of the Sliding Window protocol for arbitrary channel lengths and realistic parameter values. In this process we located a previously undiscovered fault leading to lack of liveness in a version of the protocol.


Data Item Temporal Logic Safety Property Label Transition System Execution Sequence 
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.


  1. 1.
    Bolognesi, T. & Brinksma, E.: Introduction to the ISO specification language LOTOS, in The Formal Descr. Technique LOTOS, North-Holland, 1989, pp. 23–73Google Scholar
  2. 2.
    Clarke, E. M. & Long, D. E. & McMillan, K. L.: Compositional model checking, in Proceedings of the Fourth IEEE LICS, 1989, pp. 353–362Google Scholar
  3. 3.
    De Nicola, R. & Vaandrager, F.: Action vs. state based logics for transition systems, in Semantics of Sys. of Conc. Proc., LNCS vol. 469, Springer, 1990, pp. 407–419Google Scholar
  4. 4.
    Emerson, E. A.: Temporal and modal logic, in van Leeuwen, J. (ed.): Handbook of Theoretical Computer Science, Elsevier/North-Holland, 1990, pp. 997–1072Google Scholar
  5. 5.
    Graf, S. & Steffen, B. & Lüttgen, G.: Compositional Minimisation of Finite State Systems Using Interface Spec., in Formal Asp. of Comp., vol. 8, 1996, pp. 607–616Google Scholar
  6. 6.
    International Standards Organisation: Data Communications — HDLC Unbalanced Class of Procedures, Ref. No. ISO 6159, ISO, Geneva, 1980Google Scholar
  7. 7.
    Kaivola, R.: Equivalences, Preorders and Compositional Verification for Linear Time Temp. Logic and Conc. Sys., A-1996-1, Univ. of Helsinki, Dept. of Comp. Sci., 1996, 176+9 p., also in www.cs.Helsinki.FI/~rkaivola/research/ft.psGoogle Scholar
  8. 8.
    Kaivola, R. & Valmari, A.: Using truth-preserving reductions to improve the clarity of Kripke-models, in CONCUR'91, LNCS vol. 527, Springer, 1991, pp. 361–375Google Scholar
  9. 9.
    Kaivola, R. & Valmari, A.: The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic, CONCUR'92, LNCS vol. 630, Springer, 1992, pp. 207–221Google Scholar
  10. 10.
    Manna, Z. & Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, vol. 1, Specification, Springer, 1991Google Scholar
  11. 11.
    Richier, J. L. & Rodriguez, C. & Sifakis, J. & Voiron, J.: Verification in Xesar of the sliding window protocol, in PSTV VII, North-Holland, 1987, pp. 235–248Google Scholar
  12. 12.
    Sabnani, K.: An algorithmic technique for protocol verification, in IEEE Transactions on Communications, vol. 36, no. 8, 1988, pp. 924–931Google Scholar
  13. 13.
    Stenning, N. V.: A data transfer protocol, in Computer Networks, vol. 11, 1976, pp. 99–110Google Scholar
  14. 14.
    Stirling, C.: Modal and temporal logics, in Abramsky, S. & al. (eds.): Handbook of Logic in Computer Science, Oxford University Press, 1992, pp. 477–563Google Scholar
  15. 15.
    Valmari, A. & Kemppainen, J. & Clegg, M. & Levanto, M.: Putting advanced reachability analysis techniques together: the “ARA” tool, in FME'93: Industrial-Strength Formal Methods, LNCS vol. 670, Springer, 1993, pp. 597–616Google Scholar
  16. 16.
    Valmari, A. & Tienari, M.: Compositional failure-based semantic models for Basic LOTOS, in Formal Aspects of Computing, vol. 7, 1995, pp. 440–468Google Scholar
  17. 17.
    Wolper, P.: Expressing interesting properties of programs in propositional temporal logic, in Proceedings of the 13th ACM POPL, 1986, pp. 184–193Google Scholar
  18. 18.
    Wolper, P. & Lovinfosse, V.: Verifying Properties of Large Sets of Processes with Network Invariants, in Proc. of International Workshop on Automatic Verification Methods for Finite State Systems, LNCS vol. 407, Springer, 1990, pp. 68–80Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Roope Kaivola
    • 1
  1. 1.Department of Computer ScienceUniversity of HelsinkiFinland

Personalised recommendations