Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
surveys:mc [2010/02/16 11:53]
maysam.yabandeh 		surveys:mc [2010/03/01 10:11] (current)
maysam.yabandeh
Line 1: Line 1:
 ====== Model Checking Tools for Software Systems ====== ====== 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. 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. 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. 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. 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 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 ​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 ==== ==== Modeling Environment ====
Line 295: 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. 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.