Tổng quan luận án

Luận án tiến sĩ với đề tài "Một số phương pháp kiểm chứng tái cấu trúc phần mềm" được nghiên cứu và thực hiện bởi nghiên cứu sinh Đào Thị Hường dưới sự hướng dẫn khoa học của PGS.TS. Trương Ninh Thuận, bảo vệ tại Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội vào năm 2018. Luận án thuộc chuyên ngành Công nghệ thông tin, định hướng chuyên sâu về Công nghệ phần mềm và Phương pháp hình thức (Formal Methods).

Tính cấp thiết của đề tài xuất phát từ thực tiễn phát triển phần mềm: tái cấu trúc (refactoring) là tiến trình cải thiện cấu trúc bên trong của phần mềm nhằm nâng cao khả năng đọc hiểu, bảo trì và mở rộng mà không làm thay đổi hành vi quan sát được từ bên ngoài. Tuy nhiên, các thao tác tái cấu trúc rất dễ phát sinh lỗi nếu người phát triển không tuân thủ nghiêm ngặt các quy trình và tiêu chuẩn kỹ thuật. Khoảng trống nghiên cứu then chốt được tác giả chỉ ra là: đa số các nghiên cứu và công cụ hỗ trợ tái cấu trúc hiện hành mới dừng lại ở việc tìm kiếm vị trí cần tái cấu trúc hoặc thực hiện các phép biến đổi cú pháp đơn thuần dựa trên ngôn ngữ tự nhiên và mô tả bán hình thức (semi-formal). Các công trình này chưa cung cấp khung lý thuyết toán học chặt chẽ để kiểm chứng tự động sự bảo toàn các ràng buộc bất biến (class invariants) trên biểu đồ lớp và sự bảo toàn hành vi (pre/post-conditions) của các kịch bản phần mềm xuyên suốt từ giai đoạn thiết kế mô hình đến giai đoạn cài đặt mã nguồn.

Mục tiêu nghiên cứu tổng quát của luận án là đề xuất các phương pháp hình thức nhằm kiểm chứng sự bảo toàn hai loại ràng buộc ngữ nghĩa cốt lõi trong hệ thống phần mềm hướng đối tượng khi thực hiện tái cấu trúc: ràng buộc bất biến của lớp và ràng buộc hành vi của kịch bản, đồng thời hiện thực hóa phương pháp thông qua việc xây dựng công cụ kiểm chứng tự động.

Nhiệm vụ nghiên cứu của luận án tập trung giải quyết 4 bài toán lớn trong tái cấu trúc phần mềm (được đánh số theo văn bản):

  1. Đánh giá ảnh hưởng của tiến trình tái cấu trúc trên các chỉ tiêu về chất lượng (Assessing the effect of refactoring on quality): Đo lường tác động đến độ phức tạp, khả năng hiểu, khả năng bảo trì, khả năng mở rộng và hiệu năng của phần mềm.
  2. Đảm bảo tiến trình tái cấu trúc bảo toàn hành vi (Guaranteeing that the refactoring preserves software behaviour): Hình thức hóa và kiểm chứng các điều kiện ràng buộc để đảm bảo chức năng và ngữ nghĩa của hệ thống không bị sai lệch sau biến đổi.
  3. Duy trì sự nhất quán giữa các thành phần phần mềm sau tiến trình tái cấu trúc (Maintaining consistency between refactored software components after refactoring process): Kiểm chứng tính nhất quán theo chiều ngang (horizontal consistency giữa phiên bản trước và sau tái cấu trúc) và tính nhất quán theo chiều dọc (vertical consistency giữa mô hình thiết kế và mã nguồn cài đặt).
  4. Xây dựng công cụ hỗ trợ trong quá trình tái cấu trúc (Tool supports for Refactoring): Phát triển công cụ tự động hóa việc kiểm tra tính nhất quán và bảo toàn hành vi của mô hình.

Đối tượng nghiên cứu của luận án là các kỹ thuật tái cấu trúc áp dụng trên các chế tác phần mềm hướng đối tượng, bao gồm: mô hình thiết kế (biểu đồ lớp - Class Diagram, biểu đồ tuần tự - Sequence Diagram), bản cài đặt mã nguồn Java, và các ràng buộc ngữ nghĩa (bất biến của lớp, tiền điều kiện và hậu điều kiện của phương thức).

