Wireless sensor networks consist of resource constrained nodes, especially with respect to power resources. In many cases, the replacement of a dead node is difficult and costly, e.g. an implanted node in the human body. Our main goal in this paper is reducing the total power consumption of the network. For this purpose, we consider the cooperation of nodes in data transmission in terms of a group, since the major consumer of power is the data transmission process. A mobile node may move to a new location, in which it is desirable for the node to join a group. In this paper, we propose an algorithm for nodes to choose the best group in their signal range, using coalitional game theory to determine what is beneficial in terms of power consumption. The protocol is formalized in rewriting logic, implemented in the Maude tool, and validated by means of Maude's model exploration facilities. Simulation-based tools are in general not able to prove the protocol. However, by using Maude, we prove the correctness of our proposed protocol, by searching for failures of the protocol, through all possible behaviors of sensors. These searches prove that grouping nodes is done correctly in all reachable states from a set of initial states of the model. In addition, we simulate our model in order to quantitatively analyze the efficiency of the proposed protocol. The results show significant improvements in power efficiency.