Scholarlink

It has recently been proposed to formally specify a team formation protocol (TFP) using TLA \(^+\) where no messages are lost. In this paper, we consider the TFP where some reply messages are either lost in transit or received after a predetermined amount of time. We suggest a TLA \(^+\) specification for the general TFP with message loss. To capture the semantics of loss of messages, we introduce a new action. The TLC model checker has verified the protocol’s correctness for various model sizes.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

TLA \(^+\) Based Specification and Verification of a Team Formation Protocol with Message Loss

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Rajdeep Niyogi

摘要

It has recently been proposed to formally specify a team formation protocol (TFP) using TLA \(^+\) where no messages are lost. In this paper, we consider the TFP where some reply messages are either lost in transit or received after a predetermined amount of time. We suggest a TLA \(^+\) specification for the general TFP with message loss. To capture the semantics of loss of messages, we introduce a new action. The TLC model checker has verified the protocol’s correctness for various model sizes.