Publica
Hier finden Sie wissenschaftliche Publikationen aus den FraunhoferInstituten. Generating Optimal Distinguishing Sequences with a Model Checker
 First International Workshop on Advances in ModelBased Testing, AMOST 2005. Proceedings New York: ACM Press, 2005 ISBN: 1595931155 7 pp. : Ill., Lit. 
 International Workshop on Advances in ModelBased Testing (AMOST) <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.