Abstract
This paper presents a method for verifying safety property of a communication protocol modeled as two extended communicating finite-state machines with two unbounded FIFO channels connecting them. In this method, four types of atomic formulae specifying a condition on a machine and a condition on a sequence of messages in a channel are introduced. A human verifier describes a logical formula which expresses conditions expected to be satisfied by all reachable global states, and a verification system proves that the formula is indeed satisfied by such states (i.e. the formula is an invariant) by induction. If the invariant is never satisfied in any unsafe state, it can be concluded that the protocol is safe. To show the effectiveness of this method, a sample protocol extracted from the data transfer phase of the OSI session protocol was verified by using the verification system.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Brand D., and Zafiropulo P.: “On Communicating Finite-State Machines”, Journal of ACM, vol.30, pp.323–342, 1983–04.
Kakuda Y., Wakahara Y., and Norigoe M.: “A New Algorithm for Fast Protocol Validation”, Proc. of Compsac-86, pp.228–236, 1986.
Yuang M.C., and Kershebaum A.: “Parallel Protocol Verification: The Two-Phase Algorithm”, Proc. 9th Intern. Symp. on PSTV, pp.339–353, 1989.
ISO: “Information Processing Systems-Open Systems Interconnection-Estelle: A Formal Description Technique Based on an Extended State Transition Model”, ISO/DIS 9074, 1987.
CCITT: “Specification and Description Language(SDL)”, Recommendation Z100, 1989.
Gordon M.J.C.: “A Proof Generating System for Higher-Order Logic” in “VLSI Specification, Verification and Synthesis”, Kluwer Academic Publishers, pp.73–128, 1987-01.
Sarikaya B., Bochmann G.V., and Koukoulidis V.: “Method of Analysing Extended Finite-State Machine Specifications”, Computer Communications, vol.13, no.2, pp.83–92, 1990–03.
Finkel A.: “A New Class of Analyzable CFSMs with Unbounded FIFO Channels”, Proc. 8th Intern. Symp. on PSTV, pp.283–294, 1988.
Huet G., and Oppen D.:“Equations and Rewrite Rules A Survey” in “Formal Language: Perspectives and Open Problems”, R. Book eds., Academic Press, pp.349–405, 1980.
ISO: “Basic Connection Oriented Session Protocol Specification”, ISO 8327.
Higuchi M., Seki H., and Kasami T.: “A Method of Composing Communication Protocols with Priority Service”, to appear in IEICE Trans. Commun., 1992-10.
Choi T.Y., and Miller R.E.: “A Decomposition Method for the Analysis and Design of Finite State Protocols”, Proc. of 8th ACM/IEEE Data Comm. Symp., pp.167–176, 1983.
Lin H.: “Constructing Protocols with Alternative Functions”, IEEE Trans. Comput., vol.40, pp.376–386, 1991-04.
Chow C., Gouda M.G., and Lam S.S.: “A Discipline for Constructing Multiphase Communication Protocols”, ACM Trans. on Computer Systems, vol.3, pp.315–343, 1985-11.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Higuchi, M., Shirakawa, O., Seki, H., Fujii, M., Kasami, T. (1993). A verification procedure via invariant for extended communicating finite-state machines. In: von Bochmann, G., Probst, D.K. (eds) Computer Aided Verification. CAV 1992. Lecture Notes in Computer Science, vol 663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56496-9_30
Download citation
DOI: https://doi.org/10.1007/3-540-56496-9_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56496-6
Online ISBN: 978-3-540-47572-9
eBook Packages: Springer Book Archive