Somayeh Azizi - sama technical and vocational training college. Islamic Azad University, Arak Branch, Arak, Iran
Naser Nematbakhsh - Computer science department, Islamic Azad University, Najafabad Branch, Najafabad, Iran

Verification and validation of the systems modeled by formal methods is carried out through either theorem proving method or automated method. Since theorem proving method requires the user's intervention, it is difficult. In this article, the verification and validation is conducted by the model checker and automatically. For this purpose, it is possible to convert the modelled systems into transition systems and then give them to a model checker like GROOVE as inputs so that they are verified and validated. This is basically done by modelling activity diagrams through a graph transformation system and an abstract state machine (ASM). The formal description of these systems is based on token movement in Unified Modelling Language Version 2 (UML2.0) activity diagram control nodes. In this paper we present an original method of analysis the UML2.0 activity diagrams. Our analysis method builds on our formal interpretation of these diagrams with respect to the UML2.0 standard.Graphs and diagrams provide a simple and powerful approach variety of problems that are typical to computerscience, for example for activities. Models based on these notation can be seen a graph and graph transformation are involved.Formal methods specifically in the research community to improve the reliability of software used in its onstruction. In this way the software requirements specifications using mathematical tools and languages have gradually been obtained and stored

Formal Methods, verification, validation, GROOVE, Reliability