Made available in DSpace on 2015-04-14T14:49:55Z (GMT). No. of bitstreams: 1
444044.pdf: 1517934 bytes, checksum: 017ad238277ccab4a746e7590ed0bade (MD5)
Previous issue date: 2010-03-19 / The development of distributed systems and communication protocols is not a trivial task and the use of formal specification and verification techniques becomes necessary to assure the correctness of such systems. While model-checking techniques face the state space explosion problem, the use of theorem provers is an important resource for verification of systems with unlimited number of states. The formal method Event-B, increasingly being used in both industry and academia, is based on the technique of theorem proving and also supports refinement. The contribution of this work is a library of reusable formal specification patterns, in Event-B, for message passing mechanisms commonly employed in distributed systems. A specification pattern defines the desired communication semantics of a channel, having its properties formally proven. During the development of a distributed system, the developer may use these patterns by applying guided refinement steps on the target model. The resulting system is assured to have the communication semantics as defined by the pattern, thus freeing the developer of defining the communication system from scratch and of proving its properties. / O desenvolvimento de sistemas distribu?dos e protocolos de comunica??o ? uma tarefa complexa e o uso de t?cnicas de especifica??o e verifica??o formal torna-se necess?rio para garantir a corretude de tais sistemas. Enquanto t?cnicas de model-checking passam pelo problema da explos?o do espa?o de estados, o uso de provadores de teoremas representa um importante recurso para verifica??o de sistemas com ilimitado n?mero estados. O m?todo formal Event-B, de uso crescente na ind?stria e academia, se ap?ia na t?cnica de prova de teoremas e suporta refinamento. A contribui??o deste trabalho est? em proporcionar uma biblioteca reus?vel de padr?es de especifica??o, em Event-B, de mecanismos de troca de mensagens em sistemas distribu?dos. Um padr?o de especifica??o define a sem?ntica de comunica??o desejada em um canal, demostrando formalmente suas propriedades. Durante o desenvolvimento de um sistema distribu?do, o desenvolvedor pode fazer uso destes padr?es atrav?s de passos guiados de refinamento do sistema. O sistema resultante garante a semantica de comunica??o definida no padr?o utilizado e livra o desenvolvedor de se preocupar em definir o sistema de comunica??o a partir do in?cio e provar suas propriedades.
| Identifer | oai:union.ndltd.org:IBICT/oai:tede2.pucrs.br:tede/5197 |
| Date | 19 March 2010 |
| Creators | Pivetta, Paulo Junior Penna |
| Contributors | Dotti, Fernando Lu?s |
| Publisher | Pontif?cia Universidade Cat?lica do Rio Grande do Sul, Programa de P?s-Gradua??o em Ci?ncia da Computa??o, PUCRS, BR, Faculdade de Inform?ca |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da PUC_RS, instname:Pontifícia Universidade Católica do Rio Grande do Sul, instacron:PUC_RS |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | 1974996533081274470, 500, 600, 1946639708616176246 |
Page generated in 0.002 seconds