No desenvolvimento orientado a modelos, casos de teste para validar sistemas podem ser gerados a partir de um modelo que representa como o sistema deve se comportar. Por exemplo, se os serviços a serem oferecidos pelo sistema são descritos em modelos de Statecharts, é possível gerar automaticamente casos de teste para programas a partir de tais modelos. Entretanto, propriedades a serem provadas não são geradas a partir desses modelos. Em geral, desenvolvedores recebem a especificação do sistema e observam suas restrições para então definir quais propriedades devem ser satisfeitas. Este projeto propõe um estudo de um conjunto de casos de teste gerados de especificações para guiar a definição de propriedades. Primeiramente, uma técnica para geração automática de casos de teste a partir de statecharts é apresentada. Então, todos os casos de teste são observados e uma técninca para gerar as propriedades a partir dos testes adquiridos é proposta.