Um verificador de modelos explícito-simbólico

AUTOR(ES)

Umberto Souza da Costa

DATA DE PUBLICAÇÃO

2005

RESUMO

Neste trabalho, propomos uma modelagem que combina representações explícitas e simbólicas em um modelo de verificação formal explícito-simbólico. Os modelos explícitos e simbólicos têm sido usados com sucesso na verificação de sistemas concorrentes de estados finitos, como circuitos sequenciais complexos e protocolos de comunicação. A modelagem proposta tem como objetivo combinar as técnicas explícitas e simbólicas para verificação de um mesmo modelo e permitir o emprego da técnica mais eficiente à verificação de cada aspecto do modelo. Inicialmente, apresentamos uma visão geral do processo de verificação do modelo de um sistema e discutimos como propriedades temporais podem ser especificadas para este modelo. A discussão é focalizada em lógica temporal CTL, mas também consideramos a lógica temporal LTL. Em seguida, introduzimos os modelos explícitos e seus algoritmos básicos. As principais técnicas de refinamento dos verificadores de modelos explícitos são apresentados, tais como redução de ordem parcial, bit-state hashing, automatos minimizados, compressão de vetores de estados e análise estática. Discutimos, também, a verificação de modelos simbólicos e os diagramas de decisão binária. Caracterizações em ponto fixo são dadas para as versões simbólicas dos algoritmos de verificação de modelos. Apresentamos a linguagem de descrição do verificador de modelos explícito-simbólico, o Interchange Format [Bozga et al., 1999] desenvolvido nos laboratórios Verimag. Com isso, concluímos a apresentação dos conceitos básicos necessários à introdução da modelagem explícito-simbólica. A concepção do modelo combinado explícito-simbólico e algoritmos relacionados é a base teórica de nosso trabalho. Adaptamos descrições em Interchange Format à modelagem teórica do modelo combinado. Após isso, discutimos a implementação do verificador de modelos explícito-simbólico, trazendo informações sobre suas estruturas de dados mais importantes e o processo geral de verificação, desde a coleta de símbolos até a construção do modelo combinado. Finalmente, mostramos resultados experimentais e sugerimos trabalhos futuros.

ASSUNTO(S)

logica simbolica e matematica teses. computação teses. linguagem formal teses.

Documentos Relacionados

• Um Verificador seguro de integridade de arquivos
• Mercado Simbólico: um modelo de comunicação para políticas públicas
• Violência: um gozo não balizado pelo simbólico.
• O ensino explícito da compreensão da leitura. Análise do impacto de um programa de intervenção
• Influências de um ensino explícito de argumentação no desenvolvimento dos conhecimentos docentes de licenciandos em Química