Ian Stark

Automatic Verification of Java Design Patterns

Alex Blewitt, Alan Bundy and Ian Stark

In ASE '01: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, November 26-29, 2001, San Diego, California, pages 324-327. IEEE Computer Society Press, 2001.

Fetch paper (PDF, 48k). Go to other papers, talks or home page.

Abstract

Design patterns are widely used by object oriented designers and developers for building complex systems in object oriented programming languages such as Java. However, systems evolve over time, increasing the chance that the pattern in its original form will be broken.

We attempt to show that many patterns (implemented in Java) can be verified automatically. Patterns are defined in terms of variants, mini-patterns, and constraints in a pattern description language called Spine. These specifications are then processed by Hedgehog, an automated proof tool that attempts to prove that Java source code meets these specifications.

@InProceedings{blewitt/bundy/stark:autvjd,
  author =       {Alex Blewitt and Alan Bundy and Ian Stark},
  title =        {Automatic Verification of {Java} Design Patterns},
  booktitle =    {ASE~2001: Proceedings of the 16th IEEE International
                  Conference on Automated Software Engineering},
  pages =        {324--327},
  year =         2001,
  number =       nov,
  publisher =    {IEEE Computer Society Press},
  url =          {http://www.inf.ed.ac.uk/~stark/autvjd.html},
  pdf =          {http://www.inf.ed.ac.uk/~stark/autvjd.pdf}
}

Page last modified: Tuesday 5 August 2008