Design Patterns Formal Composition and Analysis

Design Patterns Formal Composition and Analysis

Halima Douibi (University Abdel Hamid Mehri, Constantine, Algeria) and Faiza Belala (University Abdel Hamid Mehri, Constantine, Algeria)
DOI: 10.4018/IJITSA.2019070101

Abstract

Informal description of design patterns was adopted to facilitate their understanding by software developers. However, these descriptions lead to ambiguities limiting their successful use in real applications. Recently, several formal methods have been employed to guarantee precise specification of design pattern elements without insisting on their behavior. The main goal of this article is to propose a rewriting logic-based framework for enhancing formal description and reasoning on design patterns composition. The proposed model is integrated and executed under Maude using K-Maude tool. It allows first to associate a meta model notation, according to MDA approach, to all design patterns elements and then, a Maude semantic basis for specifying both their structural and dynamic aspects, is given. In particular, it will be shown how the authors' combined modeling approach is exploited for defining a set of operations on patterns, and how it will be used to formal analyze patterns composition.
Article Preview

1. Introduction

In Gamma catalog (Gamma et al., 1995) Design Patterns are described in a consistent and structured way. A pattern is presented by several properties whose name, purpose, an example of a design problem that it solves and a structure of the proposed solution in the form of class diagrams. Although these Design Patterns are well documented, the decision to apply them is manual and remains largely dependent on the user. In fact, Design Patterns are elements of Reusable Object-Oriented Software, described using a combination of natural language, UML diagrams, and program code. Formal specification of Design Patterns can help to use them more effectively and correctly in software development. It can eliminate ambiguity by clarifying the different pattern’s concepts, at the same time this formal specification provides a solid foundation for reasoning about their composition and inter-relationships.

Several attempts have been made to deal with patterns formalization problem; they try to specify patterns in terms of mathematical structures and then, to check formally their accuracy (Blewitt et al., 2001; Gasparis, 2007; Herranz et al., 2002; Taibi & Ngo, 2003). Recently various formal methods (e.g. event sets, process algebras, First Order Logic, Temporal Logic of Actions), each with a particular semantics, have been used in this context. However, existing works do not pay more attention to model Design Patterns elements in order to ensure specific properties of the produced software or to increase the correctness of patterns composition. The adopted formalisms lack appropriate constructs and natural semantics to deal with specification and analysis of dynamic operations on Design Patterns.

Rewriting logic, introduced initially by Jose Meseguer (Meseguer, 1992), has been shown as one of the most appropriate formalisms to describe concurrent and non-deterministic systems. This logic unifies several formal models (Process Algebras, Petri Nets Labeled Transition Systems, ECATNets, Event Structures) (Bettaz & Maouche, 1993; Bouanaka, 1998; Marti-Oliet & Meseguer, 1996). Besides, it has several tools and operational environments; this encourages its use for systems prototyping and analysis.

K-Maude tool (Serbanuta & Rusu., 2010) is one of the most recent interface implementation, which represents a semantic framework allowing the definition of programming languages, calculi, as well as type systems or formal analysis tools (Rusu et al., 2016). In addition, it may use all Maude system surrounded verification and checking tools, as the LTL model-checker (Clavel et al., 2007b).

Another interesting feature of K-Maude tool is that thanks to its programming language description and execution capabilities, one may define its own language, enough expressive and well understood by designers. Our contribution in this work is to show how this language is extended to improve specification and analysis of Design Patterns relationships and particularly their composition. Thus, an incremental approach to formalize Design Patterns is given. This approach consists of four main phases:

  • 1.

    Providing a more abstract and generic notation of any pattern: DP-MM (Design Pattern Meta Model), starting from the most known patterns of GOF (Gamma et al., 1995), according to MDA technique;

  • 2.

    Defining a pattern as an instance of the proposed (DP-MM) Meta model;

  • 3.

    Integrating this pattern description model in Maude (Clavel et al., 2007a) in a transparent manner, allowing a non-familiar user to manipulate our Maude based executable specifications;

  • 4.

    Extending both previous models to deal with dynamic operations on Design Patterns (as composition, restriction, etc.).

Complete Article List

Search this Journal:
Reset
Open Access Articles: Forthcoming
Volume 13: 2 Issues (2020): Forthcoming, Available for Pre-Order
Volume 12: 2 Issues (2019)
Volume 11: 2 Issues (2018)
Volume 10: 2 Issues (2017)
Volume 9: 2 Issues (2016)
Volume 8: 2 Issues (2015)
Volume 7: 2 Issues (2014)
Volume 6: 2 Issues (2013)
Volume 5: 2 Issues (2012)
Volume 4: 2 Issues (2011)
Volume 3: 2 Issues (2010)
Volume 2: 2 Issues (2009)
Volume 1: 2 Issues (2008)
View Complete Journal Contents Listing