Apresenta-se neste trabalho uma abordagem de modelagem por Redes de Petri Coloridas para especificação e verificação formal de um modelo de Sistema Tutor Inteligente que utiliza a
Aprendizagem Baseada em Problemas como estratégia pedagógica. A especificação e a verificação formal permitem verificar se as funcionalidades planejadas do modelo pedagógico são realizadas, antes da etapa de implementação do sistema. Experimentos indicam consistência geral e benefícios da proposta.