A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol

2Citations
Citations of this article
13Readers
Mendeley users who have this article in their library.

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. © 2009 Elsevier B.V. All rights reserved.

Cite

CITATION STYLE

APA

Regnier, P., Lima, G., & Andrade, A. (2009). A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol. Electronic Notes in Theoretical Computer Science, 240(C), 221–238. https://doi.org/10.1016/j.entcs.2009.05.054

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free