Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Generating Optimal Distinguishing Sequences with a Model Checker

 
: Robinson-Mallett, C.; Liggesmeyer, P.; Mücke, T.; Goltz, U.

:

First International Workshop on Advances in Model-Based Testing, A-MOST 2005. Proceedings
New York: ACM Press, 2005
ISBN: 1-59593-115-5
7 pp. : Ill., Lit.
International Workshop on Advances in Model-Based Testing (A-MOST) <1, 2005, St. Louis/Mo.>
Journal Article
English
Conference Paper
Fraunhofer IESE ()
model checking; verification

Abstract
This paper presents an approach for the automatic generation of shortest Distinguishing Sequences (DS) with the Uppaal model checker. The presented method is applicable to a large number of extended finite state machines and it will find an optimal result, if a DS sequence exists for the considered automaton. Our approach is situated in an integrated testing environment that is used to generate checking sequences. The generation method is based on a DS model, which is derived from the same test model that is used for generating test cover sets. The problem of generating DS is reduced to the definition of a DS model and for this reason the complexity of our approach depends mainly on the used model checking algorithm. This means, that the presented method is automatically improved, when the model checking algorithm is improved. This includes the generation of optimal DS depending on the ability of the model checker to produce optimal results.

: http://publica.fraunhofer.de/documents/N-32979.html