Verifying Estelle specifications: numerical Petri nets approach

The techniques for verifying protocols specified in Estelle have so far focused on translating the specifications into another form, such as finite state machines or Petri nets, for which tools of verification have already been implemented. All the Estelle verification tools impose some restrictions on the specifications to be verified: the techniques use a subset of Estelle or restrict the complexity of the specifications that can be verified; or the specifications need to be specified in a variant of Estelle, rather than standardized Estelle. In particular, the dynamic behaviors of Estelle are not handled. This paper describes the verification of Estelle specifications by translating them into those of numerical Petri nets, which can then be verified by a proven automated verification tool, PROTEAN