Phạm vi nghiên cứu được xác định cụ thể:

  • Về mặt cấu trúc: Tập trung vào 5 phép toán tái cấu trúc liên quan đến mối quan hệ phân cấp trong kế thừa trên biểu đồ lớp UML gồm Folding, Abstraction, Composition, Factoring, và Unfolding.
  • Về mặt hành vi: Tập trung vào tiến trình tái cấu trúc có áp dụng mẫu thiết kế hành vi Strategy (thuộc nhóm mẫu GoF).
  • Về dữ liệu và thực nghiệm: Ứng dụng kiểm chứng trên mô hình hệ thống rút tiền tự động (ATM) và hệ thống điều khiển lưu lượng giao thông đường bộ thích ứng (Adaptive Road Traffic Control - ARTC).

Tổng quan tài liệu và vị trí của luận án

Luận án đã tổng hợp, phân loại và đánh giá có hệ thống các công trình nghiên cứu trong và ngoài nước liên quan đến các khía cạnh của tiến trình tái cấu trúc:

Hướng nghiên cứu Tác giả, công trình và năm công bố Nội dung và phương pháp tiếp cận chính
Đánh giá chất lượng trong tái cấu trúc Kataoka (2001) [33] Đề xuất độ đo tương liên (coupling metrics) để đánh giá ảnh hưởng của tái cấu trúc lên khả năng bảo trì chương trình.
Tahvildari (2003, 2004) [66] Mã hóa thiết kế thành đồ thị mục tiêu mềm (soft-goals graph) và xây dựng danh mục độ đo hướng đối tượng để tự động phát hiện vị trí tái cấu trúc.
Bảo toàn hành vi bằng biến đổi đồ thị Mens et al. (2005, 2007), Heckel et al. [8, 10, 23, 64, 73] Sử dụng kỹ thuật biến đổi đồ thị (graph transformation) để biểu diễn và kiểm chứng bảo toàn hành vi mã nguồn và mô hình.
Bảo toàn hành vi bằng điều kiện và lát cắt Leino et al. [52], Stroulia et al. [58] Sử dụng bất biến (invariants), tiền điều kiện và hậu điều kiện (pre/post-conditions) để đặc tả và đối sánh hành vi.
Tip & Krinke [42], Snelting et al. [51] Ứng dụng kỹ thuật cắt lát chương trình (slice program) và mô tả hệ thống bằng khung nhìn logic để kiểm chứng mã nguồn.
Tái cấu trúc mô hình UML Wimmer et al. (2012) [71] Xây dựng danh mục biến đổi mô hình sang mô hình bằng quy tắc kết hợp OCL, nhưng mô tả chủ yếu bằng ngôn ngữ tự nhiên.
Sunyé et al. (2001) [64] Đề xuất các phép toán thêm/xóa/chuyển phần tử trên biểu đồ lớp và máy trạng thái với ràng buộc OCL.
Ivan Porres (2003) [54] Đề xuất ngôn ngữ hành động (Action Language) để thực thi quy tắc chuyển đổi trên biểu đồ lớp và máy trạng thái.
Thomas et al. (2006) [4] Áp dụng ngôn ngữ QVT để bảo toàn ràng buộc OCL khi tái cấu trúc biểu đồ lớp (chủ yếu minh họa phép MoveAttribute).
Alessandro Folli & Tom Mens (2008) [26] Ứng dụng biến đổi đồ thị trên siêu mô hình UML cho biểu đồ lớp và máy trạng thái.
Markovic & Baar (2005, 2008) [40] Hình thức hóa và chứng minh bảo toàn ngữ nghĩa của 7 phép tái cấu trúc nguyên thủy (MoveAttribute, MoveAssociationEnd, PushDownAttribute, RenameAttribute, ExtractClass, ExtractSuperclass, PullUpMethod).
Pereira et al. (2011) [53] Đề xuất biến đổi mô hình cho các phép toán Folding, Abstraction, Composition, Factoring; thiết lập các hàm ánh xạ tương đương phương thức và thuộc tính.
Công cụ hỗ trợ tái cấu trúc Roberts et al. [57], Lee et al. [35], Eclipse IDE Phát triển các công cụ như Refactoring Browser for Smalltalk, JRefactory, Design Pattern Transformer (DPT), Refactorit, Eclipse.

