PROBABILISTIC FUZZY TIMED PROTOCOL VERIFICATION

Communication protocols always have some embedded timed properties (e. g. timeout and transmission delay). To specify and analyse the timed p roperties, a new formal model is presented in this paper. The new prot ocol specification model is called the Fuzzy Timed Communicating State Machine (FTCSM) model. Since it is very hard to precisely specify tim e bounds as constants, the fuzzy time concept is applied to specify ti me bounds, i.e. each time bound is specified as a time interval. In th e FTCSM model, each protocol entity and each communication channel is specified as an FTCSM, respectively. To analyse various properties of protocols specified in the FTCSM model, a fuzzy timed protocol verific ation method is proposed. To deal with the state space explosion probl em, we adopt the probability-based partial timed verification approach . The corresponding probabilistic fuzzy timed verification scheme for the FTCSM model is also presented in detail. Using the FTCSM model and the associated probabilistic fuzzy timed protocol verification method , an Estelle-like Probabilistic Fuzzy Timed Protocol Verification Syst em (EPFTPVS) has been developed on SUN SPARC workstations. In this way , a subset of Estelle-specified protocols with fuzzy time specificatio ns can be automatically verified using EPFTPVS.