Achieving consistency and reusability in presentation layer design using formal methods and design patterns

Published: Last Edited:

This essay has been submitted by a student. This is not an example of the work written by our professional essay writers.


The discipline of software engineering was born out of necessity. During the 1960's, the capabilities of computer hardware and end user expectation grew tremendously. Newer approaches that were more scalable and better defined were required for building larger and more complex software systems in a quicker and cost effective way. These approaches form the software engineering discipline. Software architecture design is a vital component of software engineering and deals with designing software specifications of software systems. A good software design must be simple, consistent, reusable and repeatable.

Design patterns, which are the basis of modern software architecture design, play a vital role in achieving the above mentioned desired characteristics. The patterns discussed in this paper can be classified as "enterprise application design patterns" due to their role in the development of modern object oriented enterprise applications. In this paper, we propose modeling enterprise patterns using formal methods. Formal methods are mathematical techniques based on the principles of set theory and predicate logic which are used to build verifiable models of computerized software systems. It is expected that the combination of patterns and formal methods will result formal reusable software building blocks. We believe that when these components will be used for modeling really complex systems, it must retain the formal essence of its basic constructs.

The fusion of formal methods with software architecture and design patterns is not a new concept. This can be seen from the works on formalizing software architectures that show that an Architecture Description Language based on a formal abstract model of system behavior can provide a practical means of describing and analyzing software architectures and architectural styles [1]. Alencar et al., have introduced a formal approach to model design patterns at many different architectural levels including pipes-and-filters design pattern, layered system and others [2]. Extensive work has been done to formally model behavioral design patterns [3], [4] and object oriented frameworks [5]. New formal languages have been proposed specifically for describing and reasoning about object oriented software architectures, designs, and patterns. In [6], an example of such languages is discussed. Our work, however, is on patterns used in building enterprise applications, particularly, the presentation layer, which is different from what has been done so for.

Formal model of "intercepting filter" and the "front controller" design pattern are described in this paper. The intercepting filter pattern is similar to the "pipes and filters" architectural style in which the application can have a set of pre and post processors that act on any incoming request. The front controller pattern, however, is a delegation pattern that delegates processing responsibility based on the nature of the request. Rest of the paper is structured as given below.

In sections II, significance of software design patterns is argued. In section III, the use of design patterns in enterprise applications is discussed. An identification of relationship between formal methods and design patterns is done in section IV. In section V, formalization of the design patterns is described using VDM++. Finally, conclusion and future work are discussed in section VI.

II. Significance Of Software Design Patterns

The use of patterns in any field indicates progress of human understanding [7]. In computer science, rather more specifically in software engineering, patterns are a key element of software architecture because patterns can be used to derive architectures, such as a mathematical theorem can be proved from a set of axioms [8]. Software design patterns are a mechanism for expressing recurrent design structures [4] and can be repeatedly used to address similar design problems in similar architectures. Design patterns have been extracted and repetitively applied in diverse sub domains such as software architecture [9], general object oriented designs [10], web applications development, enterprise application development [11], enterprise application integration [12], software implementation [13], software development for portable devices [14], embedded systems [15] and many more.

An object oriented design pattern is "a reusable and abstract solution to a commonly occurring design problem". This solution is defined in terms of classes, their instances, the relationships between the instances and the delegation of responsibility amongst them [4]. The most important term in this definition is "design problem". A design problem relates to the structural, creational, behavioral or other aspects of a software system as opposed to the algorithmic or computational aspects. We can classify design patterns on the basis of the problem to be solved. For example, structural patterns define ways to compose objects to obtain new functionality of a system. Similarly, creational patterns address issues related to object construction. The behavioral patterns are specifically concerned with the communication between the objects of a system [16].

Some other properties of the software design patterns can be listed as: (i) are abstract, (ii) cannot be coded but have their implementations, (iii) are well documented and their use improves the readability of the code which in turn increases maintainability, (iv) promote reusability, and (v) increase compliance to the object oriented principles.

III. Design patterns in Enterprise Applications

Enterprise software applications provide internal services to an enterprise in some focused business domain such as human resource or accounting, or could also provide services to customers of the enterprise in question. Being a class of computer software, all enterprise applications share a certain set of properties which are discussed below.

Modern enterprise applications are distributed, multi-tiered and modular in nature and need to have high reliability. All enterprise applications have a data source which in most cases is a relational database management system (RDBMS) but can also have other sources such as XML, Excel etc. Multiple data sources are common and access to it will be required by hundred of concurrent users. Enterprise applications often interact with other software systems to access data or delegate computational responsibility. All these aspects of enterprise applications make designing and maintaining an enterprise application a challenge. While developing enterprise applications, the focus is on a good structural design which is easily maintainable.