Vị trí của luận án được xác định thông qua việc giải quyết các khoảng trống học thuật từ các công trình đi trước, đặc biệt là nghiên cứu của Pereira et al. [53]. Luận án chỉ ra rằng các nghiên cứu trước đây mô tả các phép toán bằng ngôn ngữ tự nhiên hoặc bán hình thức, chưa định nghĩa chặt chẽ khái niệm "tương đương ngữ nghĩa" giữa các thuộc tính và phương thức, chưa chứng minh hình thức sự bảo toàn các ràng buộc bất biến của lớp, và các công cụ hiện có hầu như chỉ hỗ trợ tự động hóa thao tác sửa mã mà thiếu tính năng kiểm chứng tự động sự bảo toàn hành vi. Do đó, luận án định vị là công trình xây dựng khung hình thức hóa toán học hoàn chỉnh cho 5 phép toán tái cấu trúc kế thừa, thiết lập phương pháp kiểm chứng nhất quán hành vi hai mức (thiết kế và cài đặt), và hiện thực hóa bằng công cụ kiểm chứng CVT dựa trên Logic vị từ bậc 1 (First-Order Logic - FOL).

Cơ sở lý thuyết và phương pháp nghiên cứu

Cơ sở lý thuyết, khái niệm và khung phân tích

Luận án xây dựng trên nền tảng các lý thuyết và chuẩn công nghệ hình thức sau:

  • Mô hình hướng đối tượng (Object-Oriented Modeling - OOM): Hệ thống hóa các khái niệm lớp (Class), thuộc tính (Attributes), phương thức (Methods), các mối quan hệ cấu trúc (kết hợp - Association, tụ hợp - Aggregation, hợp thành - Composition, hiện thực hóa - Realization, tổng quát hóa - Generalization, phân cấp kế thừa - Class Hierarchy), cùng hệ thống ràng buộc ngữ nghĩa (Class Invariants, Pre-conditions, Post-conditions).
  • Ngôn ngữ mô hình hóa thống nhất UML (Unified Modeling Language 2.5): Sử dụng biểu đồ lớp (khung nhìn tĩnh) và biểu đồ tuần tự (khung nhìn động/kịch bản tương tác) làm đối tượng mô hình hóa chuẩn.
  • Mẫu thiết kế (Design Pattern - GoF): Sử dụng mẫu hành vi Strategy làm giải pháp mẫu để tái cấu trúc mã nguồn và mô hình, bao gồm các thành phần: giao diện IStrategy, các lớp thuật toán cụ thể ConcreteStrategy, và lớp ngữ cảnh Context.
  • Ngôn ngữ ràng buộc đối tượng OCL (Object Constraint Language 2.4 - OMG): Sử dụng để biểu diễn hình thức các bất biến (inv), tiền điều kiện (pre), hậu điều kiện (post), giá trị khởi tạo (init), giá trị dẫn xuất (derive), và truy vấn dữ liệu (query) trên mô hình thiết kế.
  • Ngôn ngữ đặc tả cho Java JML (Java Modeling Language): Sử dụng để đặc tả hình thức các hợp đồng hành vi nhúng trực tiếp trong mã nguồn Java thông qua các từ khóa requires, ensures, invariant.
  • Logic vị từ bậc 1 (First-Order Logic - FOL): Sử dụng hệ thống liên kết logic ($\Rightarrow, \wedge, \vee, \Leftrightarrow, \neg$), các ký hiệu hằng, biến, hàm, vị từ và các lượng từ ($\forall, \exists$) làm ngôn ngữ trung gian hình thức để phục vụ suy diễn và kiểm chứng tự động.

Phương pháp nghiên cứu thực tế

Luận án kết hợp chặt chẽ giữa phương pháp nghiên cứu lý thuyết hình thức và phương pháp nghiên cứu thực nghiệm công nghệ phần mềm:

  1. Phương pháp hình thức hóa toán học: Chuyển đổi toàn bộ các khái niệm thành phần của biểu đồ lớp, quan hệ kết hợp, biểu đồ tuần tự và các biểu thức ràng buộc thành các cấu trúc đại số và công thức logic vị từ bậc 1. Xây dựng 12 định nghĩa toán học chặt chẽ và thiết lập Mệnh đề 3.1.
  2. Phương pháp chứng minh hình thức: Áp dụng các quy tắc suy diễn logic mệnh đề và logic vị từ để chứng minh tính đúng đắn và bảo toàn ngữ nghĩa của các luật tái cấu trúc.
  3. Phương pháp kiểm chứng dựa trên công cụ giải SMT/FOL: Chuyển đổi văn phạm biểu thức OCL sang dạng cây cú pháp trừu tượng (AST) và sinh mã FOL tiền tố (prefix form), từ đó đưa về bài toán kiểm tra tính thỏa (satisfiability) và tính tương đương logic.
  4. Phương pháp thực nghiệm: Xây dựng phần mềm công cụ CVT (Consistency Validator Tool), tiến hành cài đặt ca nghiên cứu thực tế (case study) trên hệ thống ARTC và hệ thống ATM để đối sánh kết quả trước và sau tái cấu trúc ở cả hai pha thiết kế (UML/OCL) và cài đặt (Java/JML).

