Abstract
A protocol specification, based on which a communication system is built, should be designed without an error because a late error detection makes system correction unacceptably expensive. It is, however, becoming more and more difficult to design error-free protocol specifications for the modern complex communication systems. Such a situation causes a great demand for tools that automatically verifies properties required for protocols. One of the required properties is freedom of logic errors such as undefined reception or deadlock. Another property which is essential to reliable systems is responsiveness, i.e., a fault-tolerant and real-time property. In this paper, we introduce our protocol validation tool that verifies freedom of logic errors using the acyclic expansion algorithm. Then we discuss its applicability to the verification of responsiveness.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Y. Kakuda, Y. Wakahara, and M. Norigoe, “An acyclic expansion algorithm for fast protocol validation,” IEEE Trans. Software Eng., vol. SE-14, no. 8, pp. 1059–1070, Aug. 1988.
Y. Kakuda and T. Kikuno, “Verification of responsiveness for communication protocols,” Rep. of Tech. Group, IEICE of Japan, FTS91-57, Dec. 1991.
M. T. Liu, “Protocol engineering,” ADVANCE IN COMPUTERS, vol. 29, pp. 110–113, New York: Academic, 1989.
H. Saito and Y. Kakuda, “Protocol validation system based on the acyclic expansion algorithm,” Rep. of Tech. Group, IEICE of Japan, SSE90-18, May 1990. in Japanese.
“CCITT Recommendation Z.100, Melbourne,” Nov. 1988.
A.Ito, E. Utsunomiya, F. Nitta, Y. Kakuda, and H. Saito, “Evaluation of tools in ESCORT,” SDL’91:Evolving Methods, pp. 437–448, North-Holland, 1991.
M. Malek, “Responsive systems (A challenge for the nineties),” Microprocessing and Microprogramming, vol. 30, pp. 9–16, North-Holland, Aug. 1990.
E.W. Dijkstra, “Self-stabilizing systems in spite of distributed control,” Communications of the ACM, vol. 17, no. 11, pp. 643–644, Nov. 1974.
H. Saito, T. Hasegawa, and Y. Kakuda, “Protocol verification system for SDL specifications based on acyclic expansion algorithm and temporal logic,” 4th In’l Conf. on Formal Description Techniques (FORTE’91), pp. 513–528, Nov. 1991.
J. A. Stankovic, “Misconceptions about real-time computing: A serious problem for next-generation systems,” Computer, vol. 21, no. 10, pp. 10–19, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer-Verlag/Wien
About this paper
Cite this paper
Saito, H., Hasegawa, T. (1993). Protocol Validation Tool and Its Applicability to Responsive Protocols. In: Kopetz, H., Kakuda, Y. (eds) Responsive Computer Systems. Dependable Computing and Fault-Tolerant Systems, vol 7. Springer, Vienna. https://doi.org/10.1007/978-3-7091-9288-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-7091-9288-7_13
Publisher Name: Springer, Vienna
Print ISBN: 978-3-7091-9290-0
Online ISBN: 978-3-7091-9288-7
eBook Packages: Springer Book Archive