Protocol verification is an integral part in Software development life cycle. It is important due to its ability to identify hidden

software bugs that remains uncovered during testing phase. The bugs that are covered during protocol verification include

deadlocks, livelocks,non progress cycles and other correctness properties. The protocols that run on constrained devices like smart

objects posses some specific behaviors that are different from non constrained devices. These behaviors include periodic message

broadcast, topology encoding, topology changes and timing elapsed between various events ,clock drift between nodes etc. The

verification of such protocols require effective abstraction mechanism to incorporate these behaviors. Various modeling languages and

tools are available in the literature that provide support in abstracting out the behavior of protocols. PROMELA is considered as an

effective language for modeling protocols due to its resemblance with block structured languages. However PROMELA language lack

standard constructs to depict these behaviors. This paper propose various methods to abstract behavioral patterns for IoT related

protocols with specific attention given for modeling periodical message broadcast,topology encoding and topology changes. By using

these proposed methods validation models are constructed using PROMELA for each behavior. Finally a validation model for a

hypothetical protocol that perform event propagation from a specific node to a collector node is derived. This protocol incorporate all

the proposed mechanism to demonstrate its applicability in modeling IoT protocols. Correctness properties are inserted into this model

using LTL formula. The verification of the model covering basic safety properties and the correctness properties are performed using

Spin model checker. The abstraction mechanism depicted in this paper can be utilized as a basis to build validation models for the