Abstract

Formal Description Technics (FDT) provide features like automatic implementation, automatic testpattern generation, verification and validation. In the fieldbus domain (e.g. PROFIBUS [DIN91], FIP [FIP88]) Estelle [ISO9074] is typically used for protocol specification. An Estelle (Extended State Transition Language) specification describes extended finite state machines, which communicate by FIFO buffers.

Petri nets are an other formalism especially for modelling and analysing concurrent systems. The concept is very simple. The basic element are places (which hold state information in form of tokens), transition (which play the active part and possible change system state) and arcs which link both together [Jensen92], [Fengler91].

Several researchers developed compilers to convert formal descriptions into Pascal, C or C++. On the other side semiconductor industry produces specialized controllers (e.g. for PROFIBUS [Lange95]) to realize optimized layer-two (data-link-layer) services. Because of the high performance requirements different data-link-layers appear very specific on different platforms (8051-Microcontroller, Motorolas 68302, or a simple USART). Therefore it is mostly not easy to connect them automatically with generated "'formal"' C or C++ code.

If we want to reuse high level formal specifications on different platforms. Or if we want to run on a different application-layer (fieldbus-specs using only layer 7,2 and 1) we need a well defined Communication Abstraction Interface. This interface hides the optimized and platform specific hard- and software implementations from the automatic generated Code. It defines a abstract set of classes and methods. If we define this set of classes we will be able to bring formal specifications from a simulation and verification platform to different implementation platforms without handy modifications.