A modelação de software desempenha um papel importante na garantia da qualidade e confiabilidade de sistemas computacionais. Nesse contexto, a Unified Modeling Language (UML) e as redes de Petri são amplamente empregadas como ferramentas para representar e analisar sistemas complexos, visando validar a corretude dos diagramas. Este trabalho propõe a criação de regras para o mapeamento dos diagramas de casos de uso e sequência da UML 2.0 para redes de Petri seguras equivalentes. As regras são aplicadas na prática, mapeando diagramas de um artigo encontrado através de pesquisas, seguido pela análise formal das redes resultantes. Além disso, é realizado o mapeamento desses mesmos diagramas para redes de Petri coloridas com base em regras criadas por outros autores, bem como a análise formal desse mapeamento. Por fim, é realizada uma comparação entre as abordagens. Os resultados deste estudo fornecem uma base sólida para a compreensão e aprimoramento dos processos de mapeamento de diagramas da UML para redes de Petri seguras e coloridas, contribuindo para a validação e verificação eficaz de sistemas complexos de software.