| 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 cadaaspecto 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, automatosminimizados, 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çãodo 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.
|
|---|