Probabilistic timed protocol verification for the extended state transition model

Chung-Ming Huang, Shiun Wei Lee, Jenq Muh Hsu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

In this paper, we propose a Timed Communicating State Machine (TCSM), which belongs to the extended state transition model, to formally specify protocols that incorporate timed properties as part of their specifications. Based on the TCSM model, we also propose (1) a timed global state reachability analysis that takes time bounds and predicates into consideration, and (2) a probabilistic timed verification scheme that is based on the occurrence rates of communicating entities' transitions and the occurrence probabilities of channel entities' transitions. In this way, probability-based partial timed verification can be achieved for extended-state-transition-specified timed protocols.

Original languageEnglish
Title of host publicationProceedings of the Internatoinal Conference on Parallel and Distributed Systems - ICPADS
EditorsLionel M. Ni
PublisherIEEE
Pages432-437
Number of pages6
Publication statusPublished - 1994
EventProceedings of the 1994 International Conference on Parallel and Distributed Systems - Hsinchu, China
Duration: 1994 Dec 191994 Dec 21

Other

OtherProceedings of the 1994 International Conference on Parallel and Distributed Systems
CityHsinchu, China
Period94-12-1994-12-21

Fingerprint

Network protocols
Specifications

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

Huang, C-M., Lee, S. W., & Hsu, J. M. (1994). Probabilistic timed protocol verification for the extended state transition model. In L. M. Ni (Ed.), Proceedings of the Internatoinal Conference on Parallel and Distributed Systems - ICPADS (pp. 432-437). IEEE.
Huang, Chung-Ming ; Lee, Shiun Wei ; Hsu, Jenq Muh. / Probabilistic timed protocol verification for the extended state transition model. Proceedings of the Internatoinal Conference on Parallel and Distributed Systems - ICPADS. editor / Lionel M. Ni. IEEE, 1994. pp. 432-437
@inproceedings{7dcae7f12a0e4c3dbcc50fd610d113e3,
title = "Probabilistic timed protocol verification for the extended state transition model",
abstract = "In this paper, we propose a Timed Communicating State Machine (TCSM), which belongs to the extended state transition model, to formally specify protocols that incorporate timed properties as part of their specifications. Based on the TCSM model, we also propose (1) a timed global state reachability analysis that takes time bounds and predicates into consideration, and (2) a probabilistic timed verification scheme that is based on the occurrence rates of communicating entities' transitions and the occurrence probabilities of channel entities' transitions. In this way, probability-based partial timed verification can be achieved for extended-state-transition-specified timed protocols.",
author = "Chung-Ming Huang and Lee, {Shiun Wei} and Hsu, {Jenq Muh}",
year = "1994",
language = "English",
pages = "432--437",
editor = "Ni, {Lionel M.}",
booktitle = "Proceedings of the Internatoinal Conference on Parallel and Distributed Systems - ICPADS",
publisher = "IEEE",

}

Huang, C-M, Lee, SW & Hsu, JM 1994, Probabilistic timed protocol verification for the extended state transition model. in LM Ni (ed.), Proceedings of the Internatoinal Conference on Parallel and Distributed Systems - ICPADS. IEEE, pp. 432-437, Proceedings of the 1994 International Conference on Parallel and Distributed Systems, Hsinchu, China, 94-12-19.

Probabilistic timed protocol verification for the extended state transition model. / Huang, Chung-Ming; Lee, Shiun Wei; Hsu, Jenq Muh.

Proceedings of the Internatoinal Conference on Parallel and Distributed Systems - ICPADS. ed. / Lionel M. Ni. IEEE, 1994. p. 432-437.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Probabilistic timed protocol verification for the extended state transition model

AU - Huang, Chung-Ming

AU - Lee, Shiun Wei

AU - Hsu, Jenq Muh

PY - 1994

Y1 - 1994

N2 - In this paper, we propose a Timed Communicating State Machine (TCSM), which belongs to the extended state transition model, to formally specify protocols that incorporate timed properties as part of their specifications. Based on the TCSM model, we also propose (1) a timed global state reachability analysis that takes time bounds and predicates into consideration, and (2) a probabilistic timed verification scheme that is based on the occurrence rates of communicating entities' transitions and the occurrence probabilities of channel entities' transitions. In this way, probability-based partial timed verification can be achieved for extended-state-transition-specified timed protocols.

AB - In this paper, we propose a Timed Communicating State Machine (TCSM), which belongs to the extended state transition model, to formally specify protocols that incorporate timed properties as part of their specifications. Based on the TCSM model, we also propose (1) a timed global state reachability analysis that takes time bounds and predicates into consideration, and (2) a probabilistic timed verification scheme that is based on the occurrence rates of communicating entities' transitions and the occurrence probabilities of channel entities' transitions. In this way, probability-based partial timed verification can be achieved for extended-state-transition-specified timed protocols.

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

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

M3 - Conference contribution

AN - SCOPUS:0028758722

SP - 432

EP - 437

BT - Proceedings of the Internatoinal Conference on Parallel and Distributed Systems - ICPADS

A2 - Ni, Lionel M.

PB - IEEE

ER -

Huang C-M, Lee SW, Hsu JM. Probabilistic timed protocol verification for the extended state transition model. In Ni LM, editor, Proceedings of the Internatoinal Conference on Parallel and Distributed Systems - ICPADS. IEEE. 1994. p. 432-437