DocumentCode :
2257005
Title :
An Estelle-based probabilistic partial timed protocol verification system
Author :
Huang, Chung-Ming ; Hsu, Jenq-Muh
Author_Institution :
Dept. of Comput. Sci. & Inf. Eng., Nat. Cheng Kung Univ., Tainan, Taiwan
fYear :
2000
fDate :
2000
Firstpage :
83
Lastpage :
90
Abstract :
Complete verification of communication protocols is usually very hard to achieve due to the combinatorial state space explosion problem. Probability based partial verification provides an alternative solution to solve this problem. We adopt a Timed Communicating State Machine (TCSM), which belongs to the Extended Communicating Finite State Machine (ECFSM) model, to formally specify protocols that incorporate timed properties as part of their specifications. Based on the TCSM model, we propose a probabilistic timed verification scheme that is based on the occurrence rates of communicating entities´ transitions and occurrence probabilities of channel entities´ transitions. Using our probabilistic partial timed protocol verification scheme, an Estelle based Probabilistic Partial Timed Protocol verification system, which is called PTPVS, is developed on SUN SPARC workstations. In this way, protocol designers can use PTPVS to design and partially verify Estelle based protocol specifications with time properties
Keywords :
finite state machines; formal specification; formal verification; probability; protocols; specification languages; Estelle based probabilistic partial timed protocol verification system; Extended Communicating Finite State Machine; PTPVS; SUN SPARC workstations; TCSM model; Timed Communicating State Machine; channel entity transitions; combinatorial state space explosion problem; communicating entity transitions; communication protocols; formal specification; occurrence probabilities; occurrence rates; probabilistic timed verification scheme; probability based partial verification; protocol designers; time properties; timed properties; Automata; Computer science; Explosions; Information management; Probability; Protocols; Reachability analysis; State-space methods; Sun; Workstations;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Parallel and Distributed Systems, 2000. Proceedings. Seventh International Conference on
Conference_Location :
Iwate
ISSN :
1521-9097
Print_ISBN :
0-7695-0568-6
Type :
conf
DOI :
10.1109/ICPADS.2000.857686
Filename :
857686
Link To Document :
بازگشت