Advertisement

Re-Usable Verification Elements for High-Speed Transfer Protocol Configurations

  • P. Herrmann
  • H. Krumm
Chapter
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)

Abstract

Presently, many communication protocols are under development which are tailored to the efficient high-speed data transfer meeting different application-specific requirements. Our approach concentrates on a framework which facilitates the formal verification of the protocols. The framework supplies verified and re-usable implications between predefined protocol and service specification components. For the verification of a specific protocol, protocol, service and medium can be modelled as compositions of framework specification components. The verification corresponds to proving that the system of protocol and medium implies the service. This implication can be proven by combining component implications of the framework. We apply L. Lamport’s Temporal Logic of Actions (TLA) and use a TLA specification style supporting the compositional specification of process systems and the inference of system properties from process properties.

Keywords

Composition examples framework protocol synthesis TLA verification 

References

  1. Abadi, M. and Lamport, L. (1991) The Existence of Refinement Mappings. Theoretical Computer Science, 82 (2), 253–84.MathSciNetCrossRefzbMATHGoogle Scholar
  2. Abadi, M. and Lamport, L. (1993) Composing specifications. ACM Transactions on Programming Languages and Systems, 15 (1), 73–132.CrossRefGoogle Scholar
  3. Clark, D.D. and Tennenhouse, D.L. (1990) Architectural Considerations for a New Generation of Protocols. Computer Communications Review 20(4), 200–8, ACM SIGCOMM’90 Symposium, Philadelphia.CrossRefGoogle Scholar
  4. Doeringer, W.A., Dykeman, D., Kaiserswerth, M., Meister, W., Rudin, H., and Williamson, R. (1990) A Survey of Light-Weight Transport Protocols for High-Speed Networks. IEEE Transactions on Communications, 38 (11), 2025–39.CrossRefGoogle Scholar
  5. Haas, Z. (1991) A Protocol Structure for High-Speed Communication over Broadband ISDN. IEEE Network Magazine, Jan., 64–70.Google Scholar
  6. Herrmann, P. and Krumm, H. (1994) Compositional Specification and Verification of High-Speed Transfer Protocols, in Protocol Specification, Testing, and Verification XIV (ed. S.T. Vuong and S.T. Chanson ), IFIP, Chapmann amp; Hall, 339–46.Google Scholar
  7. Holzmann, G.J. (1990) Algorithms for Automated Protocol Verification. ATamp;T Technical Journal, Jan., 32–44.Google Scholar
  8. Holzmann, G.J. (1994) The Theory and Practice of A Formal Method: NewCoRe, in 13th World Computer Congress 94, volume I (ed. B. Pehrson and I. Simon), IFIP, Elsevier.Google Scholar
  9. ISO (1987) LOTOS: Language for the temporal ordering specification of observational behaviour International Standard ISO/IS 8807 edition.Google Scholar
  10. Kurki-Suonio, R. and Järvinen, H.M. (1988) Action system approach to the specification and design of distributed systems. ACM Transactions on Programming Languages and Systems, 4 (10), 510–54.Google Scholar
  11. La Porta, T.F. and Schwartz, M. (1993) The Multistream protocol: A highly flexible high-speed transport protocol. IEEE Journ. on Sel. Areas in Communications, 11 (4).Google Scholar
  12. Lamport, L. (1992) TLA+: Syntax and Semantics, preliminary version, Research Report, DEC Digital Systems Research Center, Palo Alto, to appear.Google Scholar
  13. Lamport, L. (1994) The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16 (3), 872–923.CrossRefGoogle Scholar
  14. Mester, A. and Krumm, H. (1995) Composition and Refinement Mapping based Construction of Distributed Applications, in Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TAPSOFT’95 satellite), BRICS, to appear.Google Scholar
  15. O’Malley, S.W. and Peterson, L.L. (1991) A Highly-Layered Architecture for High-Speed Networks, in Protocols for High-Speed Networks, II (ed. M.J. Johnson), IFIP WG 6.1/WG 6.4, North-Holland.Google Scholar
  16. Plagemann, T., Plattner, B., Vogt, M., and Walter. T. (1993) Modules as Building Blocks for Protocol Configuration. in International Conference on Network Protocols, Los Alamitos, California, IEEE Computer Society Press.Google Scholar
  17. Shankar, A.U. and Lam, S.S. (1992) A Stepwise Refinement Heuristic for Protocol Construction. ACM Transactions of Programming Languages and Systems, 14 (3), 417–61.CrossRefGoogle Scholar
  18. Vissers, C.A., Scollo, G., and van Sinderen, M. (1988) Architecture and specification style in formal descriptions of distributed systems, in Protocol Specification, Testing and Verification VIII (ed. S. Agarwal and K. Sabnani ), IFIP, Elesevier, 189–204.Google Scholar
  19. Zitterbart, M., Stiller B., and Tantawy, A.N. Application-Driven Flexible Protocol Configuration, in Kommunikation in Verteilten Systemen (ed. N. Gerner, H.-G. Hegering, and J. Swoboda), GI/ITG, 8. Fachtagung, München, Springer-Verlag, 144–58.Google Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • P. Herrmann
    • 1
  • H. Krumm
    • 1
  1. 1.Dept. of Computer ScienceUniversity of DortmundDortmundGermany

Personalised recommendations