Differences

This shows you the differences between two versions of the page.

--- surveys:mc [2010/02/15 22:59]
maysam.yabandeh
+++ surveys:mc [2010/03/01 10:11] (current)
maysam.yabandeh
@@ Line 1: / Line 1: @@
 ====== Model Checking Tools for Software Systems ======
-**//Maysam Yabandeh//** [[http://infoscience.epfl.ch/record/146549/files/|pdf]]
+**//[[http://people.epfl.ch/maysam.yabandeh|Maysam Yabandeh]]//** [[http://infoscience.epfl.ch/record/146549/files/|pdf]]
+//Please add your comments into Section [[mc#Discussion]]//
 Systematic State Exploration or Model Checking techniques have been used for years to check the model of software against user-specified properties. Nevertheless, they never achieved a wide-spread usage because of the difficulties and problems in translating from the programming languages, which are used to develop the software, to the modeling language on which the model checker can work. Recently, there have been several efforts in direct state exploration of software system implementations. In this survey, we illustrate the challenges in this domain and explain the different solutions adopted by the state-of-the-art developed tools for state exploration of software systems.  The focus of this paper in on the developed model checking tools for software systems, and it does not include solutions for unit testing and selecting the optimal test scenarios.
@@ Line 9: / Line 12: @@
 Systematic State Exploration, which is also known as **model checking**, has been used for years to systematically explore reachable states in a model and to verify them against user-specified properties. The model can be made based on a software system, a hardware system, or any general phenomena. The languages that are used to develop software systems are different from the modeling language, and the developer has to go through the tedious, time-consuming task of translating the original program into the modeling language, i.e., **abstraction**. These difficulties discourage the developers to use the model checker tools for large software systems.
