DocumentCode :
2130526
Title :
A semi-automated verification method for communication protocols modeled as 2-ECFSMs
Author :
Higuchi, M. ; Sano, J. ; Hara, K. ; Fujii, M.
Author_Institution :
Dept. of Inf. & Comput. Sci., Osaka Univ., Japan
fYear :
1996
fDate :
27-30 May 1996
Firstpage :
290
Lastpage :
297
Abstract :
Previously, we proposed a verification method via invariants for communication protocol modeled as 2-ECPSMs. In the proposed method, a human verifier describes an invariant of a given protocol in a disjunctive normal form, and a verification system shows safety or liveness based on the invariant. The tedious work on describing invariant formulae is the most significant shortcoming of the proposed method. This paper deals with a semi-automated derivation of invariant formulae for communication protocol modeled as 2-ECFSMs. In the method, the logical formula which holds on a subset of reachable states is automatically generated. Such a subset consists of states which are teachable by synchronous communication from the initial states and those which are reachable by sequences of sending transitions from synchronously reachable states. To obtain an invariant, a human verifier supplements several disjuncts for other part of reachability set. We conducted an experiment on deriving an invariant formula of a sample protocol extracted from the OSI session protocol. By the result, 636 conjunctive formulae were automatically derived and the conjunction of those formulae was shown to be an invariant of the sample protocol, i.e. the sample protocol was shown to be safe automatically
Keywords :
finite state machines; formal verification; open systems; protocols; 2-ECFSMs; OSI session protocol; communication protocols; disjunctive normal form; human verifier; invariant formula; liveness; safety; semi-automated verification method; Communication channels; Communication system control; Context; Data analysis; Humans; Open systems; Petri nets; Protocols; Software safety; Turing machines;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Distributed Computing Systems, 1996., Proceedings of the 16th International Conference on
Print_ISBN :
0-8186-7399-0
Type :
conf
DOI :
10.1109/ICDCS.1996.507927
Filename :
507927
Link To Document :
بازگشت