Um verificador de modelos explícito-simbólico

• Ano de defesa: 2005
• Autor(a) principal: Umberto Souza da Costa
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal de Minas Gerais; UFMG
• Palavras-chave em Português: Verificação de modelos; Logica simbolica e matematica; Computação; Linguagem formal
• Link de acesso: http://hdl.handle.net/1843/RVMR-6EAPMC

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.