O uso de simuladores operacionais é fundamental importância para o programa espacial brasileiro. Durante a operação de um satélite, esses simuladores são essenciais para validação de manobras críticas, testes de novas versões do software de bordo e apoio ao diagnóstico de anomalias. Visando o reuso dos simuladores operacionais, o Instituto Nacional de Pesquisas Espaciais (INPE) tem adotado um novo padrão para descrição do comportamento dos subsistemas implementados em simuladores de satélites desenvolvidos pelo INPE, baseado em tabelas de causa e efeito. Neste contexto, este trabalho de pesquisa propõe um método de verificação de simulador de satélites que consiste na geração de um conjunto de casos de teste a partir da especificação em tabelas de causa e efeito. O método combina técnicas de model checking e model based testing, considerando em particular a metodologia Conformance and Fault Injection para geração dos casos de teste. Para avaliar o método proposto, este projeto considera a realização de experimento envolvendo conjunto de especialistas que aplicaram o método proposto para alguns casos de aplicação. Com base nos modelos gerados pelos especialistas, nos casos de teste obtidos a partir dos modelos e nos resultados da aplicação dos casos de teste, espera-se analisar a facilidade de uso do método proposto, assim como sua capacidade de guiar o especialista na elaboração de modelos consistentes com a especificação. Como principal contribuição desta pesquisa espera-se sistematizar o processo de verificação de simuladores operacionais de satélites adotado pelo INPE e assim, dar uma contribuição para o sucesso das missões espaciais brasileiras.