Article Preview
Top1. 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.).