Razzaq Misbah, Ahmad Jamil
Department of Computational Sciences, Research Center for Modeling & Simulation (RCMS), National University of Sciences and Technology (NUST), Islamabad, Pakistan.
PLoS One. 2015 Dec 29;10(12):e0145690. doi: 10.1371/journal.pone.0145690. eCollection 2015.
Internet worms are analogous to biological viruses since they can infect a host and have the ability to propagate through a chosen medium. To prevent the spread of a worm or to grasp how to regulate a prevailing worm, compartmental models are commonly used as a means to examine and understand the patterns and mechanisms of a worm spread. However, one of the greatest challenge is to produce methods to verify and validate the behavioural properties of a compartmental model. This is why in this study we suggest a framework based on Petri Nets and Model Checking through which we can meticulously examine and validate these models. We investigate Susceptible-Exposed-Infectious-Recovered (SEIR) model and propose a new model Susceptible-Exposed-Infectious-Recovered-Delayed-Quarantined (Susceptible/Recovered) (SEIDQR(S/I)) along with hybrid quarantine strategy, which is then constructed and analysed using Stochastic Petri Nets and Continuous Time Markov Chain. The analysis shows that the hybrid quarantine strategy is extremely effective in reducing the risk of propagating the worm. Through Model Checking, we gained insight into the functionality of compartmental models. Model Checking results validate simulation ones well, which fully support the proposed framework.
网络蠕虫类似于生物病毒，因为它们能够感染主机并通过选定的媒介进行传播。为了防止蠕虫传播或掌握如何控制流行的蠕虫，常使用 compartmental 模型来研究和理解蠕虫传播的模式与机制。然而，最大的挑战之一是生成验证和确认 compartmental 模型行为特性的方法。这就是为什么在本研究中我们提出了一个基于 Petri 网和模型检查的框架，通过该框架我们可以细致地检查和验证这些模型。我们研究了易感 - 暴露 - 感染 - 康复（SEIR）模型，并提出了一个新模型易感 - 暴露 - 感染 - 康复 - 延迟隔离（易感/康复）（SEIDQR(S/I)）以及混合隔离策略，然后使用随机 Petri 网和连续时间马尔可夫链对其进行构建和分析。分析表明，混合隔离策略在降低蠕虫传播风险方面极其有效。通过模型检查，我们深入了解了 compartmental 模型的功能。模型检查结果很好地验证了模拟结果，充分支持了所提出的框架。
