Um verificador de modelos explícito-simbólico
Carregando...
Arquivos
Data
Autor(es)
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal de Minas Gerais
Descrição
Tipo
Tese de doutorado
Título alternativo
Primeiro orientador
Membros da banca
Claudionor Jose Nunes Coelho Junior
Newton Jose Vieira
Anamaria Martins Moreira
Arnaldo Vieira Moura
Newton Jose Vieira
Anamaria Martins Moreira
Arnaldo Vieira Moura
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.
Abstract
In this work we propose a modeling that combines explicit and symbolic representations in an explicit-symbolic formal verification model. Both explicit and symbolic models have been successfully used in the verification of finite state concurrent systems, such as complex sequential circuits and communication protocols. The proposed model aims to use explicit and symbolic techniques together to verify the same model and to make it possible to employ the most efficient technique to handle each aspect of the model. First, we give an overview of the process of model checking a system and discuss how temporal properties can be specified for a given model. The discussion is focused on computational tree logic,but we also consider linear temporal logic. Next, we present the explicit representation and its basic algorithms. The main techniques for improving explicit model checkers are presented, such as partial order reduction, bit-state hashing, minimized automata, compression of state vectors and static analysis. Also, we discuss the symbolic model checking and the binary decision diagrams. Fixpoint characterizations are given for the symbolic versions of the model checking algorithms. Then, we present the Interchange Format [Bozga et al., 1999] developed at Verimag labs, the description language of the combined explicit-symbolic model checker. At this point, we have presented the background for the introduction of the explicit-symbolic modeling. The conception of the combined explicitsymbolic model and related algorithms is the theoretical basis of our work. Descriptions in the Interchange Format are adapted to the theoretical modeling for the combined model. After that, we discuss the implementation of the explicit-symbolic model checker, discussing important data structures and the overall process, from the collection of symbols to the construction of the combined model. Finally, we show experimental results and suggest future work.
Assunto
Logica simbolica e matematica, Computação, Linguagem formal
Palavras-chave
Verificação de modelos