Automated verification of design patterns: a case study

Jonathan Nicholson, Amnon H. Eden, Epameinondas Gasparisb, Rick Kazmanc

Research output: Contribution to journalArticlepeer-review


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.
Original languageEnglish
Pages (from-to)211-222
Number of pages12
JournalScience of Computer Programming
Issue numberPart B
Publication statusPublished - 1 Feb 2014


  • Object-oriented design
  • Modeling and specification
  • Automated verification
  • Visual languages
  • Design description languages


Dive into the research topics of 'Automated verification of design patterns: a case study'. Together they form a unique fingerprint.

Cite this