Nguồn tư liệu và dữ liệu nghiên cứu

  • Tài liệu chuẩn kỹ thuật từ tổ chức OMG về UML 2.5 và OCL 2.4; tài liệu chuẩn đặc tả ngôn ngữ JML.
  • Bộ dữ liệu mô hình và mã nguồn của hệ thống điều khiển lưu lượng giao thông đường bộ thích ứng ARTC (bao gồm các lớp điều khiển tín hiệu đèn, thuật toán tối ưu optimizeTraffic(), phương thức phân tích thời gian analyzeTimeLimit()).
  • Bộ dữ liệu mô hình hệ thống rút tiền tự động ATM mô tả quan hệ phân cấp kế thừa và liên kết tài khoản.

Nội dung chính theo từng chương

Chương 1: Mở đầu

Chương 1 thiết lập nền tảng bài toán nghiên cứu. Tác giả trình bày định nghĩa chuẩn của tái cấu trúc: phân bố lại các lớp, thuộc tính và phương thức xung quanh mối quan hệ phân cấp nhằm tạo thuận lợi cho việc thích ứng và mở rộng nhưng bảo toàn hành vi bên ngoài. Tác giả phân tích chi tiết 4 bài toán lớn: đánh giá chất lượng (sử dụng độ đo tương liên của Kataoka, đồ thị soft-goals của Tahvildari), bảo toàn hành vi (bằng biến đổi đồ thị, tiền/hậu điều kiện, lát cắt chương trình), duy trì tính nhất quán (theo chiều ngang giữa các phiên bản và theo chiều dọc giữa thiết kế với mã nguồn), và công cụ hỗ trợ tái cấu trúc. Chương này cũng làm rõ 3 đóng góp chính của luận án và trình bày sơ đồ cấu trúc tổng thể 6 chương.

Chương 2: Kiến thức cơ sở

Chương 2 hệ thống hóa các khái niệm nền tảng:

  • Quy trình tái cấu trúc 6 bước chuẩn: (1) Xác định vị trí, (2) Xác định phép toán tái cấu trúc, (3) Đảm bảo bảo toàn hành vi, (4) Thực thi tái cấu trúc, (5) Đánh giá ảnh hưởng chất lượng, (6) Duy trì tính nhất quán. Phân loại 2 nhóm phép toán: nguyên thủy (Primitive) và phức hợp (Composite).
  • Đặc trưng hệ thống hướng đối tượng: Chi tiết hóa cấu trúc lớp, phương thức, thuộc tính, 6 loại quan hệ (Association, Aggregation, Composition, Realization, Generalization, Class Hierarchy) và 3 loại khẳng định (bất biến, tiền điều kiện, hậu điều kiện).
  • Ngôn ngữ mô hình hóa UML: Phân biệt nhóm biểu đồ cấu trúc (tập trung biểu đồ lớp) và biểu đồ hành vi (tập trung biểu đồ tuần tự/kịch bản tương tác).
  • Mẫu thiết kế Strategy: Kiến trúc gồm IStrategy, ConcreteStrategy, Context và cơ chế hoán đổi linh hoạt thuật toán tại thời điểm chạy.
  • Ngôn ngữ ràng buộc OCL và JML: Cơ chế đặc tả hợp đồng ngữ nghĩa, cú pháp OCL (inv, pre, post, derive, init, query) và cú pháp JML (requires, ensures, invariant, các công cụ ESC/Java2, OpenJML).
  • Logic vị từ bậc 1 (FOL): Cú pháp, ngữ nghĩa, hệ thống liên kết và lượng từ đóng vai trò ngôn ngữ trung gian cho công cụ kiểm chứng tự động.

Chương 3: Phương pháp bảo toàn bất biến trong tái cấu trúc

