Máquina de Estado Finito (MEF) é uma técnica de especificação usada para modelar o aspecto comportamental de sistemas e tem sido amplamente utilizada em diversas áreas de aplicação: protocolos de comunicação, telefonia, controle de processos, entre outros. O objetivo deste trabalho consiste em estudar os conceitos fundamentais utilizados no teste e validação de modelos baseados em MEF, com ênfase nos critérios DS [GONE70], UIO [SABN88], W [CHOW78] e Wp [FUJI91]. Dentro deste contexto foi desenvolvida tuna ferramenta, denominada MGASET, que visa a apoiar a aplicação de alguns critérios estudados, fornecendo facilidades para verificação de minimalidade, determinismo, especificação completa, conectividade forte, Máquina de Mealy e alcançabilidade do estado inicial de uma MEF; para gerar seqüência de sincronização, seqüência distingüivel, seqüências únicas de entrada/saída e conjunto de caracterizacão; e gerar, inicialmente, seqüências de teste baseada no critério W.

Finite State Machine (FSM) is an specification technique used to model the behavioral aspect of systems and has been widely used in many applications areas: communication protocols, telephony, process control and others. Testing and validation of systems specified using FSM have been the aim of many scientific works. The objective of this work consists in studying the fundamental concepts used in testing and validation of FSM based model, with emphasis in the DS [GONE70], UI° [SABN88], W [CHOW78] and Wp [FUJI91] criteria. Within of this context a tool, named MGASET, was developed that aims to support the application of the criteria studied, providing facilities to verification of minimality, detenninism, complete specification, strong conectivity, Mealy's Machine and reachability of initial state of a FSM; to generate synchronizing sequence, distinguishing sequence, unique input/ouput sequence and characterization set; and to generate, initially, test sequence based on W criteria.