Por favor, use este identificador para citar o enlazar este ítem:
https://repositorio.ufba.br/handle/ri/5258
metadata.dc.type: | Artigo de Periódico |
Título : | A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol |
Otros títulos : | Electronic Notes in Theoretical Computer Science |
Autor : | 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 |
Resumen : | 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. |
Palabras clave : | Formal Specification Verification TLA+ Real-Time Protocol |
URI : | http://www.repositorio.ufba.br/ri/handle/ri/5258 |
Fecha de publicación : | 2009 |
Aparece en las colecciones: | Artigo Publicado em Periódico (IC) |
Ficheros en este ítem:
Fichero | Descripción | Tamaño | Formato | |
---|---|---|---|---|
S1571066109001765-main.pdf | 321,7 kB | Adobe PDF | Visualizar/Abrir |
Los ítems de DSpace están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.