The use of generic models in the synthesis of FMS systems, whichallows for rapid modelling and analysis, does not ease the verificationtask difficulty. Even though generic modules can be verified separately,the verification of the interconnections between modules requires thewhole model to be considered. A potential solution is to replace thegeneric modules with their functional abstractions which realise theexternal functional behaviour of these modules. The number of places andtransitions involved in realizing the required functionality is,typically, a fraction of that used to represent complete components.This reduces the complexity of the components of the modelled system,and thus the complexity of the verification model. The verification taskcan then focus on the correctness of the interfaces, rather then on theinternal nature of the components. In this paper, for a class of Petrinet models, which can be used to represent the primary components of theAGV based FMS systems, a method that allows one to systematicallyconstruct functional abstractions is presented
展开▼
