Automated verification of design patterns: a case study

Representing design decisions for complex software systems, tracing them to code, and enforcing them throughout the lifecycle are pressing concerns for software architects and developers. To be of practical use, specification and modeling languages for software design need to combine rigor with abstraction and simplicity, and be supported by automated design verification tools that require minimal human intervention. This paper examines closely the use of the visual language of Codecharts for representing design decisions and demonstrate the process of verifying the conformance of a program to the chart. We explicate the abstract semantics of segments of the Java package java.awt as a finite structures, specify the Composite design pattern as a Codechart and unpack it as a set of formulas, and prove that the structure representing the program satisfies the formulas. We also describe a set of tools for modeling design patterns with Codecharts and for verifying the conformance of native (plain) Java programs to the charts.