Este trabalho apresenta uma nova abordagem para a modelagem da dinâmica de sistemas computacionais orientados a objetos. Ao invés de empregar diagramas de transição de estados para descrever os modelos de estados de cada classe, como faz a UML, esta abordagem propõe o emprego de redes de Petri Predicado/Transição. Analisando a interação entre objetos de classes diferentes pode-se integrar as redes de Petri de cada classe a fim de obter-se uma única rede de Petri Predicado/Transição que descreve o modelo de estados global para o sistema. A principal vantagem de se utilizar uma notação formal para modelar a dinâmica de um sistema é a possibilidade de aplicar técnicas de análise formal com o intuito de validar propriedades do sistema.