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

Abstract

Các kết quả thu được trong quá trình thực hiện luận văn được thể hiện ở những nội dung chính sau đây: • Đã 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.