Abstract:
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, compart mental models are commonly used as a means to examine and understand
the patterns and mechanisms of a worm spread. However, one of the greatest
challenges is that we have failed to produce methods to verify and validate the
behavioural properties of a compartmental model. This is why in this study
we suggested a framework based on Petri Nets and Model Checking through
which we can meticulously examine and validate these models. We investi gated Susceptible-Exposed-Infectious-Recovered (SEIR) model and proposed
a new model Susceptible-Exposed-Infectious-Recovered-Delayed-Quarantined
(Susceptible/Recovered) (SEIDQR(S/I)) along with hybrid quarantine strat egy, which is then constructed and analysed using Stochastic Petri Nets and
Continuous Time Markov Chain. The analysis shows that the hybrid quar antine 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 validates simulation ones
well, which fully support the proposed framework.
