No desenvolvimento de aplicações hipermídia, o projetista pode erroneamente inserir comportamentos indesejados. metodologias baseadas em teste ou análise de linha temporal para verificar a corretude de aplicações são limitadas, por não serem exaustivas e serem consumidoras de tempo. outra alternativa é a utilização de metodologias baseadas em verificação formal, que permitem uma análise exaustiva e mais rápida da aplicação. a verificação formal requer que a aplicação e os comportamentos a serem verificados estejam representados em linguagens formais, de difícil aprendizagem por um projetista de aplicação hipermídia. o presente trabalho propõe uma metodologia baseada no uso de verificação formal por model-checking, a partir de uma representação da aplicação, das propriedades a serem verificadas e do diagnostico de eventuais erros, ambos em linguagens e representações de fácil uso e entendimento para o projetista destas aplicações. essa metodologia é dividida em quatro fases: modelagem, transformação, verificação e diagnóstico/correção. inicialmente, o projetista codifica sua aplicação em alguma linguagem de domínio específico (por exemplo, ncl ou smil), e especifica os comportamentos desejados a serem verificados numa linguagem de descrição simples, proposta neste trabalho. a seguir, essas descrições das aplicações e comportamentos são transformadas, seguindo a abordagem mde (model driven engineering), nos modelos formais utilizados na verificação. em caso de algum comportamento desejado não ser satisfeito, a ferramenta de model-checking oferece um contraexemplo que, após transformação, é apresentado na forma de uma linha de tempo, permitindo diagnosticar a origem do erro e fornecer informações para a sua correção. para apoiar a metodologia proposta, foi construído um protótipo de um ambiente de desenvolvimento, no qual o projetista pode verificar o comportamento de sua aplicação. as avaliações da metodologia e de seu ambiente, realizadas em diversas aplicações hipermídia mostram suas potencialidades de uso para aplicações mais complexas e no caso de edição "ao vivo".