This paper describes a possible application of the Petri nets to specify the dynamics of information systems. The Petri nets are a mathematical tool allowing formal specification of the system dynamics. A formal procedure is proposed for transforming the activity diagram of the Unified Modeling Language into a Petri nets model. On the basis of this transformation it is possible to accomplish verification of the dynamic model of the real system, i.e. to evaluate whether the activities and their order are well defined. It is also possible to solve the problem of concurrency and synchronization of the activities in the system, as well as to optimize the dynamic model.