Please use this identifier to cite or link to this item:
https://repositorio.ufba.br/handle/ri/5258
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 Verification TLA+ Real-Time Protocol |
URI: | http://www.repositorio.ufba.br/ri/handle/ri/5258 |
Issue Date: | 2009 |
Appears in Collections: | Artigo Publicado em Periódico (IC) |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
S1571066109001765-main.pdf | 321,7 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.