One of the ways to organize an application is by dividing the functionality into layers. Typical examples are the operating system, the logical OSI network layers etc. Enterprise applications are frequently divided into layers each of which performs a specific and well defined functionality. The outermost layer of an enterprise application is the presentation layer which serves the purpose of an interface between the application and the outside world. Typically this is a graphical user interface meant for a human user. Other interfaces may exist as well. Next is the service layer, also known as the business layer, which performs the core functionality of the system. The data access layer hides the data source from the service layer allowing us to change the data source without impacting the rest of the application. The data source could be a relational database system, flat files, a directory, or a remotely accessible external system.

The layering mechanism increases modularity, decreases unnecessary coupling between components, increases cohesion and promotes reusability, resulting in a maintainable and well structured system. Merits of a layered approach in design an enterprise application and how this architecture evolved are discussed in detail by Fowler [11]. Patterns that specifically relate to building enterprise applications are known as enterprise design patterns. The patterns that belong to the enterprise suite are always limited to a layer of the application. In this paper, we present the formal model of two most useful presentation layer design patterns, the "Intercepting Filter" and the "Front Controller". These patterns are a part of the enterprise pattern catalog [17] published by Sun Microsystems.

IV. Formal Methods and Design Patterns

Formal methods constitute a branch of software engineering that incorporates the use of mathematics, specifically, discrete mathematics, for software development. Bowen describes the importance of formal methods in the following way. "Just because a system has passed unit and system testing, it does not follow that the system will be bug free. That is where formal methods offer considerable advantageous over more traditional methods when developing systems where high integrity is required. Formal methods allow us to propose properties of the system and to demonstrate that they hold. They allow us to examine the system behavior and convince ourselves that all possibilities have been anticipated [18]."

Due to increasing influence of computers in all aspects of our lives, and the fact that modern computer hardware allows complex computer systems to be developed [19], the impact of failure of such systems has increased. Critical systems can be divided into three broad categories. Safety critical systems are those whose failure results in human injury or loss of life. Business critical systems impact the financial standing of an enterprise. Finally, mission critical systems are whose failure impairs the goal of a given mission [20].

"If formal modeling is applied at the level of style, analyses can be extended to any system that conforms to the style [1]". This statement best captures the motivation for formalizing design patterns. In software development, the "level of style" is the design of the system which is expressed in terms of a multitude of patterns. When these patterns are formalized and then implemented, their implementations inherently contain the original analyses that were made during the formalization of the pattern. This "trickling down" of formal detail from an abstract design pattern to a concrete implementation is the primary impetus for formalizing patterns.

Our focus is on enterprise applications patterns which lie squarely in the domain of business critical systems. Most enterprise applications handle large amounts of data on which complex processes and rules operate on [11]. Failure on part of the application to provide reliable and accurate services to the stakeholders may result in irreversible damage to the financial status or the well being of the enterprise. Hence, it is logical to apply formalism to the most basic design construct of such applications, for example, the enterprise application design patterns. It proves that there is a good used of formal techniques in enterprise applications. Uniformity and consistency of modeling approaches is desired in software development. Consider an enterprise application which we model using a combination of formal techniques and informal techniques. When implemented, our application will surely contain a large number of open source and commercial components and frameworks resulting in a mix of formalism and in-formalism in our code base. We believe that such a mix is undesirable because a faulty component used in our system may cause our critical system to collapse. Therefore, the best case scenario would be for framework developers to use formal design patterns to model their wares resulting in an all encompassing formal model. Another way to put across this idea is through the well known English idiom, "a chain is only as strong as its weakest link". The chain in our analogy is our attempt to create a mathematically verifiable and correct model of an enterprise application. The weak links are the informally developed components used to actually build our system.

V. Formalizing Design Patterns

The structure of the pattern is a sequence of relationships between classes which are defined in terms of a UML sequence diagram. These relationships are well defined. Any implementation of a pattern can only be verified for compliance with the original pattern if the implementation's structure is the same as of the pattern. Our formalization methodology works on the concept discussed above. VDM++, which is an object oriented formal language is used to model our base object orientation model and patterns.

A. Formal Specification of Object Orientation

