Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks
Yati Phyo, Kazuhiro Ogata · 2018
We formally specify a mobile ad hoc network mutual exclusion protocol designed by Walter, Welch and Vaidya in Maude, a specification/programming language based on rewriting logic, and model check that the protocol enjoys the lockout freedom property. Matching equations that can be used as part of the condition of a conditional rewrite rule make it possible to concisely specify complex state transitions. The protocol needs to take into account link failures and/or recoveries, leading to a huge number of states even when there are a small number of nodes. We propose a technique to alleviate the situation, which is called a divide & conquer approach to leads-to model checking. We are interested in the lockout freedom property as one desired property for the protocol in this paper. The property can be expressed with the LTL leads-to connective.