@MASTERSTHESIS{ 2010:1896422654,
 	title = {Uma biblioteca de padr?es de especifica??o em Event-B para mecanismos de troca de mensagens em sistema distribu?dos},
 	year = {2010},
 	url = "http://tede2.pucrs.br/tede2/handle/tede/5197",
 	abstract = "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.",
 	publisher = {Pontif?cia Universidade Cat?lica do Rio Grande do Sul},
 	scholl = {Programa de P?s-Gradua??o em Ci?ncia da Computa??o},
 	note = {Faculdade de Inform?ca}
}