loading page

Formal specification and verification of a team formation protocol using TLA
  • Rajdeep Niyogi,
  • Amar Nath
Rajdeep Niyogi
Indian Institute of Technology Roorkee

Corresponding Author:[email protected]

Author Profile
Amar Nath
Sant Longowal Institute of Engineering and Technology
Author Profile

Abstract

Team formation in an environment where some relevant parameters are not known in advance is a challenging problem. Communicating automata and distributed algorithms have been used to describe protocols for team formation. A high-level specification provides a mathematical description of a protocol or a program. TLA + is a formal specification language designed to provide high-level specifications of concurrent and distributed systems. The associated model checker known as TLC is capable of model checking the TLA + specifications. Recently formal specification of a team formation protocol is given using TLA + when there is a single initiator (an agent or a robot), that initiates the team formation. Using TLA +, we examine the formal specification for the multiple initiator situation and demonstrate that a composition technique can yield a single monolithic specification for the multiple initiator situation from the single initiator situation specification. We have used models of varying sizes, and the TLC model checker has confirmed that the protocol’s specifications meet certain desired characteristics in each case.
14 Mar 2023Submitted to Software: Practice and Experience
14 Mar 2023Submission Checks Completed
14 Mar 2023Assigned to Editor
17 Mar 2023Review(s) Completed, Editorial Evaluation Pending
19 Mar 2023Reviewer(s) Assigned
24 Jun 2023Editorial Decision: Revise Major
29 Aug 20231st Revision Received
29 Aug 2023Assigned to Editor
29 Aug 2023Submission Checks Completed
29 Aug 2023Review(s) Completed, Editorial Evaluation Pending
06 Sep 2023Reviewer(s) Assigned
26 Sep 2023Editorial Decision: Revise Minor
30 Sep 20232nd Revision Received
30 Sep 2023Submission Checks Completed
30 Sep 2023Assigned to Editor
30 Sep 2023Review(s) Completed, Editorial Evaluation Pending
11 Nov 2023Reviewer(s) Assigned
21 Nov 2023Editorial Decision: Revise Minor