A MODEL CHECKING APPROACH TO COUNTERING THE DYNAMICS OF INFECTION PROPAGATION OVER NETWORK

  • : Ms Word, Ms Word Format
  • : 70 Pages
  • : ₦3,000 | $25 | ₵60 | Ksh 2720
  • : 1-5 Chapters
  •  
  • Click to DOWNLOAD Materials

A MODEL CHECKING APPROACH TO COUNTERING THE DYNAMICS OF INFECTION PROPAGATION OVER NETWORK

ABSTRACT

With the outbreak of Ebola over the past year, attention has been paid on predicting and resolving the propagation of infectious disease over network of people and animals. Model checking is a commonly used method in the field of software analysis and verification. In this thesis, we propose to use model checking to counteract the spread of foot-and-mouth disease (FMD) in networks. We abstract the FMD spread model and properties, and encode the system using a well-known model checker Spin. Our program is capable of finding intervention policies and evaluating the effectiveness of different policies. Moreover, previous works generally use simulation models to study the disease control problem which cannot provide certainty as to predict whether certain future states of the outbreak are possible under a particular control policy. Model checking, on the other hand, is guaranteed to find a path that leads to the future states as long as they are possible from a given current configuration of the contagion network under a given control policy. It is worth mentioning that the method proposed in this thesis is not limited to infectious diseases, but can also be applied to counter the spread of, for example, computer virus, forest fire, and public opinions.

 

TABLE OF CONTENTS

LIST OF FIGURES …………………………………………………………………………………………………… v

LIST OF TABLES ……………………………………………………………………………………………………. vi

ACKNOWLEDGEMENTS ……………………………………………………………………………………….. vii

Chapter 1  Introduction ……………………………………………………………………………………………… 1

Model Checking ………………………………………………………………………………………………… 2

Linear Temporal Logic ……………………………………………………………………………………….. 4

SMV and Spin …………………………………………………………………………………………………… 5

Thesis Organization ……………………………………………………………………………………………. 5

Chapter 2  Background and Related Work …………………………………………………………………… 7

FMD and Related Research …………………………………………………………………………………. 7

Model Checking and Related Research ………………………………………………………………… 8

Chapter 3  Approaches and Methods …………………………………………………………………………… 10

Farm Network and Propagation Function ……………………………………………………………… 10

Identifying a Control Policy ………………………………………………………………………………… 12

Effectiveness Evaluation of Control Policy …………………………………………………………… 13

Checking Possible Future State ……………………………………………………………………………. 14

Chapter 4  Experiments and Results ……………………………………………………………………………. 15

Experiment Setup ………………………………………………………………………………………………. 15

Checking Possible Future States ………………………………………………………………………….. 19

Evaluating Effectiveness of Policies. ……………………………………………………………………. 29

Chapter 5 Summary and Conclusion ……………………………………………………………………………. 34

Summary ………………………………………………………………………………………………………….. 34

Limitations ……………………………………………………………………………………………………….. 34

Future Work. …………………………………………………………………………………………………….. 35

References ……………………………………………………………………………………………………………….. 37

 

LIST OF FIGURES

Figure 4-1. Simulation and verification mode algorithms of Spin. …………………………………… 18

Figure 4-2. Days used to stop infections on different policies. ………………………………………… 29

Figure 4-3. Number of dead nodes on different policies. ……………………………………………….. 30

Figure 4-4. Doses of vaccination used on different policies. …………………………………………… 30

Figure 4-5. Days used to stop infections on different latent period. …………………………………. 31

Figure 4-6. Number of dead nodes on different latent period. …………………………………………. 32

Figure 4-7. Doses of vaccination used on different latent period. ……………………………………. 32

 

LIST OF TABLES

Table 4-1. The number of nodes in different states at each day for the counter example of

property p1. ………………………………………………………………………………………………………. 20

Table 4-2. The number of nodes in different states at each day for the counter example of

property p2. ………………………………………………………………………………………………………. 21

Table 4-3. The number of nodes in different states at each day for the counter example of

property p3. ………………………………………………………………………………………………………. 23

Table 4-4. The number of nodes in different states at each day for the counter example of

property p4. ………………………………………………………………………………………………………. 24

Table 4-5. The number of nodes in different states at each day for the counter example of

property p5. ………………………………………………………………………………………………………. 25

Table 4-6. The results of finding the lower limit of policies that can guarantee stop the

infection for both models. …………………………………………………………………………………… 26

Table 4-7. Performance summaries of the experiments on both theoretical model and real

data model… ……………………………………………………………………………………………………… 28

Table 4-8. Summary of comparisons between the model checking and simulation

approach… ………………………………………………………………………………………………………… 28

 

Chapter 1

Introduction

Foot-and-mouth disease (FMD) is an infectious viral disease that affects cloven-hoofed animals including sheep, pig, and cattle. The virus causes vesicles around hooves and mouths, high fever, weight loss, and is sometimes fatal to the infected animals. Given the hardiness of virus survival and transmissibility of FMD, which may lead to severe consequences including economic loss and trade restrictions posed to the society, it is of great importance to find effective policies to control FMD. However, since FMD is a foreign animal disease and field experiments are difficult or prohibited, mathematical and computation modeling methods have been proven to be successful ways to help control FMD.

The dynamics of the infectious disease spread can be viewed and modeled as the evolution of the states of nodes in trees, graphs, and other data structures. When given an initial configuration of a network and a propagation function defining how infectious nodes evolve over time, the model checking method can be used to find whether an intervention policy exists. We can also evaluate the effectiveness of different prevention policies. More importantly, by using model checking, we can check whether a future configuration (scenario) is possible or not. The result would provide direct insights to many important questions.

