Petri Nets are tools for the analysis and design of concurrent systems. There is a formal theory, which supports Petri Nets. We propose Petri Nets with Clocks which has a high expressive power in the concurrent and asynchronous process modeling and gives the possibility to model real time systems. The Petri Nets with Clocks are useful to model systems with temporal requirements via specification of clocks, using temporal invariants for the places and temporal conditions in the transitions. Also, we have developed an algorithm for the analysis of Petri Nets with Clocks. For the Business Processes Modeling, we propose to use Petri Nets with Clocks to formalize models, allowing to study the models through a quantitative and qualitative analysis. Petri Nets with Clocks includes additional temporal elements -clocks-, which are appropriate for the Business Processes Modeling and are not taken into consideration in the literature concerning the extensions of Petri Nets with time. Petri Nets with Clocks allows studying the structural properties of Business Processes Modeling. This study not only allows the simulation but also verifies formally the model. It is oriented to the verification and correction of errors in the modeling of the time variable en Business Processes.Eje: Ingeniería de softwareRed de Universidades con Carreras en Informática (RedUNCI)