Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
surveys:mc [2010/02/22 19:41] maysam.yabandeh |
surveys:mc [2010/03/01 10:11] (current) maysam.yabandeh |
||
|---|---|---|---|
| Line 12: | 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. | 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. | ||
| Line 310: | Line 310: | ||
| Q: How about SMASH? | Q: How about SMASH? | ||
| - | A: I will check it. | + | 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. |