Chương 3 là một trong hai chương đóng góp lý thuyết cốt lõi của luận án:

  • Tái cấu trúc trên quan hệ phân cấp kế thừa: Chi tiết hóa cơ chế của 5 phép toán:
    1. Folding: Gộp hai lớp có quan hệ kế thừa trực tiếp thành một lớp duy nhất để giảm độ sâu phân cấp.
    2. Abstraction: Trích xuất các thuộc tính và phương thức chung từ một lớp lớn để tạo thành một lớp cơ sở mới có quan hệ kế thừa.
    3. Composition: Gộp hai lớp độc lập (không kế thừa) thành một lớp duy nhất để loại bỏ sự cần thiết của đa kế thừa.
    4. Factoring: Nhóm các thuộc tính và phương thức trùng lặp từ nhiều lớp vào một lớp cha chung.
    5. Unfolding: Phân rã một lớp có danh sách thuộc tính lớn thành các lớp con kế thừa dựa trên việc phân vùng các tập thuộc tính rời rạc được tham chiếu bởi các nhóm phương thức riêng biệt.
  • Biến đổi quan hệ kết hợp: Phân tích 4 trường hợp biến đổi liên kết gồm: thêm kết hợp truyền ứng, xóa kết hợp truyền ứng, thay thế kết hợp (với lực lượng $MULT_1 \subseteq MULT_2$), và nối các kết hợp một chiều đối lập thành kết hợp hai chiều.
  • Quy trình và Khung hình thức hóa: Thiết lập quy trình 2 bước: (1) Thực hiện tái cấu trúc với các luật và (2) Chứng minh tính đúng đắn của luật. Xây dựng hệ thống 12 định nghĩa hình thức (từ Định nghĩa 3.1 đến 3.12) mô hình hóa cấu trúc lớp, mô hình, bất biến mô hình, cặp thuộc tính kết hợp được, cặp phương thức tương đương ngữ nghĩa.
  • Chứng minh toán học: Xây dựng các luật tái cấu trúc cho 5 phép toán dưới dạng khuôn mẫu (template) và chứng minh Mệnh đề 3.1, khẳng định rằng mô hình sau tái cấu trúc bằng các luật đề xuất bảo toàn đầy đủ các ràng buộc bất biến của mô hình ban đầu.

Chương 4: Phương pháp kiểm chứng sự bảo toàn hành vi trong tái cấu trúc

Chương 4 giải quyết bài toán bảo toàn hành vi cho các kịch bản (scenarios) phần mềm:

  • Quy trình kiểm chứng thống nhất: Đề xuất quy trình đối sánh tiền điều kiện và hậu điều kiện của kịch bản trước và sau tái cấu trúc khi áp dụng mẫu thiết kế Strategy.
  • Kiểm chứng ở mức mô hình thiết kế: Sử dụng biểu đồ tuần tự UML kết hợp biểu thức OCL. Các điều kiện biên và trạng thái chuyển đổi của kịch bản được tính toán lại sau khi áp dụng mẫu Strategy và đối sánh tính tương đương logic.
  • Kiểm chứng ở mức chương trình mã nguồn: Sử dụng mã nguồn Java nhúng đặc tả JML. Các phương thức được kiểm chứng tự động thông qua công cụ phân tích hợp đồng JML.
  • Thực nghiệm trên hệ thống ARTC (Adaptive Road Traffic Control):
    • Phân tích hạn chế của hệ thống ARTC ban đầu: thuật toán điều khiển đèn giao thông bị gắn cứng (hard-coded) vào lớp điều khiển, gây khó khăn khi thay đổi chiến lược điều khiển theo mật độ phương tiện.
    • Tái cấu trúc áp dụng mẫu Strategy: Tách thuật toán thành giao diện OptimizerStrategy và các lớp cụ thể.
    • Kiểm chứng hành vi kịch bản optimizeTraffic() và phương thức analyzeTimeLimit(): Chứng minh sự bảo toàn tuyệt đối về mặt hành vi điều chỉnh thời gian đèn tín hiệu ($signalTime = old(signalTime) \pm 10$) giữa mô hình ban đầu và mô hình tiến hóa.

Chương 5: Công cụ kiểm chứng

