PLEDGE: A PracticaL and Efficient Data GEnerator for UML

Short description:

The ability to generate test data is often a necessary prerequisite for automated software testing. For the generated data to be fit for its intended purpose, the data usually has to satisfy various logical constraints derived from specifications. When testing is performed at a system level, these constraints tend to be complex and are typically captured in expressive formalisms based on first-order logic. Using UML and its constraint language, OCL, is a standard way for capturing such constraints at a system level. However, common solvers, such as SAT or SMT, are not sufficient to address such complex constraints.

Motivated by improving the feasibility and scalability of data generation for system testing, we present a novel tool named PLEDGE (PracticaL and Efficient Data GEnerator). PLEDGE hybridizes metaheuristic search and Satisfiability Modulo Theories (SMT) for generating UML instance models subject to complex OCL constraints. This hybridization is done in such a way as to take advantage of the complementary strengths of metaheuristic search and SMT.

In a nutshell, PLEDGE works by first transforming all the constraints ascribed to a UML data model into a single constraint. This single constraint is represented in the Negation Normal Form (NNF). The tool then distributes the responsibility of solving the different subformulas in this normal form over (metaheuristic) search and SMT. Intuitively, search handles subformulas whose satisfaction involves structural tweaks to the instance model, i.e., additions and deletions of objects and links. SMT handles subformulas involving only primitive attributes, i.e., attributes with primitive types. These subformulas, if satisfiable, can be solved without structural tweaks. Many such subformulas, e.g., those whose symbols are within linear arithmetic, can be efficiently handled by background SMT theories. Finally, search and SMT are both tasked with handling subformulas whose satisfaction may require a combination of structural tweaks and value assignments to primitive attributes.

System requirements:

• Java SE Runtime Environment 8 (or higher)
• Z3 (version 4.5.1); Installation instructions for Z3 can be found at this [link].

PLEDGE's installation material:

• The most recent version of PLEDGE can be downloaded from this [link].

(Sanitized) Industrial examples:

• Case A: [class diagram (uml)*], [OCL constraints (txt)], [NNF constraint (txt)], [example object diagram with 20 instances of the root class(uml)*]
• Case B**: [class diagram (uml)*], [OCL constraints (txt)], [NNF constraint (txt)], [example object diagram with 20 instances of the root class (uml)*]
• Case C: [class diagram (uml)*], [OCL constraints (txt)], [NNF constraint (txt)], [example object diagram with 20 instances of the root class (uml)*]

* The files with a .uml extension can be opened within any EMF-based modeling environment, e.g., Papyrus.

** The Alloy model corresponding to Case B can be found at this link. This model was generated by UML2Alloy.

How to cite?

• People who wish to use or compare with PLEDGE in their publications can cite the following arXiv article: https://arxiv.org/abs/1902.00397
• The tool was developed within the SVV laboratory. For details of other publications and tools from the laboratory, please see [link].

Acknowledgment

This work is supported by the European Research Council under the European Union’s Horizon 2020 research and innovation program (grant agreement number 694277).

Contact Information

• Ghanem Soltana [homepage], Mehrdad (Mike) Sabetzadeh [homepage], and Lionel C. Briand [homepage]
• Affiliation: University of Luxembourg -- Interdisciplinary Centre for Security, Reliability and Trust
• Address: 29, Avenue John Fitzgerald Kennedy, L-1855, Luxembourg
• Emails: {soltana, sabetzadeh, briand}@svv.lu