An approach to verification and validation of a reliable multicasting protocol

ABSTRACT

This paper describes the process of implementing a complex communications protocol that provides reliable delivery of data in multicast-capable, packet-switching telecommunication networks. The protocol, called the Reliable Multicasting Protocol (RMP), was developed incrementally using a combination of formal and informal techniques in an attempt to ensure the correctness of its implementation. Our development process involved three concurrent activities: (1) the initial construction and incremental enhancement of a formal state model of the protocol machine; (2) the initial coding and incremental enhancement of the implementation; and (3) model-based testing of iterative implementations of the protocol. These activities were carried out by two separate teams: a design team and a V&V team. The design team built the first version of RMP with limited functionality to handle only nominal requirements of data delivery. In a series of iterative steps, the design team added new functionality to the implementation while the V&V team kept the state model in fidelity with the implementation. This was done by generating test cases based on suspected errant or off-nominal behaviors predicted by the current model. If the execution of a test was different between the model and implementation, then the differences helped identify inconsistencies between the model and implementation. The dialogue between both teams drove the co-evolution of the model and implementation. Testing served as the vehicle for keeping the model and implementation in fidelity with each other. This paper describes (1) our experiences in developing our process model; and (2) three example problems found during the development of RMP.

REFERENCES

• 1: Gang Luo , G. von Bochmann , A. Petrenko, Test Selection Based on Communicating Nondeterministic Finite-State Machines Using a Generalized Wp-Method, IEEE Transactions on Software Engineering, v.20 n.2, p.149-162, February 1994 [doi>10.1109/32.265636]
• 2: Deepinder P. Sidhu , Ting-kau Leung, Formal Methods for Protocol Testing: A Detailed Study, IEEE Transactions on Software Engineering, v.15 n.4, p.413-426, April 1989 [doi>10.1109/32.16602]
• 3: Montgomery, T., Design, Implementation, and Verification of the Reliable Multicasting Protocol, M.S. Thesis, West Virginia University, December 1994.
• 4: Jo-Mei Chang , N. F. Maxemchuk, Reliable broadcast protocols, ACM Transactions on Computer Systems (TOCS), v.2 n.3, p.251-273, Aug. 1984 [doi>10.1145/989.357400]
• 5: Victor Yodaiken , Krithi Ramamritham, Verification of a Reliable Net Protocol, Proceedings of the Second International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.193-215, January 08-10, 1992
• 6: Heninger, K.L., Specifying software for complex systems: New techniques and their application, IEEE Transactions on Software Engineering, Volume 6, Number 1, January 1980.
• 7: Farnam Jahanian , Aloysius K. Mok, Modechart: A Specification Language for Real-Time Systems, IEEE Transactions on Software Engineering, v.20 n.12, p.933-947, December 1994 [doi>10.1109/32.368134]
• 8: Nancy G. Leveson , Mats Per Erik Heimdahl , Holly Hildreth , Jon D. Reese, Requirements Specification for Process-Control Systems, IEEE Transactions on Software Engineering, v.20 n.9, p.684-707, September 1994 [doi>10.1109/32.317428]
• 9: S. Owre, N. Shankar, and J. M. Rushby, User Guide for the PVS Specification and Verification System (Beta Release), Computer Science Laboratory, SRI International, 1991.
• 10: David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
• 11: J. Burch, E. Clarke, D. Long, K. McMillan, and D. Dill, Symbolic Model Checking for Sequential Circuit Verification, IEEE Transactions on Computer-Aided Design, Volume 13, Number 4, April 1994.
• 12: Gerard J. Holzmann , Doron Peled, An improvement in formal verification, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, p.197-211, January 1995
• 13: S. E. Deering, Multicast routing in internetworks and extended LANs, Symposium proceedings on Communications architectures and protocols, p.55-64, August 16-18, 1988, Stanford, California, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation

Additional Classification:
  B. Hardware
  B.4 INPUT/OUTPUT AND DATA COMMUNICATIONS

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.9 Management
          Subjects: Life cycle

General Terms:
Design, Reliability, Verification