Chương 5 trình bày việc phát triển và thử nghiệm công cụ CVT (Consistency Validator Tool):

  • Kiến trúc CVT: Gồm các phân hệ chính: (1) Phân hệ tiếp nhận mô hình UML và ràng buộc OCL của hệ thống trước và sau tái cấu trúc, (2) Phân hệ phân tích cú pháp OCL, sinh cây cú pháp trừu tượng AST dựa trên văn phạm phi ngữ cảnh $G$ và tập luật sản xuất $R$, (3) Phân hệ chuyển đổi tự động biểu thức OCL sang công thức FOL dạng tiền tố (prefix), (4) Phân hệ kiểm chứng tính nhất quán dựa trên bộ giải logic vị từ.
  • Bảng luật văn phạm và chuyển đổi: Thiết lập tập luật chuyển đổi từ các toán tử logic OCL (and, or, not, implies, forAll, exists) sang các ký hiệu FOL tương ứng.
  • Kết quả thực nghiệm: Cài đặt giao diện đồ họa người dùng (GUI), chạy thử nghiệm kiểm chứng trên các tập dữ liệu ca kiểm thử. Kết quả xuất ra màn hình minh chứng rõ ràng hai trạng thái: thông báo "Nhất quán" (Consistent) khi mô hình bảo toàn hành vi và thông báo "Không nhất quán" (Inconsistent) kèm phản ví dụ khi có sự sai lệch ràng buộc.

Chương 6: Kết luận và hướng phát triển

Chương 6 tổng kết các kết quả đạt được, phân tích ưu điểm và hạn chế của các phương pháp đề xuất, đồng thời vạch ra các hướng nghiên cứu mở rộng trong tương lai.

Kết quả và những đóng góp mới

Luận án đã đạt được các đóng góp khoa học và thực tiễn chính sau:

  1. Đóng góp về mặt lý luận hình thức hóa bảo toàn bất biến:

    • Xây dựng thành công khung lý thuyết toán học hoàn chỉnh gồm 12 định nghĩa hình thức để mô hình hóa biểu đồ lớp UML và các ràng buộc bất biến.
    • Thiết lập khuôn mẫu biểu diễn và đề xuất hệ thống luật tái cấu trúc cho 5 phép toán trên quan hệ phân cấp kế thừa (Folding, Abstraction, Composition, Factoring, Unfolding).
    • Chứng minh bằng toán học Mệnh đề 3.1, xác lập rằng tiến trình tái cấu trúc tuân thủ các luật đề xuất bảo toàn tuyệt đối các ràng buộc bất biến của mô hình.

  2. Đóng góp về phương pháp kiểm chứng bảo toàn hành vi:

    • Đề xuất quy trình kiểm chứng tính nhất quán hành vi hai mức (mức thiết kế mô hình UML/OCL và mức mã nguồn cài đặt Java/JML) khi tái cấu trúc bằng mẫu thiết kế (Strategy pattern).
    • Xây dựng phương pháp tính toán và đối sánh hình thức các tiền/hậu điều kiện của kịch bản tương tác (scenarios).
    • Minh chứng tính khả thi và hiệu quả của phương pháp thông qua ca thực nghiệm hệ thống điều khiển giao thông ARTC.

  3. Đóng góp về mặt công cụ thực nghiệm:

    • Thiết kế kiến trúc và phát triển thành công công cụ phần mềm CVT (Consistency Validator Tool).
    • Xây dựng giải thuật và bộ quy tắc chuyển đổi tự động từ đặc tả OCL sang công thức logic vị từ bậc 1 (FOL) thông qua cây cú pháp trừu tượng AST, giải quyết hạn chế của việc thiếu hụt công cụ kiểm chứng trực tiếp trên OCL.

  4. Kiến nghị và giải pháp đề xuất:

    • Đề xuất áp dụng quy trình kiểm chứng hình thức như một bước bắt buộc trong các công cụ tái cấu trúc tự động để ngăn ngừa lỗi phát sinh.
    • Khuyến nghị kết hợp song song việc kiểm chứng bất biến cấu trúc tĩnh (Chương 3) và kiểm chứng hành vi động (Chương 4) trong suốt vòng đời phát triển phần mềm hướng đối tượng.

Hạn chế và hướng nghiên cứu tiếp

Hạn chế của luận án

  • Về phạm vi phép toán: Luận án mới tập trung nghiên cứu 5 phép toán tái cấu trúc liên quan đến phân cấp kế thừa trên biểu đồ lớp; chưa bao quát toàn bộ các phép tái cấu trúc nguyên thủy và phức hợp khác trong danh mục của Fowler.
  • Về phạm vi mẫu thiết kế: Phương pháp kiểm chứng hành vi mới được cài đặt và kiểm nghiệm chi tiết trên một mẫu thiết kế hành vi cụ thể là mẫu Strategy; chưa triển khai thực nghiệm cho các mẫu thiết kế thuộc nhóm khởi tạo (Creational) và nhóm cấu trúc (Structural).
  • Về mức độ tự động hóa của công cụ: Công cụ CVT hiện tập trung kiểm chứng tính nhất quán ở mức mô hình OCL/FOL; việc liên kết tự động hoàn toàn giữa kiểm chứng mã nguồn JML và mô hình thiết kế OCL trong một giao diện tích hợp duy nhất vẫn cần tiếp tục hoàn thiện.

