Tamanho da fonte: 

Os produtos de software e hardware desenvolvidos atualmente envolvem alto nível de complexidade. A abordagem tradicional para verificação envolve realizar testes e simulações. Contudo tais abordagens não exploram todo o universo de possíveis estados do sistema e assim não são apropriadas para garantir que um produto de software ou hardware é isento de erros. Técnicas de métodos formais como verificação de modelos têm sido largamente usadas e bem aceitas na indústria e na academia e podem ser utilizadas em complemento a essa abordagem tradicional. A busca por produtos de software e hardware com qualidade tem motivado o uso dessas técnicas formais, principalmente porque testar programas concorrentes não é uma tarefa trivial e é suscetível a erros. Verificação de modelos é o problema de testar automaticamente e exaustivamente se um modelo que representa um sistema atende a uma dada especificação e pode ser aplicada a sistemas modelados em diagramas de estados finitos, tais como sistemas de hardware embarcados que implementam funções veiculares. O objetivo deste projeto de iniciação científica foi o estudo e a aplicação da técnica de verificação de modelos em funções veiculares modeladas em estados finitos. Para aplicação da técnica de verificação de modelo são necessárias 3 etapas: modelagem, especificação e verificação. Na modelagem faz-se a descrição das características e comportamentos do sistema a ser analisado em uma linguagem. Na especificação faz-se a descrição das propriedades do sistema a serem verificadas e na verificação é executado um procedimento de verificação com a finalidade de determinar se as propriedades são mantidas no modelo. Para realizar a verificação de modelos utilizou-se o produto de software denominado NuSMV e na etapa de modelagem a linguagem SMV, a qual é entendida pela ferramenta NuSMV.  Na etapa de especificação utiliza-se lógica temporal (CTL). O projeto encontra-se em fase de finalização e como resultados parciais temos a aplicação da técnica de verificação de modelos nas funções veiculares analisadas e a capacitação de recurso humano na área de métodos formais, especificamente na técnica verificação de modelos.