On the verification of time-dependent protocols using timed reachability analysis

Fuchun Lin; Ming T. Liu; Charles J. Graff

doi:10.1109/HICSS.1989.48003

On the verification of time-dependent protocols using timed reachability analysis

Fuchun Lin^*, Ming T. Liu, Charles J. Graff

^*Corresponding author for this work

Institute of Network Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

2 Scopus citations

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.

Original language	English
Title of host publication	Proceedings of the Hawaii International Conference on System Science
Editors	Bruce D. Shriver
Publisher	Publ by Western Periodicals Co
Pages	285-294
Number of pages	10
ISBN (Print)	0818619120
DOIs	https://doi.org/10.1109/HICSS.1989.48003
State	Published - 1 Dec 1989
Event	Proceedings of the Twenty-Second Annual Hawaii International Conference on System Sciences: Software Track - Kailua-Kona, Hawaii, USA Duration: 3 Jan 1989 → 6 Jan 1989

Publication series

Name	Proceedings of the Hawaii International Conference on System Science
Volume	2
ISSN (Print)	0073-1129

Conference

Conference	Proceedings of the Twenty-Second Annual Hawaii International Conference on System Sciences: Software Track
City	Kailua-Kona, Hawaii, USA
Period	3/01/89 → 6/01/89

Access to Document

10.1109/HICSS.1989.48003

Cite this

Lin, F., Liu, M. T., & Graff, C. J. (1989). On the verification of time-dependent protocols using timed reachability analysis. In B. D. Shriver (Ed.), Proceedings of the Hawaii International Conference on System Science (pp. 285-294). (Proceedings of the Hawaii International Conference on System Science; Vol. 2). Publ by Western Periodicals Co. https://doi.org/10.1109/HICSS.1989.48003

@inproceedings{f97e7524f82f46fbaeb5617e32df6932,

title = "On the verification of time-dependent protocols using timed reachability analysis",

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. ",

author = "Fuchun Lin and Liu, {Ming T.} and Graff, {Charles J.}",

year = "1989",

month = dec,

day = "1",

doi = "10.1109/HICSS.1989.48003",

language = "English",

isbn = "0818619120",

series = "Proceedings of the Hawaii International Conference on System Science",

publisher = "Publ by Western Periodicals Co",

pages = "285--294",

editor = "Shriver, {Bruce D.}",

booktitle = "Proceedings of the Hawaii International Conference on System Science",

note = "Proceedings of the Twenty-Second Annual Hawaii International Conference on System Sciences: Software Track ; Conference date: 03-01-1989 Through 06-01-1989",

}

Lin, F, Liu, MT & Graff, CJ 1989, On the verification of time-dependent protocols using timed reachability analysis. in BD Shriver (ed.), Proceedings of the Hawaii International Conference on System Science. Proceedings of the Hawaii International Conference on System Science, vol. 2, Publ by Western Periodicals Co, pp. 285-294, Proceedings of the Twenty-Second Annual Hawaii International Conference on System Sciences: Software Track, Kailua-Kona, Hawaii, USA, 3/01/89. https://doi.org/10.1109/HICSS.1989.48003

On the verification of time-dependent protocols using timed reachability analysis. / Lin, Fuchun; Liu, Ming T.; Graff, Charles J.
Proceedings of the Hawaii International Conference on System Science. ed. / Bruce D. Shriver. Publ by Western Periodicals Co, 1989. p. 285-294 (Proceedings of the Hawaii International Conference on System Science; Vol. 2).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - On the verification of time-dependent protocols using timed reachability analysis

AU - Lin, Fuchun

AU - Liu, Ming T.

AU - Graff, Charles J.

PY - 1989/12/1

Y1 - 1989/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0024863478&partnerID=8YFLogxK

U2 - 10.1109/HICSS.1989.48003

DO - 10.1109/HICSS.1989.48003

M3 - Conference contribution

AN - SCOPUS:0024863478

SN - 0818619120

T3 - Proceedings of the Hawaii International Conference on System Science

SP - 285

EP - 294

BT - Proceedings of the Hawaii International Conference on System Science

A2 - Shriver, Bruce D.

PB - Publ by Western Periodicals Co

T2 - Proceedings of the Twenty-Second Annual Hawaii International Conference on System Sciences: Software Track

Y2 - 3 January 1989 through 6 January 1989

ER -

On the verification of time-dependent protocols using timed reachability analysis

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this