关键词: BRP TLA＋ ABP规约 验证 模型检验

Abstract:

The Bounded Retransmission Protocol（BRP） is an industrial protocol designed for the transfer of large data files over unreliable communication lines . The protocol relies on specific assumptions on the timed behaviours of its components. This paper describes our experiences with specifying and verifying BRP using TLA＋. First,we give an informal natural-language description about the main principles and requirements of BRP. Then a model is built bas sed on this. Using TLA＋,we specify the untimed BRP first, and then complete the whole specification by adding real-time constraints. Finally, the propeerties of BRP are verified by the model checker TLC.

Key words: BRP;TLA＋, ABP, specification, verification, model checking