Abstract
Many communication protocols are modeled as finite state machines (FSM’s). In general, the size of states becomes large in order to treat parameter values such as sequence numbers, and the state explosion may occur. In this paper, we will propose an FSM/C model where the executability of each transition may depend on the number of times that its starting state has been visited, and propose a technique for verifying a liveness property for the model where we avoid the state explosion. For verifying the liveness property, we use an integer linear programming technique.
Chapter PDF
References
G.S. Avrunin, U.G. Buy, J.C. Corbett, L.K. Dillon and J.C. Wileden: “Automated Analysis of Concurrent Systems with Constrained Expression Toolset”, IEEE Trans. on Soft. Eng., Vol. 17, No. 11, pp. 1204–1222, 1991.
J.C. Corbett: “Verifying General Safety and Liveness Properties With Integer Programming”, Proc. Computer Aided Verification 82, pp. 337–348, 1992.
M.G. Gouda and N. J. Multari: “Stabilizing Communication Protocols”, IEEE Trans. on Computers, Vol. 40, No. 4, pp. 448–458, 1991.
LINDO : “Linear interactive and discrete optimizer for linear, integer, and quadratic programming problems”, LINDO Systems, Inc..
S.S. Lam and A. U. Shanker: “Protocol Validation via Projection”, IEEE Trans. on Soft. Eng., Vol. SE-10, No. 4, pp. 325–361, 1984.
J.R. Zhao and G. V. Bochmann: “Reduced Reachability Analysis of Communication Protocols: A New Approach”, Proc. 6th IFIP Int. Conf. Protocol Specification, Testing and Verification (PSTV VI), pp.243–254, North-Holland, 1986.
T. Higashino, A. Nakata, T. Itoh and K. Taniguchi: “Verification of Liveness Property for Communicating FSM’s with Conditional Transitions depending on State Visiting Numbers”, ICS Research Report, 95-ICS-6, Dept. Information and Computer Sciences, Osaka University, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Higashino, T., Nakata, A., Itoh, T., Taniguchi, K. (1996). Verification of Liveness Property for Communicating FSM’s with Conditional Transitions depending on State Visiting Numbers. In: Bochmann, G.v., Dssouli, R., Rafiq, O. (eds) Formal Description Techniques VIII. FORTE 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34945-9_31
Download citation
DOI: https://doi.org/10.1007/978-0-387-34945-9_31
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2958-9
Online ISBN: 978-0-387-34945-9
eBook Packages: Springer Book Archive