Phần mềm ngày càng được xây dựng và phát triển mạnh mẽ. Phần mềm được tạo ra phải đảm bảo chất lượng. Kiểm chứng phần mềm là một trong những giai đoạn quan trọng trong quy trình sản xuất phần mềm. Kiểm chứng động phần mềm nhằm phát hiện và tìm lỗi trong giai đoạn kiểm thử phần mềm. Phương pháp lập trình hướng khía cạnh ( Aspect Oriented programming - AOP) cùng với công nghệ AspectJ ra đời tạo ra hướng phát triển mới cho kiểm chứng phần mềm, nâng cao khả năng tìm và sửa lỗi phần mềm mà không ảnh hưởng đến mã nguồn hệ thống. Từ yêu cầu thực tế, khi mô hình UML đang là sự lựa chọn phổ biến cho mô hình hóa hệ thống phần mềm ở giai đoạn thiết kế, việc kiểm chứng các ràng buộc giữa các tương tác trong biểu đồ trình tự UML là rất cần thiết. Cùng với yêu cầu thực tế đề ra và lựa chọn AOP là giải pháp giải quyết vấn đề, trong phạm vi khóa luận, tôi xin trình bày phương pháp sinh mã AspectJ tự động phục vụ cho việc kiểm chứng phần mềm với công cụ là plugin Create Aspect tự động sinh mã AspectJ dựa trên phương pháp này. Nội dung chính của phương pháp này dựa trên các kiến thức về AOP, UML, XML, ANNOTATIONS để chuyển đổi các giao thức ràng buộc đối tượng đặc tả bời biểu đồ UML sang modun aspect phục vụ cho việc kiểm chứng. Ý nghĩa thực tiễn là việc sinh ra mã aspect sẽ đan xen vào chương chình thực hiện việc kiểm chứng các ràng buộc giữa các đối tượng trong thời gian chạy.
