Please use this identifier to cite or link to this item: https://hdl.handle.net/10216/69405
Author(s): Valério Rosset
Pedro F. Souto
Francisco Vasques
Title: Formal verification of a group membership protocol using model checking
Issue Date: 2007
Abstract: The development of safety-critical embedded applications in domains such as automotive or avionics is an exceedingly challenging intellectual task. This task can, however, be significantly simplified through the use of middleware that offers specialized fault-tolerant services. This middleware must provide a high assurance level that it operates correctly. In this paper, we present a formal verification of a protocol for one such service, a Group Membership Service, using model checking. Through this verification we discovered that although the protocol specification is correct, a previously proposed implementation is not.
Subject: Ciências da computação e da informação
Computer and information sciences
Scientific areas: Ciências exactas e naturais::Ciências da computação e da informação
Natural sciences::Computer and information sciences
URI: https://repositorio-aberto.up.pt/handle/10216/69405
Source: ON THE MOVE TO MEANINGFUL INTERNET SYSTEMS 2007: COOPLS, DOA, ODBASE, GADA, AND IS, PT 1, PROCEEDINGS
Document Type: Artigo em Livro de Atas de Conferência Internacional
Rights: openAccess
License: https://creativecommons.org/licenses/by-nc/4.0/
Appears in Collections:FEUP - Artigo em Livro de Atas de Conferência Internacional

Files in This Item:
File Description SizeFormat 
59507.pdf254.08 kBAdobe PDFThumbnail
View/Open


This item is licensed under a Creative Commons License Creative Commons