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.

Made available in DSpace on 2014-12-17T15:47:48Z (GMT). No. of bitstreams: 1 ClaudiaFCKT.pdf: 525104 bytes, checksum: 174fb60f1cf9ebfc609d837f2787b6b1 (MD5) Previous issue date: 2007-07-27 / Este trabalho apresenta uma extens?o do provador haRVey destinada ? verifica??o de obriga??es de prova originadas de acordo com o m?todo B. O m?todo B de desenvolvimento de software abrange as fases de especifica??o, projeto e implementa??o do ciclo de vida do software. No contexto da verifica??o, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte ? checagem satisfatibilidade de f?rmulas da teoria axiom?tica dos conjuntos, ou seja, podem ser aplicadas ao m?todo B. A checagem de SMT consiste na checagem de satisfatibilidade de f?rmulas da l?gica de primeira-ordem livre de quantificadores dada uma teoria decid?vel. A abordagem de checagem de SMT implementada pelo provador autom?tico de teoremas haRVey ? apresentada, adotando-se a teoria dos vetores que n?o permite expressar todas as constru??es necess?rias ?s especifica??es baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-G?del (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias n?odecid?veis, a teoria NBG apresenta-se como uma op??o adequada para a expans?o da capacidade dedutiva do haRVey ? teoria dos conjuntos. Assim, atrav?s do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao m?todo B