Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
surveys:mc [2010/02/16 08:57] maysam.yabandeh |
surveys:mc [2010/02/21 21:45] maysam.yabandeh add discussion |
||
|---|---|---|---|
| Line 2: | Line 2: | ||
| **//Maysam Yabandeh//** [[http://infoscience.epfl.ch/record/146549/files/|pdf]] | **//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 56: | Line 59: | ||
| 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 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 ==== | ==== Modeling Environment ==== | ||
| Line 138: | Line 141: | ||
| 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. | 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 ==== | ==== Peers ==== | ||
| Line 295: | Line 298: | ||
| 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 will be added soon. | ||