Net Verifier of Discrete Event System models expressed by UML Activity Diagrams

In this paper the net verification method of discrete event-driven systems modeled by UML activity diagrams is proposed. Verification is made in a formal way using a suitable procedure called activity diagram to net verifier (in short: ADN-verifier). The ADN verifier operates in two steps: (1) conversion of given activity diagram (AD) into coloured Petri net (CPN), (2) dynamic properties analysis of CPN obtained by conversion. Examination of CPN properties, exploiting Petri net theory methods, enables us to draw conclusions about dynamic properties of the original activity diagram. It was shown, that, during the conversion process, using conversion rules, dynamic properties of the model are preserved. Completeness and independence of the rules were shown as well. The following fundamental properties were shown: (i) simulation of AD by CPN obtained by conversion, and (ii) detection in finite time of any structural incorrectness in AD model by application of ADN verifier. In the case of faulty behavior detection, the method was extended to identify incorrectness in the AD model under consideration. An example of ADN verification is given in the domain of modeling discrete production systems.