Formalizing Patterns with the User Requirements Notation

Patterns need to be described and formalized in ways that enable the reader to determine whether the particular solution presented is useful and applicable to his or her problem in a given context. However, many pattern descriptions tend to focus on the solution to a problem, and not so much on how the various (and often conflicting) forces involved are balanced. This chapter describes the user requirements notation (URN), and demonstrates how it can be used to formalize patterns in a way that enables rigorous trade-off analysis while maintaining the genericity of the solution description. URN combines a graphical goal language, which can be used to capture forces and reason about trade-offs, and a graphical scenario language, which can be used to describe behavioral solutions in an abstract manner. Although each language can be used in isolation in pattern descriptions (and have been in the literature), the focus of this chapter is on their combined use. It includes examples of formalizing Design patterns with URN together with a process for trade-off analysis.

The Applications and Enhancement of LePUS for Specifying Design Patterns

Standardized pattern representations have become a popular way to capture, classify, and communicate the essential characteristics of software designs. Both books and large Web sites serve as pattern repositories for use by software design engineers. Because they are usually expressed in verbal and diagrammatic form using, say, UML, they are susceptible to ambiguities and the consequent misinterpretation. The goal of this chapter is to illustrate how to represent rigorously Design patterns, in order to avoid this problem, and to analyze the capabilities of this technique. It describes a more formal, logic-based language for representing pattern structure and an extension that can also represent other aspects of patterns, such as intent, applicability, and collaboration. This mathematical basis serves to eliminate ambiguities. The chapter explains the concepts underlying the languages and shows their utility by representing two classical patterns, some concurrent patterns, and various aspects of a few other patterns.

Modeling and Reasoning about Design Patterns in Slam-Sl

In this chapter, a formal model for Design patterns is studied. The formal specification of a Design pattern is given as a class operator that transforms a design given as a set of classes into a new design that takes into account the description and properties of the Design pattern. The operator is specified in the Slam-Sl specification language, in terms of pre and postconditions. Precondition collects properties required to apply the pattern and postcondition relates input classes and result classes encompassing most of the intent and consequences sections of the pattern. Formalization is mandatory for reasoning about Design patterns and for implementing assistant tools.

A Visual Language for Design Pattern Modeling and Instantiation

In this chapter we describe the Design pattern modeling language, a notation supporting the specification of Design pattern solutions and their instantiation into UML design models. DPML uses a simple set of visual abstractions and readily lends itself to tool support. DPML Design pattern solution specifications are used to construct visual, formal specifications of Design patterns. DPML instantiation diagrams are used to link a Design pattern solution specification to instances of a UML model, indicating the roles played by different UML elements in the generic Design pattern solution. A prototype tool is described, together with an evaluation of the language and tool.

Precision, Flexibility, and Tool Support

There are two important requirements that any approach to formalizing Design patterns must meet. First, the approach must enable the precise specification of the implementation requirements and behavioral guarantees associated with a wide range of patterns. Second, the formalization of each pattern must retain the pattern’s inherent flexibility. In this chapter, we present a novel approach to formalizing Design patterns that satisfies these seemingly conflicting requirements. For the formalism to be of practical value, we also need tools that can assist practitioners in determining whether the patterns used in designing their systems have been implemented correctly. Such tools are especially important during system maintenance and evolution to ensure that the design integrity of a system is not compromised. We show how our approach lends itself to the construction of such tools.

Formalising Design Patterns as Model Transformations

This chapter describes techniques for the verification of refactorings or transformations of UML models which introduce Design patterns. The techniques use a semantics of object-oriented systems defined by the object calculus (Fiadeiro & Maibaum, 1991; Lano, 1998), and the pattern transformations are proved to be refinements using this semantics.

A Generic Model of Object-Oriented Patterns Specified in RSL

Object-oriented patterns are a promising technique for achieving widespread reuse of software architectures. They capture the static and dynamic structures of components and frameworks in successful solutions to problems for a wide range of domains. However, patterns are invariably described informally in the literature, which makes it difficult to give any meaningful certification of pattern-based software. The design process could be enhanced by means of an automatic support for modeling and verification with a proper formal foundation. In this chapter, we show how formal specifications of GoF patterns, based on the RAISE language, have been helpful in developing that tool support, where we have adopted the well-known Java language upon its portability facet. Thus, the object-oriented design process is extended by the inclusion of pattern-based modeling and verification steps, the latter involving checking design correctness and appropriate pattern application through the use of the supporting tool, called DePMoVe (design and pattern modeling and verification).

Spine

Patterns are often described in terms of concrete examples in specific programming languages in catalogues (Gamma, Helm, Johnson, & Vlissides, 1995). The description is worded such that a practitioner in an object-oriented programming language will be able to understand the key points of the pattern and translate it into a programming language of their choice.This abstract description of patterns is well suited for intelligent readers, but less suited for automated tasks that must process pattern information. Furthermore, the way in which the pattern information is encoded is often strongly influenced by the type of processing that is being performed on the pattern. In this chapter, the Spine language will be presented as a way of representing Design patterns in a suitable manner for performing verification of a pattern’s implementation in a particular source language. It is used by a proof engine

Patterns of Collective Behavior in Ocsid

This chapter presents an abstraction mechanism for collective behavior in reactive distributed systems. The mechanism allows the expression of recurring patterns of object interactions in a parametric form, and the formal verification of temporal safety properties induced by applications of the patterns. The abstraction mechanism is defined and compared to Design patterns, an established software engineering concept. While there are some obvious similarities, because the common theme is abstraction of object interactions, there are important differences as well. The chapter discusses how the emphasis on full formality affects what can be expressed and achieved in terms of patterns of object interactions. The approach is illustrated with the Observer and Memento patterns.

An Integrated Approach to Design Patterns Formalization

A Design pattern describes a set of proven solutions for a set of recurring design problems that occur within a context. As such, reusing patterns improves both quality and time-to-market of software projects. Currently, most patterns are specified in an informal fashion, which gives rise to ambiguity, and limits tool support and correct usage. This chapter describes balanced pattern specification language (BPSL), a language intended to accurately describe patterns in order to allow rigorous reasoning about them. BPSL incorporates the formal specification of both structural and behavioral aspects of patterns. Moreover, it can formalize pattern composition and instances of patterns (possible implementations of a given pattern).