In the software engineering world, modeling has a rich tradition, dating back to the earliest days of programming. The most recent innovations have focused on notations and tools that allow users to express system perspectives of value to software architects and developers in ways that are readily mapped into the programming language code that can be compiled for a particular operating system platform. The current state of this practice employs the Unified Modeling Language (UML) as the primary modeling notation. The UML allows development teams to capture a variety of important characteristics of a system in corresponding models. Transformations among these models are primarily manual. However, potential faults that violate desired properties of the software system might still be introduced during the process. Verification technique is well-known for its ability to assure the correctness of models and uncover design problems before implementation. This paper presents a set of rules that allows Software engineers to transform the behavior described by a UML 2.0 Activity Diagram (AD) into a Petri Net (PN). The main purpose of the transformation to Petri nets is to use the theoretical results in the Petri nets domain to analyze the equivalent Petri nets and infer properties of the original workflow. Furthermore, we implement a tool to support the transformation process.