Extended state identification and verification using a model checker Export

@article{citeulike:867730, abstract = {This article presents a method for the application of model checking, i.e., verifying a finite state system against a given temporal specification, on the problem of generating test inputs. The generated test inputs allow state characterization, i.e., the identification of internal states of the software under test by observation of the input/output behavior only. A test model is derived semi-automatically from a given state-based specification and the testing goal is specified in terms of temporal logic. On the basis of these inputs, a model checking tool performs the testing input generation automatically. In consequence, the complexity of our approach is strongly depending on the input model, the testing goal, and the model checking algorithm, which is implemented in the used tool. The presented approach can be adapted with small changes to other model checking tools. It is a capable test generation method, whenever a finite state model of the software under test exists. Furthermore, it provides a descriptive view on state-based testing, which may be beneficial in other contexts, e.g., education and program comprehension.}, author = {Robinson-Mallett, Christopher and Liggesmeyer, Peter and Mucke, Tilo and Goltz, Ursula}, booktitle = {Advances in Model-based Testing}, citeulike-article-id = {867730}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.infsof.2006.03.006}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B6V0B-4K18VP9-1/2/9caa8ab3ed794a07884105e38f5f2b50}, doi = {10.1016/j.infsof.2006.03.006}, journal = {Information and Software Technology}, keywords = {arantza, ontopipe, std, testing}, month = {October}, number = {10}, pages = {981--992}, posted-at = {2006-09-25 13:41:09}, priority = {2}, title = {Extended state identification and verification using a model checker}, url = {http://dx.doi.org/10.1016/j.infsof.2006.03.006}, volume = {48}, year = {2006} }

TY - JOUR ID - citeulike:867730 L3 - citeulike-article-id:867730 N2 - This article presents a method for the application of model checking, i.e., verifying a finite state system against a given temporal specification, on the problem of generating test inputs. The generated test inputs allow state characterization, i.e., the identification of internal states of the software under test by observation of the input/output behavior only. A test model is derived semi-automatically from a given state-based specification and the testing goal is specified in terms of temporal logic. On the basis of these inputs, a model checking tool performs the testing input generation automatically. In consequence, the complexity of our approach is strongly depending on the input model, the testing goal, and the model checking algorithm, which is implemented in the used tool. The presented approach can be adapted with small changes to other model checking tools. It is a capable test generation method, whenever a finite state model of the software under test exists. Furthermore, it provides a descriptive view on state-based testing, which may be beneficial in other contexts, e.g., education and program comprehension. IS - 10 JF - Information and Software Technology EP - 992 TI - Extended state identification and verification using a model checker VL - 48 T2 - Advances in Model-based Testing SP - 981 KW - arantza KW - ontopipe KW - std KW - testing AU - Robinson-Mallett, Christopher AU - Liggesmeyer, Peter AU - Mucke, Tilo AU - Goltz, Ursula PY - 2006/10// UR - http://dx.doi.org/10.1016/j.infsof.2006.03.006 ER -