Description and Verification of Pattern-Based Composition in Coq - Advances in Computational Science and Engineering - page 244

Method. These relations are static relations, which, once coded in the program, cannot
be changed during the run time. Clearly, these relations are just suitable for modeling
the structural aspect of design patterns. To model behavioral aspects of design pat-
terns, we should concern relations about Objects. Many authors [4][6] use temporal
logic, like Temporal Logic of Action [9], to formalize the behavioral aspect of design
patterns. It is our future concern to integrate these two aspects in Coq.
Furthermore, to achieve a higher level of automation in the proving of composition,
we should develop a GUI tool to convert UML diagrams to Coq scripts. Usually, the
graphical representation of design patterns in UML can be easily exported to XMI for-
mat. Then we need to convert this format to the scripts in Coq. This would hide details
about Coq from designers, thus improve the work efficiency of system designers.
References
1. Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming
Languages and Systems 15(1), 73-132 (1993)
2. Moriconi, M., Qian, X., Riemenschneider, R.A.: Correct architecture refinement. IEEE
Transactions on Software Engineering 21(4), 356-372 (1995)
3. Tommi, M.: Formalizing design pattern. In: Proceedings of the 20th International Confer-
ence on Software Engineering, pp. 115-124 (1998)
4. Taibi, T., Ngo, D.C.L.: Formal specification of design pattern combination using BPSL.
International Journal of Information and Software Technology (IST) 45(3), 157-170
(2003)
5. Eden, A.H., Hirshfeld, Y.: Principles in formal specification of object-oriented architec-
tures. In: Proceedings of the 11th CASCON, Toronto, Canada (November 2001)
6. Dong, J., Alencar, P., Cowan, D.: Ensuring structure and behavior correctness in design
composition. In: Proceedings of the 7th Annual IEEE International Conference and Work-
shop on Engineering of Computer Based Systems (ECBS), Edinburgh UK, pp. 279-287
(2000)
7. Keller, R., Reinhard, S.: Design components: towards software composition at the design
level. In: Proceedings of the 20th International Conference on Software Engineering, pp.
302-311 (1998)
8. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns, Elements of Reusable
Object-Oriented Software. Addison-Wesley Publishing Company, Reading (1995)
9. Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Lan-
guages and Systems 16(3), 873-923 (1994)
10. Coquand, T., Huet, G.: The calculus of constructions.Technical Report 530, INRIA (1986)
11. Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical
Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)
12. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq'Art:
The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science.
Springer, Heidelberg (2004)
13. Alencar, P., Cowan, D., Lucena, C.: A formal approach to architectural design patterns. In:
Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 576-594.
Springer, Heidelberg (1996)