The architectural basis of software system design is design patterns whereas the base of design patterns is object orientation. Our efforts to formalize design patterns would be flawed and incomplete if we do not formalize object orientation first. This approach has been adopted by several others who have formalized patterns [4], [3]. We have intentionally kept the scope of our object oriented formal model limited as opposed to more comprehensive approaches pursued by other researchers. Only those concepts of object orientation that are core to our work have been formalized currently. This model however will be expanded as part of our future work.

Method Signature

class MethodSignature


parameter :: token

instance variables

accessModifier : Visibility;

name : Global'mSignature;

parameters : set of parameter;

returnType : token;

end MethodSignature

Interface: An interface can be considered as a set of method signatures. We ensure as part of the pre condition that the same signature is not repeated in a given interface.

class Interface

instance variables

public signatures : set of signature;

public name : Global'interfaceName;


addMethodSignature(sig : Signature)

ext rd signatures

pre sig not in set signatures

post signature = signature union {sig};

end Interface

Class Definition: An object oriented class can be considered as a set of interfaces which the class implements and a set of signatures that are part of the class definition.

class ClassDef

instance variables

name : seq of char;

interfaces : set of Interface;

signatures : set of Signature;


containSignature()b : bool

ext rd signatures : set of Signature

pre sig <> null and len signatures>0

post true;

end ClassDef

Relation: A relationship class describes the type of relationship that could exist between two given classes. Patterns discussed in this paper can be modeled by defining association relationships between the participating classes. These relationships are dictated by the pattern structure.

class Relation


relations = Association | Aggregation | Composition;

instance variables

relationship : (ClassDef-> ClassDef)-> relations

end Relation

Pattern: An object oriented design pattern can be considered as a sequence of called methods or operations. The specification described below has an operation by the name of isValidPattern. It checks if the sequence of relationships of a particular pattern is valid or not.

class Pattern


pType = InterceptingFilter | FrontController;

instance variables

relations : seq of Relation;



ext wr relations : seq of Relation

pre rel <> null and rel not in set relations

post relations = relations ^ [rel];

isValidPattern(relation : Relation`relations, classA : ClassDef, classB : ClassDef)flag:bool

ext rd relations : seq of Relation

pre elems relations > 0

post forall r in set relations &

rel(classA,classB,relation) in set r(i).relationship;

end Pattern

B. Formalization of Enterprise Presentation Layer Patterns

1) Intercepting Filter Pattern

The intercepting filter pattern is the first pattern of the presentation layer. The primary inspiration of it is to have multiple preprocessors or "filters" each of which performs a specific and well defined task. In essence this design pattern is the preprocessor variant of the "pipes and filters" architectural style [21] useful in applications that receive input from external world in the form of HTTP requests. The same pattern is also used frequently for post processing. Examples of this could be compressing or encrypting responses to the original requestors.

The best way to describe the interceptor filter pattern is via the airport analogy. For example, a passenger has to board a flight but before he is able to travel, he has to complete a number of predefined and sequential activities. Each of these activities is unrelated and independent of each other. Only once a passenger has passed through these preliminary steps successfully is he able to board the flight which happens to be his actual goal. Transforming UML sequence diagram to mathematical relations results in the following:

((Class â†" Class) â†" Relation Type)

1 ((Client, Filter Manager), Association)

2 ((Filter Manager, Filter Chain), Association)

3 ((Filter Chain, Filter), Association)

4 ((Filter Chain, Target), Association)

Intercepting Filter Pattern: The intercepting filter pattern is a subclass of pattern. The isValidPattern method of the parent class is used to validate the pattern.

class InterceptingFilter is subclass of Pattern


isValidPattern(relation : Relation`relations, classA : ClassDef, classB : ClassDef)flag:bool

pre true

post Pattern` isValidPattern(relation, classA, classB);

end InterceptingFilter

Filter Chain: The filter chain class is a component class of the pattern and is a subclass of the ClassDef class. The filter chain is composed of a sequence of filters. Each filter is called in order and is validated in the processFilter operation.

class FilterChain is subclass of ClassDef

instance variables

public filters : seq of Filter;


containSignature()b : bool

pre true

post ClassDef`containSignature();

addFilter(filter : Filter)

ext rd filters : seq of Filter

pre filter not in set filters

post filters = filters ^ [filter];

processFilter(request : token,response : token)

ext rd filters : seq of Filter

pre elems filters > 0

post let filter = hd filterChain and filterChain = tl filterChain in filter.containSignature(sig) and filter.doFilter(request,response, filterChain);

end FilterChain

Filter: The filter class is another component of the intercepting filter design pattern. Every filter called has its own structure validated from isWellDefinedClass operation.

class Filter is subclass of ClassDef

instance variables

