Estelle, an internationally standardized Formal Description Technique (FDT), does not have enough expressive power to describe timing behaviours of distributed or multimedia system. To address this limitation, we have developed Time-Estelle, an extended Estelle which is capable of doing so. Past techniques employed for verifying Estelle specifications have not considered time factors and were usually based on a variant or a subset of Estelle and all translating such specifications to another form, such as Finite State Machines or Petri Nets. This paper describes a method of verifying Time-Estelle specification using Communicating Time Petri Nets (CmTPNs).
展开▼
