Test generation with Satisfiability Modulo Theories solvers in model‐based testing. (29th May 2014)

• Record Type: Journal Article
• Authors: Cantenot, Jérôme; Ambert, Fabrice; Bouquet, Fabrice; Brucker, Achim D.; Julliand, Jacques
• Is Part Of: Software testing, verification & reliability. Volume 24:Number 7(2014)
• Page Start: 499
• Page End: 531
• Publication Date: 2014-05-29
• Subjects: Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1537
• Languages: English
• ISSNs: 0960-0833

Abstract

<abstract abstract-type="main" id="stvr1537-abs-0001"> <title>SUMMARY</title> <p id="stvr1537-para-0001">This paper presents a framework for UML/OCL model test generation. This framework is based on three parts. The first part is the transformation from a UML/OCL model into a Satisfiability Modulo Theories (SMT) instance. The metamodel associated with the two models and the transformation rules are presented. The second part is the animation strategies used for the generation of SMT instances to compute test sequences. The paper studies five different types of strategy to build the first‐order formula used by an SMT instance. The paper also gives the results of experiments on six case studies that were used to validate the method. Copyright © 2014 John Wiley &amp; Sons, Ltd.</p> </abstract>