Please use this identifier to cite or link to this item:
metadata.dc.type: Artigo de Periódico
Title: A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol
Other Titles: Electronic Notes in Theoretical Computer Science
Authors: Regnier, Paul Denis Etenne
Lima, George Marconi de Araújo
Andrade, Aline Maria Santos
metadata.dc.creator: Regnier, Paul Denis Etenne
Lima, George Marconi de Araújo
Andrade, Aline Maria Santos
Abstract: We describe the formal specification and verification of a new fault-tolerant real-time communication protocol, called DoRiS, which is designed for supporting distributed real-time systems that use a shared high-bandwidth medium. Since such a kind of protocol is reasonably complex and requires high levels of confidence on both timing and safety properties, formal methods are useful. Indeed, the design of DoRiS was strongly based on formal methods, where the TLA+ language and its associated model-checker TLC were the supporting design tool. The protocol conception was improved by using information provided by its formal specification and verification. In the end, a precise and highly reliable protocol description is provided.
Keywords: Formal Specification
Real-Time Protocol
Issue Date: 2009
Appears in Collections:Artigo Publicado em Periódico (IC)

Files in This Item:
File Description SizeFormat 
S1571066109001765-main.pdf321,7 kBAdobe PDFView/Open

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.