Earticle

초록

영어

Design patterns capture elegant design solutions and facilitate reuse in design level. In the Component Based Software Engineering (CBSE), design patterns were treated as design components, which serve as elemental components and can be composed to construct a large software system. In the process of composition, the key problem is how to ensure the correctness of composition. To address this problem, a criterion for correct composition is needed. The well known “faithfulness” principle is chosen as the correctness criterion and our discussions are based on this principle. In this paper, we at first use First Order Logic to model some elemental entities and relations in Object Oriented Design, which serve as an ontology in the domain. Then using the vocabulary in the ontology, we formally specify design patterns and formalize the “faithful” principle as theorems in Coq. Finally, we prove the theorems and thus show the correctness of composition. As a case study, we described and verified the composition of Composite pattern and Decorator pattern. Once a composition is proven to be correct, one can use the composition repeatedly. This would facilitate reuse of design in a larger scale and reduce errors in design phase, which justifies all the efforts of verifying their correctness.

목차

Abstract
 1 Introduction
 2 Related Works
 3 Problem Illustration
 4 The Formal Proof
 5 Conclusions and Future Work
 References

키워드

저자

• Qiang Liu [ Department of Computer Science and Technology, East China Normal University ]
• Zongyuan Yang [ Department of Computer Science and Technology, East China Normal University ]
• Jinkui Xie [ Department of Computer Science and Technology, East China Normal University ]

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of Control and Automation

• 간기

  월간

• pISSN

  2005-4297

• 수록기간

  2008~2016

• 십진분류

  KDC 505 DDC 605