The timed communicating state machine (TCSM) for communication protocols

This paper presents a new model, named Timed Communicating State Machine (TCSM) to specify protocols that incorporate timed properties as part of their specifications. Using the TCSM model, each transition is associated with a head state, a tail state, a predicate, an input event, a time interval, and an action part. In this way, the TCSM model can be directly applied to ISO´s Estelle, which is a Formal Description Technique (FDT) for specifying communication protocols. The notations of the TCSM are also based on that of Estelle, so that they are not foreign to users of Estelle. We also present the corresponding formal TCSM-based verification scheme. Bases on the TCSM model and the verification scheme, we are currently developing an Estelle-based timed protocol verification system on SUN SPARC workstations