Verifying Estelle specifications: numerical Petri nets approach

Author

Jirachiefpattana, J. ; Lai, R.

Author_Institution

Dept. of Comput. Sci. & Comput. Eng., La Trobe Univ., Bundoora, Vic., Australia

fYear

1993

fDate

19-22 Oct 1993

Firstpage

334

Lastpage

341

Abstract

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

Keywords

Petri nets; finite state machines; formal verification; protocols; software tools; specification languages; Estelle specifications verification; Estelle verification tools; PROTEAN; automated verification tool; finite state machines; numerical Petri nets; Automata; Computer science; ISO standards; Logic; Petri nets; Protocols;

fLanguage

English

Publisher

ieee

Conference_Titel

Network Protocols, 1993. Proceedings., 1993 International Conference on

Conference_Location

San Francisco, CA

Print_ISBN

0-8186-3670-X

Type

conf

DOI

10.1109/ICNP.1993.340894

Filename

340894