Kiểm chứng phần mềm có một vai trò quan trọng trong việc đảm bảo tính đúng đắn của hệ thống phần mềm trong suốt quá trình thực thi,kiểm chứng giúp phát hiện,tìm ra lỗi và thông báo lỗi cho nhà phát triển. 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 ramột hướng phát triển mới cho kiểm chứng phần mềm, giúp nâng cao khả năng dò tìmlỗi, thông báo lỗimà không ảnh hưởng tới mã nguồn hệ thống. Trong thực tế, biểu đồ UML là sự lựa chọn rất phổ biến cho việc mô hình hóa hệ thống phần mềm ở giai đoạn thiết kếhiện nay.Trong đó, biểu đồ tuần tự (sequence diagram) là một biểu đồ quan trọng, nó miêu tả các cách thức đối tượng tương tác và giao tiếp với nhau.Việc kiểm chứng thiết kếvà kiểm chứng các giao thức ràng buộc trong biểu đồ trình tựlà rất cần quan trọngvì nếu thiết kế biểu đồ tuần tự sai kéo theo các hoạt động của hệ thống hoặc trình tự hệ thống cần thực hiện sẽ bị sai dẫn tới toàn bộ hệ thống thiết kế sai. Trong phạm vi khóa luận, tôixin 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 từ biểu đồ tuần tự kết hợp với máy trạng thái và công cụtự động sinh mã aspect dựa trên phương pháp này. Mã aspect tạo ra từ công cụ có thể dùng đan vào chương trình để thực hiện nhiệm vụ kiểm chứng các ràng buộc giữa các đối tượngvà tính đúng đắn của hệ thốngnhằm giảm thiểu tối đa lỗi khi viết mã cài đặt cho hệ thống