Ph.D. Thesis, Report LAAS--90113, pages 1-148 pp.. Toulouse, France: Centre National de la Recherche Scientifique, Lab. d'Automatique et d'Analyse des Systemes, 1990. In French.
Abstract: The Estelle formal description technique and the prototyping of an environment for the validation of protocols described with the aid of this technique are described. Based on previous works, a rendezvous mechanism is formally defined to bring Estelle closer to Petri nets, the latter being a modeling tool for which well proven validation techniques are available. The extension of these techniques to Estelle descriptions is carried out within the framework of the development of the ESTIM tool which offers simulation functionalities for interactive analysis as a protocol as well as verification functionalities for automatic generation of the quotient automaton, which characterizes the service provided by the protocol.
Keywords: protocol validation environment; Estelle; rendezvous mechanism; ESTIM protocol tool; tool which offers simulation functionalities for interactive.
Back to the Petri Nets Bibliography