Logo des Repositoriums
 
Konferenzbeitrag

State identification and verification using a model checker

Lade...
Vorschaubild

Volltext URI

Dokumententyp

Text/Conference Paper

Zusatzinformation

Datum

2006

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

Verlag

Gesellschaft für Informatik e.V.

Zusammenfassung

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.

Beschreibung

Robinson-Mallett, Christopher; Liggesmeyer, Peter (2006): State identification and verification using a model checker. Software Engineering 2006, Proceedings der Fachtagung des GI-Fachbereichs Softwaretechnik. Bonn: Gesellschaft für Informatik e.V.. PISSN: 1617-5468. ISBN: 3-88579-173-0. pp. 131-142. Regular Research Papers. Leipzig. 28.-31. März 2006

Schlagwörter

Zitierform

DOI

Tags