name:seq of char;

interfaces : set of Interface;


containSignature()b : bool

pre true

post ClassDef`containSignature()


pre let fClass = mk_ ClassDef(name,interfaces) in isWellDefinedClass(fClass) and containSignature()

post TRUE;

doFilter(servletRequest:token,servletResponse:token,filterChain: FilterChain)

pre let fClass = mk_ ClassDef(name,interfaces) in isWellDefinedClass(fClass) and containSignature()

post TRUE;

end Filter

Filter Manager: The filter manager class contains the filter chain. The process filter operation is used to start the execution process.

class FilterManager is subclass of ClassDef

instance variables

filterChain : FilterChain;


containSignature()b : bool

pre true

post ClassDef`containSignature();

processFilter(filter : Filter,request : token , response:token)

pre filterChain <> null

post filtersChain.processFilter(request, response) and let target = mk_ Target() in target.execute(request ,response);

end FilterManager

Target: The target class is the final one called after all filters are successfully called and executed.

class Target



pre true

post true

end Target

2) Front Controller Pattern

Once, a requestor's request has passed through the intercepting filter, the request is handled by the front controller pattern. The front controller pattern primarily deals with delegation of computational responsibility based on the nature of the problem to be computed.

For example, a bank serves as an analogy for the front controller design pattern. Based on the type of request, the receptionist guides the customer to the relevant desk where his request is fulfilled. Transforming UML sequence diagram to mathematical relations results in the following:

