A Formalization of the FIP Protocol Using Estelle

In this paper we report on an ongoing project aimed at using Estelle, a standard formal description technique for protocols and distributed systems, to formalize and analyze the FIP field-bus protocol. At present, only the formalization part of the task has been completed, so the paper focuses on this aspect. The formalization part in itself is interesting especially because it is a means to describe in a precise, clear and unambiguous way the protocol, thus avoiding misunderstandings. Moreover, it is a basis for automatic correctness verification, performance evaluation and rapid prototyping. The paper first recalls the key aspects of field-buses in general and FIP in particular, then introduces the basic features of the Estelle formal description technique, and illustrates the formal specification of FIP in Estelle.