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 state diagram of the Unified Modeling Language into a Petri nets model. On the basis of this transformation a verification of the dynamic model of the real system can be done. This means the evaluation of the completeness of the dynamic model and its consistency with the system requirements. It is also possible to solve the problem of concurrency and synchronization of the process in the system, as well as to optimize the dynamic model.