A Generic Model of Object-Oriented Patterns Specified in RSL

Abstract

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).