Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
surveys:mc [2010/02/16 11:54] 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 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. | ||