Verifying behavioral correctness of design pattern implementation

Design pattern describes a recurring problem and its common solution, which usually is in abstract form. The application of design pattern requires coding the generic solution. It is necessary to assure the coding process correctly implements not only the structure but also the desired behavior of the design pattern. This problem is called implementation correctness in this paper. By providing the definition of partial order between sequence diagrams, we formally describe the implementation correctness. We verify the implementation correctness with model checking by using process algebra to specify the source code and temporal logic to specify the behavior of the pattern.