Submitted by Alice Araujo (alice.caraujo@ufpe.br) on 2017-11-30T19:32:07Z No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) dissertacao-mestrado.pdf: 1137883 bytes, checksum: 9a8f7f4770dbbe3447440be8dc484c65 (MD5) / Made available in DSpace on 2017-11-30T19:32:07Z (GMT). No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) dissertacao-mestrado.pdf: 1137883 bytes, checksum: 9a8f7f4770dbbe3447440be8dc484c65 (MD5) Previous issue date: 2016-09-15 / FACEPE / Testes constituem uma parcela significativa da energia despendida em projetos voltados ao desenvolvimento de software. Estima-se que entre 30% a 50% do custo total do projeto é destinado a testes. Esta necessidade de verificar a regularidade de sistemas é bastante antiga e nos últimos anos a busca por novas técnicas e ferramentas que mitiguem o esforço gasto nestas verificações vem se acentuando. Neste contexto, uma técnica que se destaca é a de verificação de modelos (Model checking) que consiste em explorar exaustivamente todos os estados alcançáveis de um determinado sistema no intuito de descrever cenários que indiquem possíveis comportamentos, embasando tal verificação em matemática precisa e inequívoca. Esta técnica tem despertado o interesse de muitas indústrias devido ao sucesso obtido pelo apoio das ferramentas de verificação de modelos (model checkers) em vários projetos de alta complexidade. Estes verificadores são ferramentas que exploram um sistema de transições rotuladas (LTS), construído a partir de algumas especificações (um modelo M), para determinar se uma dada fórmula (f) em lógica temporal, ou propriedade, é válida; ou simplesmente, M |ù f. O presente trabalho apresenta uma forma sistemática de construir um verificador de modelos LTL para um subconjunto da linguagem Circus totalmente baseado na semântica operacional desta linguagem. Mas em vez de codificar diretamente o verificador de modelos em alguma linguagem de programação, é usado o framework K por se tratar de um framework semântico executável à base de reescrita em que as linguagens de programação, sistemas de tipos e ferramentas de análise formais podem ser definidos usando configurações, computações e regras. Além disso, a ferramenta resultante deste trabalho é demostrada com alguns estudos de caso no intuito de comparar seu desempenho bem como aspectos qualitativos com outros verificadores de modelos. / Tests constitute a significant portion of the energy expended in projects aimed at software development. It is estimated that between 30% and 50% of the total project cost is spent in testing. This need to verify the correctness of systems is quite old and in recent years the search for new techniques and tools to mitigate the effort spent on these checks has been increasing. In this context, a technique that stands out is Model Checking. This technique consists in exhaustively exploring all reachable states of a given system in order to check whether a given property, usually given in terms of some temporal logics, is valid. Several industries are interested in this technique due to the success achieved by the support of model checking tools (Model checkers) in various projects of high complexity. This paper presents a systematic way to build a LTL model checker for a subset the Circus language using its operational semantics. But instead of directly encoding the semantics using a programming language, we use the K framework because it is an executable semantic framework based on rewrite rules. Moreover, the resulting tool is exercised with few case studies in order to compare their performance as well as qualitative aspects with other model checkers.