Verified Operational Patterns with Graph Transformation

Using object-oriented patterns such as design patterns, architectural patterns, and refactoring operations has considerably simplified the design process of software systems. With the proliferation of Domain-Specific Languages, the generalization of OO patterns is a natural demand. A straightforward idea is to adapt OO patterns with automated tool support to the practice of Domain-Specific Modeling as well. A possible solution for that is using graph transformations to formalize and realize such patterns. One may expect, however, that the patterns are realized in a way that they are correct and do exactly what we expect them to. In this paper, we present how one can precisely define the requirements for a domain-specific model pattern, and how to verify the requirements on the implemented patterns. The presented concept is motivated and illustrated with a case study from the state chart domain.