Mahmoud Talebi, Jan Friso Groote, Conrad Dandelski: Modelling and Verification of a Cluster-tree Formation Protocol Implementation for the IEEE 802.15.4 TSCH MAC Operation Mode. MARS 2017: 117-128