PROBABILISTIC VERIFICATION

Communication protocols always have some embedded timed properties (e.g. timeout and transmission delay). To specify and analyse the timed properties, a new formal model is presented in this paper. The new protocol specification model is called the Fuzzy Timed Communicating State Machine (FTCSM) model. Since it is very hard to precisely specify time bounds as constants, the fuzzy time concept is applied to specify time bounds, i.e. each time bound is specified as a time interval. In the 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 verification method is proposed. To deal with the state space explosion problem, 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 System (EPFTPVS) has been developed on SUN SPARC workstations. In this way, a subset of Estelle-specified protocols with fuzzy time specifications can be automatically verified using EPFTPVS. © 1993 Academic Press, Inc.