UML MANUFACTURING SYSTEM MODEL ANALYSIS USING PETRI NETS

The net verification method of Discrete Event-Driven Systems modelled by UML activity diagrams is proposed. Verification is made in a formal way by suitable procedure called Activity Diagram to Net verifier (is short: ADN-verifier). First, conversion of activity diagrams (AD) into Coloured Petri net (CPN) is proposed. Next, dynamic properties of CPN are analysed, such as: rules independence, completeness, simulation of AD by CPN, detection of any structural incorrectness in AD model. The method was extended to identify incorrectness in the AD model. Application of ADN-verification method is presented by example from manufacturing systems domain.