Resumo:
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.