((Class â†" Class) â†" Relation Type)

1 ((Client, Controller), Association)

2 ((Controller, Dispatcher), Association)

3 ((Controller,View), Association)

4 ((Controller, Helper), Association)

Client: Like the previous pattern, the client class is checked if it's well defined. The doGet operation is the entry point of execution for a client request.

class ClientPage is subclass of ClassDef

instance variables

controller : Controller;


containSignature()b : bool

pre true

post ClassDef`containSignature();

public doGet(HttpServletRequest : token, HttpServletResponse : token)

pre controller <> null and

let fClass = mk_ClassDef(, controller.interfaces)

in isWellDefinedClass(fClass) and


post controller. processResponse(HttpServletRequest, HttpServletResponse);

end ClientPage

Controller: The controller class, which is a major component of the front controller pattern, is checked for class validity. Similarly, the other classes, i.e., dispatcher, helper and command have simple checks for structure validity.

class Controller is subclass of HttpServlet

instance variables

page : View;

name:seq of char;

interfaces : set of Interface;


public init(ServletConfig : token)

pre true

post HttpServlet'init(ServletConfig);

public processResponse(HttpServletRequest : token, HttpServletResponse : token)

pre true

post let helper = mk_ RequestHelper()

in let command = helper.getCommand() in

command.containSignature() and

page = command.execute(HttpServletRequest, HttpServletResponse) and

page.containSignature()and dispatch(HttpServletRequest, HttpServletResponse,page);

public dispatch(HttpServletRequest : token, HttpServletResponse : token)

pre true

post true;

end Controller


class RequestDispatcher is subclass of ClassDef


containSignature()b : bool

pre true

post ClassDef`containSignature();

public forward(HttpServletRequest : token, HttpServletResponse : token)

pre HttpServletRequest<>null

post true;

end RequestDispatcher


class RequestHelper is subclass of ClassDef

instance variables

httpServletRequest : token;

command : Command;


containSignature()b : bool

pre true

post ClassDef`containSignature();

public getCommand()c:Command

pre true

post c = command;

end RequestHelper


class Command is subclass of ClassDef

instance variables

page : View;


containSignature()b : bool

pre true

post ClassDef`containSignature();

public execute(HttpServletRequest : token, HttpServletResponse : token)mypage: View

pre HttpServletRequest<>null and HttpServletResponse<>null

post mypage = page;

end Command

VI. Conclusion

In this paper, we have presented a formal specification of two enterprise presentation layer design patterns. The objective of this research is proposing approaches to formalize systems at an abstract design level rather than giving its implementation detail at the early stages of system's development. As formal methods are powerful at an abstract level, that is why, their use will increase reusability of the formal specification of the design for any of its implementations in addition to increasing confidence ensuring its correctness. We observed that the formal nature of this design will trickle down to any implementation of the design of a system. After formal description of design patterns, we believe that these reusable components will result in consistent and uniform architectures that use formalism across the entire application instead of just formal custom code supported by informal reusable components.

We proposed a formal methodology rather a detailed approach followed in [9], [3]. We first provided a formal specification of the basic object oriented constructs and then reused it while constructing formal models of the patterns. Some similar work can be found in [22], [23], [24] which was taken as starting point for this resaerch.

The relative ease by which we were able to formalize our patterns using VDM++ can be attributed to the fact that an object oriented formal specification language was used to model object oriented constructs and concepts. A lot of concepts, that we would have had to model ourselves in a non-object oriented language such as Z, came inherently while using VDM++. The formal description of the next layer design pattern of the enterprise suite is under progress and will appear soon in our future work.

VII. References

[1] Allen, R. J., "A Formal Approach to Software Architecture", CMU Technical Report CMU-CS-97-144, Vol. 6, 1997.

[2] Alencar, P.S.C., Cowan, D.D. and Lucena, C.J.P., "A Formal Approach to Architectural Design Patterns", FME96: Industrial Benefit and Advances in Formal Methods, 1996.

[3] Reynoso, L. and Moore, R., "Gof Behavioral Patterns: A Formal Specification", United Nations University, International Institute for Software Technology, 2000.

[4] Cechich, A. and Moore, R., "A Formal Specification of GoF Design Patterns", International Institute for Software Technology, The United Nations University, Vol. 1, 1999.

[5] Crnkovic, I., et al., "Object Oriented Design Frameworks: Formal specification and some Implementation Issues", Proc. Of 4th IEEE Int'l Baltic Workshop, 2000.

[6] Eden, A.H., "Formal Specification of Object-Oriented Design", International Conference on Multidisciplinary Design in Engineering CSME-MDE, Montreal , 2001.

[7] Coad, P., "Object Oriented Patterns", Communications of the ACM, Vol. 5 (4), p102-103, 1994.

[8] Beck, K., and Johnson, R., "Patterns Generate Architectures", ECOOP'94, Springer-Verlag, 1994.

[9] Shaw, M., "Some Patterns for Software Architecture", Vlissides, Coplien & Kerth (eds.), Pattern Languages of Program Design, Vol. 2, Addison-Wesley, pp. 255-269, 1996.

[10] Gamma, E., Helm, R. Johnson, R and Vlissides, J., "Design Patterns: Elements of Reusable Object Oriented Software", Addison Wesley Professional Computing Series, 1995.

[11] Fowler, M., "Patterns of Enterprise Application Architecture" Addison-Wesley, 2003.

[12] Hohpe, G. Woolf, B., and Brown, K., "Enterprise Integration Patterns: Designing, Building, and Deploying Messaging Solutions", Addison-Wesley, 2004.

[13] Beck, K., "Implementation Patterns", Addison-Wesley, 2008.

[14] Narsoo, J., and Nawaz M., "Identification of Design Patterns for Mobile Services with J2ME", The Journal of Issues in Informing Science and Information Technology, Vol. 5, 2008.

[15] Gay, D., et al., "Software Design Patterns for TinyOS", ACM Trans, Embedd Computing, Vol. 6 (4), 2007.

[16] Bowen, J.P., and Stavridou, V., "Safety-Critical Systems, Formal Methods and Standards", IEE/BCS Software Engineering Journal, Vol 5, 1993.

[17] Alur, D., Crupi, J., and Malks, D., "Core J2EE Patterns: Best Practices and Design Strategies", Prentice Hall/Sun Microsystems Press, 2003.

[18] Bowen, P., and Hinchey, M., "Ten Commandments of Formal Methods", IEEE Computer Society, Vol. 10, 1995.

[19] Bowen, J., Stavridou, V. P., "Safety-Critical Systems, Formal Methods and Standards", IEE/BCS Software Engineering Journal, Vol. 1(2) 1993.

[20] Charatan, Q., and Kans, A., "Formal Software Development from VDM to Java", Palgrave Macmillan, 2003.

[21] Garlan, D., and Shaw, M., "An Introduction to Software Architecture", CMU Software Engineering Institute Technical Report, CMU/SEI-94-TR-21, ESC-TR-94-21, Vol. 6, 1994.

[22] Reza,H. and Grant, E., "A Formal Approach to Software Architecture of Agent-base Systems", Int'l Conference on Information Technology, Vol. 1, pp. 591-595, 2004.

[23] Dong, J., et al., "Composing Pattern-based Components and Verifying Correctness", Journal of Systems and Software, Vol. 80 (11), pp. 1755-1769, 2007.

[24] Taibi, T., "Formal Specification of Design Patterns Relationships", Proc. of 2nd Int'l Conference on Advances in Computer Science and Technology, pp. 310-315, 2006.