Especifica o e Verifica o Formal de um modelo de STI-PBL por Redes de Petri Coloridas

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.