Trong quy trình phát triển phần mềm, kiểm chứng phần mềm đóng vai trò quan trọng trong việc đảm bảo tính đúng đắn của hệ thống trong suốt quá trình thực thi. Nó có nhiệm vụ phát hiện và dò tìm lỗi cho giai đoạn kiểm thử phần mềm. Phương pháp lập trình hướng khía cạnh (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, giúp nâng cao chức năng dò tìm, sửa lỗi phần mềm mà không ảnh hưởng tới mã nguồn hệ thống. Từ yêu cầu thực tế, khi mà mô hình UML đang là sự lựa chọn phổ biến cho việc 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 giao thức ràng buộc đối tượng, giao thức ràng buộc giữa các tác tử trong hệ đa tác tử được mô tả trong biểu đồ trạng thái và biểu đồ trình tự UML, AUML là rất cần thiết trong thời gian chạy. Dựa vào yêu cầu thực tế đặt ra cùng với việc lựa chọn AOP làm 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ã aspect phục vụ cho mục đích kiểm chứng phần mềm và xây dựng công cụ Protocol Verification Generator (PVG) tự động sinh mã aspect dựa trên phương pháp này. Nội dung chính của phương pháp là dựa vào các kiến thức về AOP và UML, XML, AUML, JADE framework để chuyển đổi các giao thức ràng buộc đối tượng được đặc tả bởi biểu đồ UML, giao thức tương tác giữa các tác tử trong hệ đa tác tử được đặc tả bởi biểu đổ AUML sang các mô-đun aspect phục vụ quá trình kiểm chứng. Ý nghĩa thực tiễn của bài toán là việc sử dụng mã aspect vừa được tạo ra đan vào chương tr ình chính thông qua b ộ đan (aspect weaver) của AspectJ để thực hiện nhiệm vụ kiểm chứng các giao thức ràng buộc giữa các đối tượng, các tác tử trong thời gian chạy