University of Sannio, Italy
CADP (Construction and Analysis of Distributed Processes)
DPF (Design Pattern Finder)
Detecting instances of design patterns helps assessing the quality of
the source code of object-oriented software systems. The DPF (Design
Pattern Finder) tool automatically extracts used design patterns from
the object oriented source code. DPF is based on a meta-model and
graph comparison techniques. Similar to other automatic design pattern
extraction techniques, the results computed by DPF are not always very
precise: some design patterns might be missed (DPF is not complete),
and some design patterns might be falsely detected (DPF is not sound).
This case study tackles the latter, using model checking to refine the
results computed by DPF.
To extract design patterns from a Java system, the proposed approach applies the following steps. First DPF analyzes the source and byte code, yielding a model (called system graph) according to DPF's meta-model. Second, design pattern candidates are extracted from the system graph using graph matching. Third, the system graph is translated into a basic LOTOS specification, and each design pattern candidate is translated into a set of mu-calculus formulae, instantiating formula templates with parameters extracted during the model construction step. Finally, the obtained mu-calculus formulae are checked on the LOTOS specification: if a formula is not satisfied, the corresponding design pattern is a false positive, i.e., wrongly detected.
Using model checking takes into account additional structural or
behavioral relationships, enabling to check a wider set of properties,
to increase the precision, and to significantly reduce the number of
Mario Luca Bernardi, Marta Cimitile, Giuseppe De Ruvo, Giuseppe A.
Di Lucca, and Antonella Santone.
"Improving Design Patterns Finder Precision Using a Model Checking
In Proceedings of the CAiSE 2015 Forum at the 27th International
Conference on Advanced Information Systems Engineering (CAiSE'2015),
Stockholm, Sweden, CEUR Workshop Proceedings, volume 1367, pp. 113-120,
Available on-line at: http://ceur-ws.org/Vol-1367/paper-15.pdf
or from the CADP Web site in PDF or PostScript
Department of Engineering
University of Sannio
82100 - Benevento
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|