Hạn chế mở rộng dựa trên phạm vi nghiên cứu

Do giới hạn phạm vi mô hình hóa trên biểu đồ lớp và biểu đồ tuần tự UML, luận án chưa xét đến sự biến đổi hành vi trên các biểu đồ động phức tạp khác như biểu đồ máy trạng thái (State Machine Diagram) hoặc biểu đồ hoạt động (Activity Diagram) trong các hệ thống thời gian thực có ràng buộc khắt khe về thời gian và tài nguyên bộ nhớ.

Hướng nghiên cứu tiếp theo

  1. Mở rộng khung lý thuyết và luật tái cấu trúc cho các mẫu thiết kế khác trong nhóm GoF (như State, Observer, Factory Method, Adapter).
  2. Nghiên cứu phương pháp kiểm chứng bảo toàn hành vi trên các biểu đồ hành vi khác của UML, đặc biệt là biểu đồ máy trạng thái cho hệ thống nhúng và thời gian thực.
  3. Nâng cấp và hoàn thiện công cụ CVT thành một plugin tích hợp trực tiếp vào các môi trường phát triển tích hợp (IDE) phổ biến như Eclipse, hỗ trợ tự động phát hiện vi phạm bất biến và tự động đề xuất phương án sửa lỗi trực quan cho lập trình viên.

Giá trị tham khảo

Luận án mang lại giá trị tham khảo học thuật và ứng dụng thực tiễn rõ rệt cho các nhóm đối tượng sau:

  • Đối với nghiên cứu sinh, học viên cao học chuyên ngành Khoa học máy tính và Kỹ thuật phần mềm: Luận án cung cấp một tài liệu tham khảo chuẩn mực về phương pháp hình thức hóa toán học cho các mô hình phần mềm hướng đối tượng. Đặc biệt, hệ thống 12 định nghĩa ở Chương 3 và phương pháp chuyển đổi văn phạm OCL sang FOL ở Chương 5 là tài liệu mẫu hữu ích cho các nghiên cứu về kiểm chứng mô hình (Model Checking) và kiểm chứng phần mềm (Software Verification).
  • Đối với giảng viên và các nhà nghiên cứu: Có thể sử dụng nội dung Chương 2, Chương 3 và Chương 4 làm học liệu chuyên đề phục vụ giảng dạy các môn học bậc sau đại học như Phương pháp hình thức trong công nghệ phần mềm, Kiến trúc và Thiết kế phần mềm nâng cao, Tái cấu trúc và Bảo trì phần mềm.
  • Đối với kỹ sư phần mềm, kiến trúc sư hệ thống và người làm chính sách công nghệ: Cung cấp quy trình bài bản để kiểm soát chất lượng khi nâng cấp, bảo trì các hệ thống phần mềm nghiệp vụ phức tạp. Phương pháp kiểm chứng hợp đồng hành vi (OCL/JML) giúp các dự án phần mềm quan trọng (như giao thông, ngân hàng) giảm thiểu rủi ro lỗi ngữ nghĩa phát sinh trong quá trình tái cấu trúc mã nguồn.

Câu hỏi thường gặp

1. Năm phép toán tái cấu trúc trên quan hệ phân cấp kế thừa được luận án nghiên cứu gồm những phép toán nào và có cơ chế hoạt động ra sao?

Năm phép toán bao gồm:

  • Folding: Gộp hai lớp có quan hệ kế thừa trực tiếp cha - con thành một lớp duy nhất nhằm giảm độ sâu phân cấp của cây kế thừa.
  • Abstraction: Trích xuất các thuộc tính và phương thức từ một lớp có sẵn để tạo thành một lớp cơ sở (lớp cha) mới, đồng thời thiết lập quan hệ kế thừa từ lớp mới này đến phần còn lại của lớp ban đầu.
  • Composition: Gộp hai lớp độc lập (không có quan hệ kế thừa) thành một lớp duy nhất để tránh việc phải sử dụng kỹ thuật đa kế thừa gây xung đột phương thức.
  • Factoring: Nhóm các thuộc tính và phương thức trùng lặp xuất hiện ở nhiều lớp vào trong một lớp cha chung, sau đó tạo liên kết kế thừa từ lớp cha đến các lớp đó.
  • Unfolding: Phân chia một lớp có quá nhiều thuộc tính thành các lớp con kế thừa từ phần còn lại của lớp ban đầu, dựa trên việc phân vùng các tập thuộc tính rời rạc được tham chiếu bởi các phương thức tương ứng.

