O uso de técnicas formais de teste de software tem se mostrado um bom mecanismo para revelar a presença de falhas de software. Uma das técnicas mais utilizadas é o Teste Baseado em Máquinas de Estados Finitos, uma técnica de teste funcional, suportada pela criaçã e uso de um modelo que descreve o comportamento do sistema sob teste. A partir deste modelo, os casos de teste podem ser gerados e executados, e os resultados dessa exacuçã avaliados. Este artigo apresenta uma revisão desta técnica de teste, apresentando suas principais características, vantagens e desvantagens –enfocando os principais criterios de teste definidos para ela. Além disso, também são apresentadas algumas ferramentas utilizadas para a automação dos testes por meio dessa técnica e a aplicação de parte desta técnica por meio de um estudo de caso.