Verifying correctness of interfaces of design models of manufacturing systems using functional abstractions

In this paper, we introduce descriptions of selected primary components of automated guided vehicle (AGV)-based flexible manufacturing systems. These descriptions represent invariant structural and functional properties expressed at a certain level of abstraction of components such as machining stations and load and unload stations. To model these objects, a class of Petri nets is adopted and briefly introduced in the paper. This class allows for representing the unidirectional flow of physical resources and control information/data, which is characteristic of the primary components. The issue of the verification of the interconnections or interfaces among the Petri nets of primary components is addressed by the introduction of functional abstractions of the Petri net models of these components. In this paper we demonstrate the usefulness of functional abstractions in verification of the correctness of the interconnections among objects. In doing so, a simple manufacturing system is adopted