- Tên đề tài luận văn: Nghiên cứu về kiểm chứng bất biến của đối tượng sử dụng lập trình hướng khía cạnh.. - Đã nghiên cứu phương pháp lập trình hướng khía cạnh (Aspect-Oriented Programming - AOP). - Khảo sát những ưu, nhược điểm của phương pháp lập trình này và khả năng ứng dụng vào kiểm chứng bất biến của đối tượng tại thời điểm thực thi.. - Đã đề xuất các cách tiếp cận mở rộng để kiểm chứng bất biến của đối tượng Java tại thời điểm thực thi sử dụng phương pháp lập trình hướng khóa cạnh (AOP) và cài đặt thực nghiệm trên các ví dụ minh họa. - Trong tiếp cận này, một ứng dụng hướng đối tượng được thiết kế bởi UML/OCL và được cài đặt bằng ngôn ngữ Java. - Các bất biến của các đối tượng Java sẽ được kiểm chứng tự động tại thời điểm thực thi bởi các mã aspect đã được đan kết. - Các mở rộng bao gồm sự thừa kế các ràng buộc trong AspectJ, kiểm chứng bất biến của lớp con có ràng buộc thay đổi so với lớp cha và kiểm chứng bất biến liên quan đến thuộc tính được thêm vào lớp con.. - Đã nghiên cứu công cụ kiểm chứng mô hình cho các chương trình Java là Java PathFinder (JPF), đặc biệt là phần mở rộng của nó là thực thi ký hiệu dùng để sinh tự. - động các ca kiểm thử cho các phương thức, các thuộc tính của đối tượng Java trong chương trình hướng đối tượng Java.. - Sử dụng thực thi ký hiệu để sinh tự động các ca kiểm thử cho các phương thức trong ví dụ minh họa nhằm kiểm tra lại các aspect dùng để kiểm chứng bất biến.. - Đã trình bày phương pháp kiểm chứng bất biến của đối tượng sử dụng phương pháp chèn các khẳng định vào mã nguồn Java. - Sau khi các khẳng định được chèn vào mã nguồn Java và được thực thi bởi công cụ kiểm chứng mô hình JPF thì JPF sẽ thông báo vi phạm đầu tiên nó gặp phải và dừng quá trình thực thi.. - Khả năng ứng dụng trong thực tiễn: hình thành phương pháp kiểm chứng bất biến của đối tượng tại thời điểm thực thi sử dụng lập trình hướng khía cạnh với các quan hệ kế thừa.. - Những hướng nghiên cứu tiếp theo: Trong thời gian tới, chúng tôi tiến hành cài đặt hoàn thiện công cụ kiểm chứng cho phương pháp AOP. - Chúng tôi cũng mong muốn phát triển một công cụ để sinh các aspect kiểm chứng tự động cho tất cả các bất biến ứng với tất cả các lớp dựa trên các quan hệ của các lớp và các biểu thức OCL được lưu trữ trong các định dạng tệp tin cụ thể đối với phương pháp kiểm chứng bất biến sử dụng AOP.. - Đồng thời chúng tôi cũng muốn phát triển một công cụ để thực hiện việc chèn các khẳng định một cách tự động vào các chương trình nguồn Java tương ứng nhằm làm đầu vào cho công cụ kiểm chứng mô hình JPF.