Improving Design Pattern Finder Precision Using Model Checking

Organisation:	University of Sannio, Italy
Method:	LOTOS MCL
Tools used:	CADP (Construction and Analysis of Distributed Processes) DPF (Design Pattern Finder)
Domain:	Software Architectures
Period:	2015
Size:	n/a.
Description:	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.
Conclusions:	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 false positives.
Publications:	[Bernardi-Cimitile-DeRuvo-et-al-15] Mario Luca Bernardi, Marta Cimitile, Giuseppe De Ruvo, Giuseppe A. Di Lucca, and Antonella Santone. "Improving Design Patterns Finder Precision Using a Model Checking Approach". 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, June, 2015. Available on-line at: http://ceur-ws.org/Vol-1367/paper-15.pdf or from the CADP Web site in PDF or PostScript
Contact:	Antonella Santone Department of Engineering University of Sannio Viale Traiano 82100 - Benevento ITALY Email: santone@unisannio.it
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page