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
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;
Conference_Titel :
Parallel and Distributed Systems, 2000. Proceedings. Seventh International Conference on
Conference_Location :
Iwate
Print_ISBN :
0-7695-0568-6
DOI :
10.1109/ICPADS.2000.857686