This Article 
 Bibliographic References 
 Add to: 
SDE: Incremental Specification and Development of Communications Software
April 1991 (vol. 40 no. 4)
pp. 553-561

A technique for applying formal message sequence specifications to the full definition of systems is presented. The technique supports automatic transformation of message sequence descriptions into communicating process descriptions that implement the sequences. It also supports hierarchical verification of protocols in the message sequences and process descriptions. Both a language for message sequence description, SAL, and a design support environment, SDE, have been developed based on the proposed technique. To collectively and hierarchically describe message sequences, SAL can compose message sequences from message sequence elements. By adding SAL descriptions, SDE supports the incremental specification and development of communications software: consistency between the added sequences and existing software is verified, and the existing software is automatically updated. This support especially contributes to the efficient maintenance of communications software. The feasibility and usefulness of the proposed technique are demonstrated by experimental application of SDE to PBX.

[1] G. v. Bochmann, "Usage of protocol development tools: The result of a survey," inProtocol Specification, Testing and Verification VII. Amsterdam, The Netherlands: North-Holland, 1987, pp. 147-170.
[2] M. T. Liu, "Protocol engineering," inAdvances in Computers, Vol. 29, New York: Academic, 1989, pp. 79-195.
[3] H. Rudin, "Protocol engineering: A critical assessment," inProc. 8th IFIP Symp. Protocol Specification, Testing, Verification, North-Holland, 1988, pp. 3-16.
[4] ISO, ISO 9074, "Information Processing Systems, Open Systems Interconnection, Estelle--A Formal Description Technique Based on an Extended State Transition Model."
[5] H. Ichikawa, M. Itoh, and M. Shibasaki, "Protocol oriented service specifications and their transformation into CCITT specification and description language,"Trans. IECE Japan, vol. E69, no. 4, pp. 524-535, 1986.
[6] H. Ichikawa, M. Itoh, and J. Kato, "Communications software management with verification and transformation of protocol-oriented specifications," inProc. GLOBECOM'87, Nov. 1987, pp. 651-655.
[7] P. W. Dell, L. A. Jackson, R. O'Brien, and R. Tinker, "Computer-aided design for software,"Software&Microsyst., vol. 1, no. 1, 1981.
[8] M. Itoh and H. Ichikawa, "Hierarchical verification of communications programs specification based on concurrent processes,"Trans. IECE Japan, vol. J69-B, no. 5, pp. 449-459, May 1986.
[9] M. Itoh and H. Ichikawa, "Protocol verification algorithm using reduced reachability analysis,"Trans. IECE Japan, vol. E66, no. 2, pp. 88-93, 1983.
[10] M. Kajiwara, H. Ichikawa, M. Itoh, and Y. Yoshida, "Specification and verification of switching software,"IEEE Trans. Commun., vol. COM-33, no. 3, pp. 193-198, 1985.
[11] G. V. Bochmann and R. Gotzhein, "Deriving protocol specifications from service specifications," inProc. SIGCOMM'86, 1986, pp. 144-156.
[12] F. Khendek, G. V. Bochmann, and C. Kant., "New results on deriving protocol specifications from service specifications," inProc. ACM SIGCOMM'89 Symp., 1989, pp. 136-145.
[13] P. M. Chu and M. T. Liu, "Synthesizing protocol specifications from service specifications," inProc. IEEE Computer Networking Symp., 1988, pp. 173-182,
[14] P. M. Chu and M. T. Liu, "Protocol synthesis in a state-transition model," inProc. COMPSAC'88, 1988, pp. 505-512.
[15] J. Kato, M. Itoh, and H. Ichikawa, "Optimization of concurrent process program specification," inProc. Third Karuizawa Workshop Circuits Syst., 1990, pp. 175-182.
[16] J. E. Hopcroft, "An n log n algorithm for minimizing states in a finite automaton," inTheory of Machines and Computations. New York: Academic, 1971.
[17] A. V. Aho, J. E. Hopcroft, and J. D. Ullman,The Design and Analysis of Computer Algorithms. Menlo Park, CA: Addison-Wesley, 1974.
[18] J. Kato and N. Arakawa, "Software architecture for automated communications software development," inProc. IEE 7th Int. Conf. Software Eng. Telecommun. Switching Syst., July 1989, pp. 29-33.
[19] ISO, ISO 8807, "Information Processing Systems, Open Systems Interconnection, LOTOS--A Formal Description Technique Based on the Temporal Ordering of Observational-Behaviour."
[20] CCITT, Recommendation Z.100, "Functional Specification and Description Language (SDL)," 1988.
[21] A. Takura and H. Ichikawa, "Completing protocols according to requirements," inProc. ICCC Symp.'89, Beijing, Sept. 1989, pp. 116-119.
[22] I. Nishikado, Y. Sakai, and T. Kubo, "Integrated key telephone system with digital bus architecture,"Rev. Elec. Commun. Labs., vol. 35, no. 6, pp. 657-664, 1987.
[23] CCITT Recommendations X.200-250, 1988.
[24] CCITT Recommendations X.20-32, 1988.
[25] M. Accettaet al., "Mach: A new kernel foundation for UNIX development," inProc. USENIX 1986 Summer Conf., 1986, pp. 93-112.
[26] Sun Microsystems, Inc., "SUN OS4.0 System services overview," 1988.
[27] H. Ichikawa, K. Yamanaka, and J. Kato, "Incremental specification in LOTOS," inProc. 10th IFIP Symp. Protocol Specification, Testing, Verification, June 1990, pp. 185-200.
[28] R. J. Haas and R. W. Humes, "Intelligent Network/2: A network architecture concept for the 1990s," inProc. Int. Switching Symp., Mar. 1987, pp. 944-951.
[29] T. Kondo, H. Sakai, T. Yamaguchi, and E. Kamimura, "Architecture of open application system," Rep. of Tech. Group, IECE J, SE87-89, 1987.
[30] P. Zafiropulo, "Protocol validation by duologue-matrix analysis,"IEEE Trans. Commun., COM-27, pp. 1761-1780, 1979.

Index Terms:
SDE; incremental specification and development; communications software; formal message sequence specifications; hierarchical verification of protocols; SAL; design support environment; PBX; computer communications software; formal specification; program verification; protocols.
H. Ichikawa, M. Itoh, J. Kato, A. Takura, M. Shibasaki, "SDE: Incremental Specification and Development of Communications Software," IEEE Transactions on Computers, vol. 40, no. 4, pp. 553-561, April 1991, doi:10.1109/12.88473
Usage of this product signifies your acceptance of the Terms of Use.