Incremental modeling based on pneumatic equipment plans and sequential function charts

The paper presents an approach to obtain a closed-loop model of controlled manufacturing systems. The major obstacle in applying such models to formal verification of real systems is the effort that is needed to design a formal model of the plant behavior. We show in this contribution how a semi-formal description of the plant, called pneumatic equipment plan, can be used to reduce the effort to design a formal plant model and therefore narrow the gap between formal verification and its practical applicability