In this thesis, we propose to use model checking to resolve the problem of counteracting infection spread in networks, specifically for the control of foot-and-mouth disease (FMD). We address the following questions in this thesis. First, we construct a network and study the propagation function over the network. Second, we use model checking techniques to search for an effective intervention policy based on the initial configuration of the FMD model and propagation function. Third, we verify the effectiveness of different intervention policies. Finally, we answer some proposed questions by using model checking to examine whether a future configuration (scenario) is possible. We also compare our model checking approach with simulation on their performances. It is worth mentioning that our approach of identifying and verifying effective policies using model checking is not limited to counter-act disease across a network of animals. It can also be applied to, for example, virus across a network of computers (Serazzi and Zanero, 2004), fire across a network of forests (Finbow and MacGillivray, 2009), and rumors across a network of social media (Zanette, 2002).

1.1 Model Checking

It is of great importance to verify the correctness of computer systems. Formal verification is widely applied in both hardware and software design and system checking. Particularly it plays a major role in safety critical systems. Formal verification usually consists of three essential parts.

  • A framework or model for the system: use a description language to model the system.
  • A specification language: use a specification language to define the properties that will be checked for the system.
  • A verification method: use a verification method to determine whether the model meets the specifications.

As one of the common formal verification methods, model checking is an automated property verification method originally developed to deal with the bugs in concurrent systems. Concurrency bugs are usually difficult to be found by testing due to their non-reproducible characteristics and the fact that they are not covered by test cases. Model checking plays an important role in finding bugs in the concurrent systems (Huth and Ryan, 2004).

Model checking uses temporal logic, which is propositional and predicated logic. A model based on temporal logic has several states and can be true for some states and false for other states. For those dynamic formulas, they can change their values with the evolution of the system from state to state. For traditional logic, the value may never change when the value of all its boolean variables are fixed such as p = A ¬B C. Instead, temporal logic uses the concept of time, which is represented as the transition between different states. In this sense, the value of a formula is not fixed because of its dynamic nature (Huth and Ryan, 2004).

In model checking, we use M to represent the transition system, and 𝜙 to represent the properties of the system. To verify whether the property meets the model, model checking process usually consists of three general steps.

  • Use a description language to model the system as model M.
  • Use a specification language to encode the property 𝜙.
  • Run the model checker to see whether the property holds for the model M.

Generally speaking, the ultimate goal of model checking is to check the following entailment.

M, s |= 𝜙

Here M is the model that model checking works on, s is the starting state of the model and 𝜙 is the specifications to be checked. The output answer of running the model checker is either success, which means the property holds for the model M, or “error”, which means the property does not hold for the model M. For most model checkers, if the answer is “error”, they will also produce a counter example with traces that lead to the failure. This function is very useful in the design and debugging of the system. For our project, we can take advantage of this feature to help us find a control policy that can stop the propagation of the infectious disease (Huth and Ryan, 2004).

1.2 Linear Temporal Logic

Linear time temporal logic (also known as LTL) is a temporal logic that treats the time as an infinite sequence of states. If we consider a sequence of states as a path, we can encode all future paths using LTL. The formal description of LTL is as follows (Huth and Ryan, 2004).

𝜙 = T | F | p | (¬1) | (12) | (12) | (1 → 𝜙2) | (X𝜙1) | (F𝜙1) | (G𝜙1) | (𝜙1 U 𝜙2) | (𝜙1 W 𝜙2) |

(1 R 𝜙2)

In the definition above, p is a propositional atom. Also, T, F, ¬𝜙1, 12 and 𝜙12 are all LTL formulas if 𝜙1 and 𝜙2 are LTL formulas. X, G, F, W, U, R are operators. For example, X means next, so X𝜙1 is true if 𝜙1 is true in the next state. G means globally all future states, so G𝜙1 is true if 𝜙1 is true for all future states. F means some future states, so F𝜙1 is true if 𝜙1 is true for some future states. U, R, W in the formula represent Until, Release, and Weak-until. The details of all the operators can be found at the book Logic in Computer Science (Huth and Ryan, 2004).

1.3 SMV and Spin

NuSMV (also known as SMV) that stands for “New Symbolic Model Verifier.” As an open and structured platform for model checking, SMV provides a description language for system modeling and directly checks the linear-time temporal logic on these models. SMV takes (1) a program written in a description language that describes the system, and (2) a specification written in linear temporal logic as the input. The output is either true, if the specification holds for the system, or a trace that leads to the failure showing why the specification does not hold for the system (Huth and Ryan, 2004).

Another model checker, Spin (Simple Promela INterpreter), is developed by Gerard Holzmann at Bell Labs in 1980. It is widely used in analyzing Promela programs on system design errors such as deadlocks and assertion violations. The systems that Spin works on are described in Promela (Process Meta Language), which is a modeling language used to describe concurrent and distributed systems such as network protocols. Similar to SMV, Spin verifies properties in linear temporal logic formulas. Because most of our experiments are implemented in Spin, we will discuss the use of Spin in details in the experiment sections.

1.4 Thesis Organization

The remaining of the thesis is organized as follows. Chapter 2 provides the background information and discusses the related works of literature on foot-and-mouth disease and model checking. Chapter 3 explains the approach and methods we used in details. Chapter 4 contains implementation of the experiments and discussion of the experiment results. The last chapter

discusses the summary, limitation and future work for this project.

A MODEL CHECKING APPROACH TO COUNTERING THE DYNAMICS OF INFECTION PROPAGATION OVER NETWORK

Sharing is caring!

Leave a Reply