Title :
On the verification of time-dependent protocols using timed reachability analysis
Author :
Lin, Fuchun Joseph ; Liu, Ming T. ; Graff, Charles J.
Author_Institution :
Ohio State Univ., Columbus, OH, USA
Abstract :
An automated approach to verifying general properties of time-dependent protocols, using a formal model called time transmission grammar plus (TTG+), is introduced. The novel part of the approach is to represent the global state of the model as a pair of state and timing constraint matrices. Timed reachability analysis based on such a representation is then developed to verify various protocol properties. A simple multidestination stop-and-wait protocol is used to illustrate the model and the reachability algorithm
Keywords :
computer communications software; grammars; program verification; protocols; TTG+; automated approach; formal model; global state; multidestination stop-and-wait protocol; protocol properties; reachability algorithm; time transmission grammar plus; time-dependent protocol verification; timed reachability analysis; timing constraint matrices; Automata; Contracts; Gold; Laboratories; Petri nets; Protocols; Reachability analysis; Timing;
Conference_Titel :
System Sciences, 1989. Vol.II: Software Track, Proceedings of the Twenty-Second Annual Hawaii International Conference on
Conference_Location :
Kailua-Kona, HI
Print_ISBN :
0-8186-1912-0
DOI :
10.1109/HICSS.1989.48003
