Gesellschaft f�r Informatik e.V.

Lecture Notes in Informatics


Software Engineering 2006, Proceedings der Fachtagung des GI-Fachbereichs Softwaretechnik, 28.-31. März 2006 in Leipzig P-79, 131-142 (2006).


2006


Editors

Bettina Biel, Matthias Book, Volker Gruhn (eds.)


Contents

State identification and verification using a model checker

Christopher Robinson-Mallett and Peter Liggesmeyer

Abstract


This paper presents a method for the application of model checking, i.e. verifying a finite state system against a given temporal specification, to the problem of generating test inputs. The generated test inputs allow state characterization, i.e. the identification and verification of internal states of the software under test by observation of the input/output behavior only. A test model is derived semiautomatically 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 depending on the input model, the testing goal, and the applied model checking algorithm. The presented approach can be adapted with small changes to other model checking tools. It is a capable test generation method, whenever a state based behavioral specification 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.


Full Text: PDF

ISBN 3-88579-173-0


Last changed 24.01.2012 21:53:21