Verification and validation of UML 2.0 sequence diagrams using colored Petri nets

One of the major challenges in the software development process is the improvement of the error detection in the early phases of the software life cycle. If the software error is detected at the design phase before of the implementation, the software quality will acceptably be increased. For this purpose, the Verification and Validation of UML diagrams play a very important role in detecting flaws at the design phase. This paper presents a Verification and Validation technique for one of the most popular UML diagrams: sequence diagrams. The proposed approach creates an executable model from UML interactions expressed in sequence diagrams using colored petri nets and uses CPN Tools to simulate the execution and to verify properties written in standard ML. In The proposed approach, we have used the sequence diagram elements including massages, send/receive events and source/destination of messages and have written properties in terms of boolean expression over the elements. The main contribution of this work is to provide an efficient mechanism to be able to track the execution state of an interaction in sequence diagram. The obtained results show that The proposed approach reduces impressively the probability of errors appearance at the software implementation phase. therefore, sofware can be more reliable at the end of the software development process.