-To alleviate these problems, two general approaches have been used: i) automatically generating a model of the software, and ii) directly exploring the state space of the original software itself rather than a model of that. The former approach still suffers from the drawbacks of translation into a model; due to mismatches between the original software and the abstracted model, the found bugs are not sound. In other words, the reported bugs can not necessarily manifest in the original application as well.
+To alleviate these problems, two general approaches have been used: i) automatically generating a model of the software [[http://dblp.uni-trier.de/rec/bibtex/journals/sttt/BeyerHJM07|BLAST]] [[http://dblp.uni-trier.de/rec/bibtex/conf/popl/GodefroidNRT10|SMASH]], and ii) directly exploring the state space of the original software itself rather than a model of that. The former approach still suffers from the drawbacks of translation into a model; due to mismatches between the original software and the abstracted model, the found bugs are not sound. In other words, the reported bugs can not necessarily manifest in the original application as well.
+A recent example of approaches that automatically construct the abstract state space for exploration is [[http://dblp.uni-trier.de/rec/bibtex/journals/sttt/BeyerHJM07|BLAST]]. The estimated abstract model is an over-approximation of the actual state space with respect the checking predicates. In other words, the abstracted model is guaranteed to explore all the paths that leads to the violation of user-specified predicates, but the explored paths are not all feasible. BLAST uses the counterexamples to refine the abstract model. This process continues till either the the tool returns, proving no predicate violation, or return a path that violates the specified predicate. False negatives and positives are still positive due to mismatch between the programming language, C, and the abstracted model.
 The second approach, which is the focus of this paper, systematically explores the state space of the software system by controlling the scheduler and the inputs to the software. In this way, the developers can check the state space of their software without going through the error-prone, expensive task of abstraction. Although appealing, there are certain challenges in this approach that affect both applicability and efficiency of such tools. In this paper, we demonstrate these challenges and the different solutions adopted by the related tools.
@@ Line 56: / Line 61: @@
 Not all the branches in the state graph that is obtained by symbolic execution are valid; some branches can be impossible to be traversed in a real run. The property checking module can help to prune some impossible branches. It can be used to evaluate the condition in the instruction; if the condition is evaluated as false, then the corresponding branch will be pruned, and vice versa. In Figure {{:surveys:se-statespace.gif?100|}}, the grayed branches are pruned from exploration. Consequently, the size of the space graph can be potentially much smaller than the case with early binding.
-The disadvantage of symbolic execution is that the complexity is pushed to the property checking module. However, there are well-known off-the-shelf SAT solvers, which take the history of operations performed on the symbolic variable as well as the list of assumed conditions and return weather the condition is satisfiable or not. The problem is that computation time of SAT solvers is not bounded, and it can take forever for a SAT solver to response. Besides, the size of the assumed condition set and the sequence of performed operations could become too large to be efficiently handled by state-of-the-art SAT solvers. For these reasons, Symbolic Execution can also quickly stick in the state explosion problem.
+The disadvantage of symbolic execution is that the complexity is pushed to the property checking module. However, there are well-known off-the-shelf SAT solvers, which take the history of operations performed on the symbolic variable as well as the list of assumed conditions and return whether the condition is satisfiable or not. The problem is that computation time of SAT solvers is not bounded, and it can take forever for a SAT solver to respond. Besides, the size of the assumed condition set and the sequence of performed operations could become too large to be efficiently handled by state-of-the-art SAT solvers. For these reasons, Symbolic Execution can also quickly get stuck with the state explosion problem.
-==== Modeling Environment ====
-The only thing that the state space exploration algorithm can be certain about is the sequence of program instructions. The sequence of states that will be explored by a program run depends on the particular environment that the program is deployed in.
-The **environment** is everything except the sequence of instructions in the program, which includes the hardware, the operating system, the communication environment, the input devices, the time, and also the other programs that will interact with the software.
-Every uncertainty about the environment introduces a non-determinism point into the search algorithm and worsens the state explosion problem. On the other hand, every assumption about the environment eliminates the corresponding non-determinism point and alleviates the state explosion problem.
-Another advantage of modeling the environment is eliminating the states which are impossible or improbable for the deployed software system to get into. For example, if we know that the input values to the system are always non-zero, we can ignore the branches that check for zero values. Beside the reduction in number of explored states, the search algorithm does not report the invariant violations that are impossible or improbable to occur in practice. Therefore the accuracy of the search algorithm increases and the number of false positive reports reduces.
-The disadvantage of modeling the environment is that the state exploration software becomes i) more complicated and ii) more environment dependent. For each model, we have to add some new logics that implement the model to the state exploration system, which makes the state exploration system complicated. On the other hand, every model makes some assumptions about the environment in which the software will be deployed. These assumptions could change from system to system or from time to time. However, the expenses for updating the model might not be trivial. For example, using a model of TCP rather than its actual implementation is one major source of complexity in the state exploration tools. Moreover, the model has to be updated when new versions of TCP are deployed.
-In the next section, we categorize the parts of the environment surrounding the software systems and discuss the employed techniques for modeling them or reducing uncertainty regarding them.
-===== Environment =====
-We define the environment as all the elements that will directly or indirectly affect the behavior of the deployed system. For each part of environment that we are uncertain about its behavior, we must explore all the possible actions and reactions in model checking. Uncertainty regarding each part of the environment can lead to more non-determinism points in the exploration process and consequently worsen the state explosion problem. By assuming a model for each part of the environment, we can further reduce the uncertainty and hence alleviate the exponential growth of the state space.
-In this section, we categorize the different parts of the environment and present different approaches that have been taken to reduce the uncertainty regarding each category. For a software system, we can split the environment into three general categories: i) the upper layer applications, which uses the provided service by the software, ii) the lower layer services, which supply the software with some services, and iii) the peers, which are the identical replicas of the software with whom the software interacts. In the following, we explain each category in more detail.
-====== Model Checking Tools ======
-Systematic State Exploration or Model Checking techniques have been used for years to check the model of software against user-specified properties. Nevertheless, they never achieved a wide-spread usage because of the difficulties and problems in translating from the programming languages, which are used to develop the software, to the modeling language on which the model checker can work. Recently, there have been several efforts in direct state exploration of software system implementations. In this survey, we illustrate the challenges in this domain and explain the different solutions adopted by the state-of-the-art developed tools for state exploration of software systems.  The focus of this paper in on the developed model checking tools for software systems, and it does not include solutions for unit testing and selecting the optimal test scenarios.
-===== Introduction =====
-Systematic State Exploration, which is also known as **model checking**, has been used for years to systematically explore reachable states in a model and to verify them against user-specified properties. The model can be made based on a software system, a hardware system, or any general phenomena. The languages that are used to develop software systems are different from the modeling language, and the developer has to go through the tedious, time-consuming task of translating the original program into the modeling language, i.e., **abstraction**. These difficulties discourage the developers to use the model checker tools for large software systems.
-To alleviate these problems, two general approaches have been used: i) automatically generating a model of the software, and ii) directly exploring the state space of the original software itself rather than a model of that. The former approach still suffers from the drawbacks of translation into a model; due to mismatches between the original software and the abstracted model, the found bugs are not sound. In other words, the reported bugs can not necessarily manifest in the original application as well.
-The second approach, which is the focus of this paper, systematically explores the state space of the software system by controlling the scheduler and the inputs to the software. In this way, the developers can check the state space of their software without going through the error-prone, expensive task of abstraction. Although appealing, there are certain challenges in this approach that affect both applicability and efficiency of such tools. In this paper, we demonstrate these challenges and the different solutions adopted by the related tools.
-In this paper, we refer to the employed algorithm for state exploration, as exploration algorithm or search algorithm. Given a explored state, the search algorithm invokes a property checker module on that. The property checker could check for deadlocks or user-specified properties which are also known as invariants. The assert statements inside the source code can either be checked by the property checker or their violation can be trapped and be reported to the developer.
-Similar to the tools for checking the models, the main challenge is still the state space explosion issue: the phenomena of exponentially increase in number of states by exploring deeper levels. However, here more number of non-determinisms as well as the large size of the real applications worsen this problem in a way that exhaustive exploration techniques become ineffective. Section [[mc#State Explosion Problem|link]] demonstrates this problem and its direct correlation with non-determinisms in the software systems. Section [[mc#Environment|link]] discusses that how we can alleviate the state explosion problem by more precise emulation of the environment. Section [[mc#Exploration Algorithm|link]], explains the changes in the exploration algorithms that can make efficient exploration of such large state spaces feasible. Finally, in Section [[mc#Exploration Algorithm|link]] we compare the state-of-the-art tools and illustrate how each of them addresses the described challenges.
-===== State Explosion Problem =====
-The processing unit (CPU) that runs a software program computes only the single next state of the system by executing the next instruction in the program.
-Figure  depicts the state space explored by running the sample program presented in Figure<latex>bool $x$ = read(); bool $y$ = read(); if ($x$ and $y$) $z$ = 5; else $z$ = 8; if ($x$) $z$ = 2 * $z$; else $z$ = 0; </latex>.
-In contrary to that, more than one state can result from an instruction execution in systematic state space exploration.
-For example, when an if-then-else instruction checks for a variable that its value is received from an input device such as keyboard, the next state of the system depends on the concrete value of the variable. Although this value will be determined at run-time, during state space exploration it is a source of **non-determinism** for the search algorithm.
-Corresponding to each non-determinism point, a branch will be introduced to the state space to cover all the possible options. Taking each branch leads the system to a potentially different state. The number of reachable states exponentially increases with the number of branches, which is known as **state explosion** phenomenon.
-==== State Space ====
-As mentioned before, the space of potential states that a software can visit is way larger than the set of visited states by a particular run. For example, the state space of the snippet of code shown in Figure<latex>bool $x$ = read(); bool $y$ = read(); if ($x$ and $y$) $z$ = 5; else $z$ = 8; if ($x$) $z$ = 2 * $z$; else $z$ = 0; </latex>
- is illustrated in Figure {{:surveys:whole-statespace.gif?100}}. As you can observe, in contrary to the visited states by running the program, the state space is not sequential; there exist branches corresponding to each non-determinism point. Each set of joint branches bind some values to a particular non-determinism point. For example, corresponding to Variable <latex>x</latex> which be assigned at run-time, there is a branch at Figure {{:surveys:whole-statespace.gif?100}} to cover both values **true** and **false**.
-The policy that specified the position that a branch appears in the state graph is determined by the exploration algorithm. The policy defines when the possible values should be bound to the non-determinism points.
-=== Early Binding ===
-In early binding, a branch covering the possible values is added when the variable is assigned. For example, in the snippet of code shown in Figure
-<latex>bool $x$ = read(); bool $y$ = read(); if ($x$ and $y$) $z$ = 5; else $z$ = 8; if ($x$) $z$ = 2 * $z$; else $z$ = 0; </latex>
-, Boolean <latex>x</latex> is assigned by reading from keyboard. In Figure {{:surveys:whole-statespace.gif?100}}, which is the visited states following by the early-binding policy, the first branch is added immediately after assigning the value to Boolean <latex>x</latex> in the program.
-=== Late Binding, Before Usage ===
-In late binding before usage, a set of branches covering the possible values is added right before the assigned variable is actually used [[http://infoscience.epfl.ch/record/128816|link]]. For example, in Figure {{:surveys:latebinding-statespace.gif?100|}}, which depicts the visited states following by the late-binding policy, the first branch is added right before Variable <latex>x</latex> is used at Line~3. The resulting state space by following the late binding policy is equivalent to the state space explored by early binding policy. However, it could potentially be more compact by merging equivalent states. The disadvantage is the slight added complexity for late binding.
-=== Late Binding, During Property Evaluation ===
-The binding can be postponed till the time the model checker evaluates the user-specified properties against the system state. Since the concrete value is not bound, a **symbolic** value is kept for the variable. The model checker then has to keep track of the operations performed on the symbolic value and pass them to the property checking module. This technique is called **Symbolic Execution**.
-The major challenge in symbolic execution is to executing **conditional branch** instructions. Conditional branch in programming languages is the essential part for implementation of if-then-else and loop statements. (Note that conditional branches are different from the branches in state space graph.) In the normal run of the program, the CPU jumps to the position specified by the instruction, if the corresponding condition is evaluated to true. In symbolic execution, the model checker does not have the concrete values to evaluate the condition. Therefore, a branch is added to the state space to cover both true and false values. In Figure {{:surveys:se-statespace.gif?100|}}, the first branch is added right before evaluating <latex>x</latex> \&\& <latex>y</latex> in the first if-then-else statement of the code snippet shown in Figure
-<latex>bool $x$ = read(); bool $y$ = read(); if ($x$ and $y$) $z$ = 5; else $z$ = 8; if ($x$) $z$ = 2 * $z$; else $z$ = 0; </latex>
-. By taking each branch, an assumption is made about the evaluation of the condition. The set of assumptions made along the path will be passed to the property checking module.
-Note that the state space graph obtained by symbolic execution is not equivalent to the state space graph obtained by early binding. Here, the branches in the graph correspond to branch points in the program structure. Corresponding to each if-then-else statement, a branch is added to the current position at state graph.
-Not all the branches in the state graph that is obtained by symbolic execution are valid; some branches can be impossible to be traversed in a real run. The property checking module can help to prune some impossible branches. It can be used to evaluate the condition in the instruction; if the condition is evaluated as false, then the corresponding branch will be pruned, and vice versa. In Figure {{:surveys:se-statespace.gif?100|}}, the grayed branches are pruned from exploration. Consequently, the size of the space graph can be potentially much smaller than the case with early binding.
-The disadvantage of symbolic execution is that the complexity is pushed to the property checking module. However, there are well-known off-the-shelf SAT solvers, which take the history of operations performed on the symbolic variable as well as the list of assumed conditions and return weather the condition is satisfiable or not. The problem is that computation time of SAT solvers is not bounded, and it can take forever for a SAT solver to response. Besides, the size of the assumed condition set and the sequence of performed operations could become too large to be efficiently handled by state-of-the-art SAT solvers. For these reasons, Symbolic Execution can also quickly stick in the state explosion problem.
 ==== Modeling Environment ====
@@ Line 211: / Line 143: @@
 Models can hide the complexities of the operating system services and increase state exploration performance. For example, a PIPE in Linux operating system can be modeled by a simple queue structure. The problem with models is that they are valid as long as conform to the implementation of the original service. In the case of complex services such as TCP, the model is not trivial and can be very complicated. This increases the risk of a mistake in modeling the service as well as expenses of updating the model according to the new changes in the service implementation. The other advantage of using models is that due to simplification in the model, the state of the model is much simpler and more controllable. Thus, it will be feasible to reproduce a series of events on them.
-The expenses of modeling the operating system and its maintenance increase with the increase in the number of operating system services. For example, Windows offers more than 100 system calls [[www.usenix.org/events/nsdi09/tech/full_papers/yang/yang.pdf|link]]; modeling all these system call in an operating system which has more than one million lines of code is very expensive and unreliable.
+The expenses of modeling the operating system and its maintenance increase with the increase in the number of operating system services. For example, Windows offers more than 100 system calls [[http://www.usenix.org/events/nsdi09/tech/full_papers/yang/yang.pdf|link]]; modeling all these system call in an operating system which has more than one million lines of code is very expensive and unreliable.
 ==== Peers ====
@@ Line 287: / Line 219: @@
 === Event Interleaving ===
-The non-determinism in event interleaving is a major contributor to exponential growth of the state space. POR techniques, which are sound and complete, alleviate this problem slightly. Nevertheless, the state explosion still manifests after a few steps. Because of that, most of the developed tools for model checking of software systems were forced to eventually rely on random walks [[http://dblp.uni-trier.de/rec/bibtex/conf/nsdi/KillianAJV07|link]]  [[www.usenix.org/events/nsdi09/tech/full_papers/yang/yang.pdf|link]].
+The non-determinism in event interleaving is a major contributor to exponential growth of the state space. POR techniques, which are sound and complete, alleviate this problem slightly. Nevertheless, the state explosion still manifests after a few steps. Because of that, most of the developed tools for model checking of software systems were forced to eventually rely on random walks [[http://dblp.uni-trier.de/rec/bibtex/conf/nsdi/KillianAJV07|link1]]  [[http://www.usenix.org/events/nsdi09/tech/full_papers/yang/yang.pdf|link2]].
 Realistically speaking, in large software systems the completeness property of POR techniques is not appealing as much. Therefore, the heuristics which are not complete but leads the search to more relevant states are more interesting. One example is **Consequence Prediction**, which is proposed in CrystalBall [[http://www.usenix.org/event/nsdi09/tech/full_papers/yabandeh/yabandeh.pdf|link]]. It filters a non-network handler, if the handler is already run on the same node local state, i.e., the process state.
@@ Line 350: / Line 282: @@
 ==== Modist ====
-Modist  [[www.usenix.org/events/nsdi09/tech/full_papers/yang/yang.pdf|link]] is a stateless model checker for unmodified distributed systems in Windows. The big steps for model checking are the code between two system calls. It instruments the application binary to replace the system calls with some API wrappers. The wrapper mostly contacts the exploration back-end with RPC and then invokes the original system call or returns failure, depending on the back-end response. In the case of networking APIs, the wrapper redirects the call from the original networking API to a network model. The model is implemented by an asynchronous IO channel as well as a proxy thread for intercepting the packets. Therefore, the other processes can be located on remote machines.
+Modist  [[http://www.usenix.org/events/nsdi09/tech/full_papers/yang/yang.pdf|link]] is a stateless model checker for unmodified distributed systems in Windows. The big steps for model checking are the code between two system calls. It instruments the application binary to replace the system calls with some API wrappers. The wrapper mostly contacts the exploration back-end with RPC and then invokes the original system call or returns failure, depending on the back-end response. In the case of networking APIs, the wrapper redirects the call from the original networking API to a network model. The model is implemented by an asynchronous IO channel as well as a proxy thread for intercepting the packets. Therefore, the other processes can be located on remote machines.
 The time issue is addressed by using symbolic execution starting from the invocation position of the time function. The back-end tries different values of time that cover all the branches in the code till a certain depth. The paper does not propose a solution to random functions and their appearance in the application or the operating system can cause difficulties in deterministically replaying the error path.
@@ Line 357: / Line 289: @@
 The source code is not publicly available.
 ===== Conclusions =====
@@ Line 367: / Line 300: @@
 Time and random values are still two big problems in model checking. Although application-specific solutions have been proposed, there is still no approach to force the developers to use them. Perhaps, the future programming languages can be **model checking-aware** in the sense that they force the developers to use only the mechanisms that are already instrumented to be used in model checkers.
+===== Discussion =====
+Q: How about BLAST?
+A: It is added now.
+----
+Q: How about SMASH?
+A: It suffers from the same problems as BLAST does. Abstract based model checking is not in the scope of this paper and citing the paper is enough. I cited the paper in the introduction.