O objetivo deste trabalho é prover métodos eficientes de geração de casos de teste para sistemas reativos críticos. Sistemas dessa natureza compreendem sistemas de tempo real e com transformações de contexto. Uma das técnicas mais usadas na geração de conjuntos de teste tem sido a abordagem baseada em modelos formais. Neste caso, os formalismos fornecem uma base sólida para que a atividade de teste seja efetuada de forma precisa e segura.

Este trabalho propõe a construção de modelos formais, métodos e técnicas, bem como estratégias de teste, para dar suporte ao processo de geração automática de conjuntos de teste, aplicáveis a sistemas complexos. Porém, o processo de geração de testes baseado em modelos se torna, muitas vezes, impraticável em aplicações reais, devido ao problema da explosão combinatória de estados. Daí a necessidade de se encontrar modelos adequados que capturem o comportamento desejado dos sistemas a serem testados, bem como a importância  de se construir métodos que contornem o problema da explosão do espaço de estado, de maneira razoável, permitindo que a geração de testes seja um processo aplicável a sistemas complexos.

Entre os modelos abordados neste trabalho estão: (i) as tradicionais Máquinas de Estados Finito (FSM); (ii) uma extensão das FSM usando variáveis de contexto, as Máquinas de Estados Finito Estendida (EFSM); (iii) a extensão temporizada de EFSM (TEFSM), que possui, não apenas variáveis de contexto, mas também variáveis relógio; (iv) os modelos temporizados com entradas e saídas independentes, conhecidos como Timed I/O Automata (TIOA); e (v) uma extensão proposta para TIOA, denominado Timed I/O Context Automata (TIOCA), para compreender a evolução contínua de tempo e também as transformações de contexto.

Com relação a geração de testes baseada em tais modelos, foi proposto, primeiramente, uma técnica de derivação de sequências de confirmação para TEFSM, usando model-checking. Em seguida, foi proposta uma generalização para um método de geração de conjuntos completos de teste usando FSM. Também foi desenvolvido um novo método de discretização do modelo TIOA, provendo a base necessária para a geração de casos de teste usando os conceitos de proposta de teste e produto síncrono. Por fim, foi desenvolvida uma extensão do método de discretização para TIOA também proposto neste trabalho, aplicado ao modelo TIOCA, permitindo a geração de testes em sistemas com evolução contínua de tempo e fluxo de dados, usando os conceitos de proposta de teste e produto de TIOCA.