Formal Modeling and Quantitative eva‎luation of IoT Quality Attributes Based on Stochastic Petri Nets

1/20/2026 12:00:00 AM

Today, Internet of Things (IoT) systems have numerous applications across different fields. As a result, eva‎luating their quality of service is particularly significant. Up to this point, various modeling and eva‎luation methods have been proposed. However, IoT systems possess unique characteristics that are complex and, in some instances, cannot be effectively modeled using existing methods. These characteristics include reliance on energy sources, mobility, concurrency, and interaction. Hence, the primary motivation behind this research was to introduce an appropriate formal modeling method for these systems that incorporates specific initial concepts aligned with the aforementioned features, while also allowing for a quantitative eva‎luation of qualitative attributes. The primary aim of this research was to deliver formal methods for modeling and quantitative eva‎luation of Internet of Things systems utilizing stochastic Petri nets (SPNs). To accomplish this objective, the initial step involved studying and identifying the characteristics of these systems and the challenges associated with modeling in this domain. In the second step, formal models were proposed, with each model specifically addressing one of the modeling challenges in this area. The third step presented modeling and eva‎luation methods and tools based on the proposed models. Ultimately, these models and software tools were applied in case studies within the Internet of Things field. In this thesis, stochastic reward networks (SRNs), which are an extension of the stochastic Petri net, are utilized as the primary formal model. Two formal models, abbreviated as SB-SRN and MSRN, have been proposed to address the challenges of energy resources and mobility, respectively. Subsequently, a final model referred to as MPSRN has been introduced, which integrates all the challenges in this field in a combined manner. These models incorporate essential basic concepts corresponding to the characteristics of Internet of Things systems, and the use of these fundamental concepts has facilitated the modeling process of these systems. The formal definitions related to the proposed models and their eva‎luation methods are presented in this thesis. These models possess the capability to quantitatively eva‎luate the qualitative attributes of Internet of Things systems, and for this purpose, a modeling and eva‎luation tool named PNDE has been developed. To demonstrate the usefulness of the proposed models, the details and results of the case studies employing these models and the proposed tools are provided in the thesis. The results obtained from various scenarios illustrate the capability for quantitative eva‎luation and the adaptability of the models to Internet of Things systems.

اينترنت اشياء , تحرّك , مدل‌سازي صوري , ارزيابي كمّي , شبكه‌هاي پتري تصادفي

internet of things , mobility , formal models , quantitative eva‎luation , stochastic Petri nets

Arman Sanahmadi

Mohammad Abdollahi Azgomi