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

Volume

2

fYear

1989

fDate

3-6 Jan 1989

Firstpage

285

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/HICSS.1989.48003

Filename

48003