2. Sự khác biệt căn bản giữa hai ngôn ngữ đặc tả OCL và JML trong quy trình kiểm chứng của luận án là gì?

Sự khác biệt căn bản nằm ở giai đoạn áp dụng trong vòng đời phát triển phần mềm:

  • OCL (Object Constraint Language): Là ngôn ngữ đặc tả thuần túy ở mức mô hình thiết kế (UML), được dùng để mô tả các bất biến của lớp, tiền điều kiện và hậu điều kiện của phương thức mà không làm thay đổi trạng thái mô hình và không phụ thuộc vào ngôn ngữ lập trình cụ thể.
  • JML (Java Modeling Language): Là ngôn ngữ đặc tả hình thức ở mức mã nguồn cài đặt, được nhúng trực tiếp vào các tệp mã nguồn Java (bằng các chú thích //@ hoặc /*@ ... @*/) để phục vụ việc biên dịch, thực thi và kiểm chứng tính đúng đắn của chương trình Java cụ thể.

3. Tại sao luận án phải chuyển đổi biểu thức OCL sang Logic vị từ bậc 1 (FOL) trong công cụ CVT thay vì kiểm chứng trực tiếp?

Luận án lựa chọn chuyển đổi sang FOL vì ở thời điểm nghiên cứu, các công cụ hỗ trợ kiểm chứng trực tiếp biểu thức OCL còn rất hạn chế về số lượng và khả năng tự động hóa. Trong khi đó, các công cụ và bộ giải dựa trên Logic vị từ bậc 1 (như các bộ giải SMT / FOL Theorem Prover) đã đạt đến độ hoàn thiện, trưởng thành cao về mặt lý thuyết và hiệu năng thực thi. Việc chuyển đổi OCL sang FOL dạng tiền tố thông qua cây cú pháp trừu tượng (AST) cho phép tận dụng sức mạnh tính toán của các bộ chứng minh định lý tự động sẵn có để đưa ra kết luận chính xác về tính nhất quán.

4. Ca thực nghiệm hệ thống ARTC đã minh chứng cho phương pháp kiểm chứng bảo toàn hành vi như thế nào?

Trong ca thực nghiệm hệ thống điều khiển lưu lượng giao thông đường bộ thích ứng (ARTC), bài toán đặt ra là tái cấu trúc để tách thuật toán tối ưu hóa đèn giao thông ra khỏi lớp điều khiển cứng bằng cách áp dụng mẫu Strategy. Luận án đã mô hình hóa kịch bản optimizeTraffic() và phương thức analyzeTimeLimit() trước và sau tái cấu trúc bằng OCL (ở mức thiết kế) và JML (ở mức mã Java). Phương pháp kiểm chứng đã đối sánh các ràng buộc trạng thái tín hiệu đèn (heavyTraffic, lowTraffic, red, green) và chứng minh được rằng sự biến đổi thời gian đèn ($signalTime$) hoàn toàn tương đương logic giữa hai phiên bản, khẳng định hành vi hệ thống được bảo toàn trọn vẹn.

Kết luận

Luận án tiến sĩ "Một số phương pháp kiểm chứng tái cấu trúc phần mềm" của tác giả Đào Thị Hường đã giải quyết thành công bài toán kiểm chứng hình thức sự bảo toàn các ràng buộc ngữ nghĩa trong tái cấu trúc phần mềm hướng đối tượng. Tác giả đã xây dựng hệ thống cơ sở lý thuyết toán học chặt chẽ để chứng minh sự bảo toàn bất biến trên biểu đồ lớp UML cho 5 phép toán phân cấp kế thừa, đồng thời thiết lập quy trình kiểm chứng bảo toàn hành vi thống nhất từ mô hình thiết kế đến mã nguồn cài đặt khi áp dụng mẫu thiết kế Strategy. Việc phát triển và thực nghiệm thành công công cụ CVT chuyển đổi OCL sang FOL trên hệ thống thực tế ARTC đã khẳng định tính đúng đắn, tính khả thi và giá trị ứng dụng cao của các kết quả nghiên cứu.