Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-02-22T21:43:01Z
No. of bitstreams: 1
PauloEwertonGomesFragoso_DISSERT.pdf: 1631728 bytes, checksum: 56a10da50e4f607b55bac9c065912a21 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-02-23T23:34:33Z (GMT) No. of bitstreams: 1
PauloEwertonGomesFragoso_DISSERT.pdf: 1631728 bytes, checksum: 56a10da50e4f607b55bac9c065912a21 (MD5) / Made available in DSpace on 2016-02-23T23:34:33Z (GMT). No. of bitstreams: 1
PauloEwertonGomesFragoso_DISSERT.pdf: 1631728 bytes, checksum: 56a10da50e4f607b55bac9c065912a21 (MD5)
Previous issue date: 2015-03-09 / Event-B ? um m?todo formal de modelagem e verifica??o de sistemas de transi??o discretos.
O desenvolvimento com Event-B produz obriga??es de prova que devem ser verificadas,
isto ?, ter sua validade verificada para manter a consist?ncia dos modelos produzidos.
Solucionadores de Satisfatibilidade M?dulo Teoria s?o provadores autom?ticos de teoremas
usados para verificar a satisfatibilidade de f?rmulas l?gicas considerando uma teoria
(ou combina??o de teorias) subjacente. Solucionadores SMT n?o apenas lidam com f?rmulas
extensas em l?gica de primeira ordem, como tamb?m podem gerar modelos e provas,
bem como identificar subconjuntos insatisfat?veis de hip?teses (n?cleos insatisfat?veis). O
suporte ferramental para Event-B ? provido pela Plataforma Rodin: um IDE extens?vel,
baseado no framework Eclipse, que combina funcionalidades de modelagem e prova. Um
plug-in SMT para Rodin tem sido desenvolvido com o objetivo de integrar ? plataforma
t?cnicas alternativas e eficientes de verifica??o. Neste trabalho foi implementada uma s?rie
de complementos ao plug-in para solucionadores SMT em Rodin, a saber, melhorias na
interface do usu?rio para quando obriga??es de prova s?o reportadas como inv?lidas pelo
plug-in. Adicionalmente, algumas caracter?sticas do plug-in, tais como suporte ? gera??o
de provas e extra??o de n?cleo insatisfat?vel, foram modificadas de modo a tornaremse
compat?veis com o padr?o SMT-LIB para solucionadores SMT. Realizaram-se testes
utilizando obriga??es de prova aplic?veis para demonstrar as novas funcionalidades. As
contribui??es descritas podem, potencialmente, afetar a produtividade de forma positiva. / Event-B is a formal method for modeling and verification of discrete transition systems.
Event-B development yields proof obligations that must be verified (i.e. proved valid) in
order to keep the produced models consistent. Satisfiability Modulo Theory solvers are
automated theorem provers used to verify the satisfiability of logic formulas considering a
background theory (or combination of theories). SMT solvers not only handle large firstorder
formulas, but can also generate models and proofs, as well as identify unsatisfiable
subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin
platform: an extensible Eclipse based IDE that combines modeling and proving features.
A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient
verification techniques to the platform. We implemented a series of complements to the
SMT solver plug-in for Rodin, namely improvements to the user interface for when proof
obligations are reported as invalid by the plug-in. Additionally, we modified some of the
plug-in features, such as support for proof generation and unsat-core extraction, to comply
with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof
obligations to demonstrate the new features. The contributions described can potentially
affect productivity in a positive manner.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/19825 |
| Date | 09 March 2015 |
| Creators | Fragoso, Paulo Ewerton Gomes |
| Contributors | 00809085437, http://lattes.cnpq.br/2985658685449858, Gomes, Bruno Emerson Gurgel, 01061676420, http://lattes.cnpq.br/7812661521592212, Oliveira, Marcel Vin?cius Medeiros, 02386943488, http://lattes.cnpq.br/1756952696097255, Bonichon, Richard Walter Alain, 70552758493, Deharbe, David Boris Paul |
| Publisher | Universidade Federal do Rio Grande do Norte, PROGRAMA DE P?S-GRADUA??O EM SISTEMAS E COMPUTA??O, UFRN, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0048 seconds