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 luận án ts m

Tổng quan về luận án

Luận án này tập trung giải quyết các thách thức then chốt trong lĩnh vực tái cấu trúc phần mềm hướng đối tượng, đặc biệt là việc kiểm chứng tính bảo toàn của hệ thống trong quá trình biến đổi. Trong bối cảnh phát triển phần mềm hiện đại, tái cấu trúc (refactoring) được công nhận là một kỹ thuật mạnh mẽ nhằm "cải thiện cấu trúc bên trong mà không làm ảnh hưởng đến hành vi bên ngoài của hệ thống" [p.iii, p.1]. Tuy nhiên, hoạt động này, nếu không được kiểm soát chặt chẽ, rất dễ phát sinh lỗi và làm suy giảm các đặc trưng chất lượng phần mềm [p.iii].

Bối cảnh khoa học và tính tiên phong của nghiên cứu

Nghiên cứu này được đặt trong bối cảnh ngày càng gia tăng sự phức tạp của hệ thống phần mềm và nhu cầu bức thiết về các phương pháp đảm bảo chất lượng, đặc biệt là khả năng duy trì tính đúng đắn và hành vi dự kiến sau các hoạt động cải tiến. Luận án mang tính tiên phong khi đề xuất các phương pháp hình thức hóa và kiểm chứng toàn diện, vượt ra ngoài các cách tiếp cận bán hình thức hoặc không hình thức trước đây [p.4-5].

Research gap SPECIFIC với citations từ literature

Dù đã có nhiều nghiên cứu về tái cấu trúc, một số khoảng trống quan trọng vẫn tồn tại. Cụ thể, "chưa có nghiên cứu nào thực sự đi sâu và xem xét sự biến đổi của các ràng buộc bất biến khi thực hiện tái cấu trúc biểu đồ lớp" [p.5]. Các công trình trước đây của Pereira và cộng sự [53], Sunyé và cộng sự [64] thường chỉ dừng lại ở việc biểu diễn các phép toán tái cấu trúc bằng "phương pháp không hình thức (informal) hoặc nửa hình thức (semi-formal) và mô tả các phép toán bằng ngôn ngữ tự nhiên" [p.4-5], dẫn đến thiếu chính xác và khó khăn trong việc xây dựng công cụ hỗ trợ.

Hơn nữa, về bảo toàn hành vi, "Các nghiên cứu này tập trung kiểm chứng sự bảo toàn hành vi chính giai đoạn mã nguồn với nhau, hoặc kiểm tra sự nhất quán giữa các giai khác nhau của tiến trình phát triển phần mềm (giai đoạn thiết kế với giai đoạn cài đặt mã nguồn)" [p.3]. Luận án này đặc biệt phân biệt bằng cách tập trung vào "đối tượng xem xét biến đổi hành vi trong tái cấu trúc" là "các kịch bản (scenarios) tham gia vào tiến trình tái cấu trúc" [p.64], một khía cạnh ít được chú ý một cách có hệ thống trong các nghiên cứu trước. Vấn đề công cụ hỗ trợ cũng là một khoảng trống lớn, khi "hầu hết các công cụ này đều rơi vào loại thứ nhất [tìm kiếm vị trí tái cấu trúc] và chưa có sự xem xét đến vấn đề bảo toàn hành vi của hệ thống sau tiến trình tái cấu trúc" [p.3].

Research questions và hypotheses

Luận án giải quyết các câu hỏi nghiên cứu sau:

1. Làm thế nào để đề xuất một phương pháp hình thức để bảo toàn bất biến của lớp trong quá trình tái cấu trúc biểu đồ lớp của UML?
2. Làm thế nào để xây dựng một phương pháp kiểm chứng sự bảo toàn hành vi của hệ thống phần mềm khi áp dụng các mẫu thiết kế trong tái cấu trúc, xuyên suốt các giai đoạn thiết kế và cài đặt?
3. Làm thế nào để phát triển một công cụ tự động hỗ trợ kiểm chứng tính nhất quán trong tái cấu trúc mô hình phần mềm, đặc biệt là quá trình chuyển đổi biểu thức OCL sang các công thức logic hình thức?

Các giả thuyết chính của luận án bao gồm: H1: Có thể hình thức hóa các thành phần của biểu đồ lớp và các phép toán tái cấu trúc liên quan đến quan hệ phân cấp, đồng thời chứng minh được sự bảo toàn bất biến của lớp bằng phương pháp toán học. H2: Bằng cách hình thức hóa các kịch bản (biểu đồ tuần tự) và các ràng buộc về tiền/hậu điều kiện, có thể kiểm chứng được sự bảo toàn hành vi của hệ thống trong tái cấu trúc có áp dụng mẫu thiết kế tại cả giai đoạn thiết kế và cài đặt. H3: Một công cụ có thể được xây dựng để tự động kiểm tra tính nhất quán về mặt hành vi trong tái cấu trúc mô hình phần mềm thông qua việc chuyển đổi OCL sang Logic Vị từ bậc 1 (FOL) và sử dụng các công cụ giải SMT.

Theoretical framework với tên theories cụ thể

Luận án được xây dựng trên nền tảng vững chắc của một số lý thuyết và ngôn ngữ hình thức quan trọng:

• Ngôn ngữ Mô hình hóa Thống nhất (UML - Unified Modeling Language): Được sử dụng để mô tả cấu trúc tĩnh (biểu đồ lớp - Class Diagram) và hành vi động (biểu đồ tuần tự - Sequence Diagram) của hệ thống phần mềm [p.14]. UML, khởi xướng bởi Grady Booch, James Rumbaugh, và Ivar Jacobsen, là chuẩn ISO và nền tảng của phương pháp luận hướng đối tượng [p.14].
• Ngôn ngữ Ràng buộc Đối tượng (OCL - Object Constraint Language): Là ngôn ngữ hình thức, do IBM phát triển và được OMG chuẩn hóa, dùng để đặc tả các ràng buộc bất biến (invariants), tiền điều kiện (pre-conditions), và hậu điều kiện (post-conditions) trên các mô hình UML [p.21].
• Ngôn ngữ Đặc tả cho Java (JML - Java Modeling Language): Cung cấp phương tiện để đặc tả hình thức các ràng buộc tương tự (invariants, pre/post-conditions) trực tiếp trong mã nguồn Java [p.25], phục vụ cho việc kiểm chứng ở giai đoạn cài đặt.
• Logic Vị từ Bậc 1 (FOL - First-Order Logic): Đóng vai trò là cơ sở lý thuyết trung gian để biểu diễn các ràng buộc và thực hiện kiểm chứng tự động bằng các công cụ giải SMT (Satisfiability Modulo Theories) như Z3 [22], KeY [1], CVC4 [6] [p.26-27].
• Mẫu Thiết kế (Design Patterns): Cụ thể là Mẫu Strategy (một mẫu hành vi trong nhóm của Gang of Four - GoF [67]), được sử dụng như một kỹ thuật tái cấu trúc nhằm cải thiện thiết kế và tính linh hoạt của hệ thống [p.19-20].
• Lý thuyết Đồ thị: Ngầm định trong các khái niệm về biểu đồ lớp và biến đổi mô hình.

Đóng góp đột phá với quantified impact

Luận án mang đến các đóng góp đột phá với tác động rõ rệt:

1. Hình thức hóa và Chứng minh Bảo toàn Bất biến: Đề xuất phương pháp bảo toàn bất biến của lớp trong tái cấu trúc biểu đồ lớp của UML, bằng cách hình thức hóa các phần tử và ràng buộc bất biến bằng ký pháp toán học. Các luật tái cấu trúc cho 5 phép toán cơ bản (Folding, Abstraction, Composition, Factoring, Unfolding) được định nghĩa và "chứng minh tính đúng đắn của các luật này bằng phương pháp toán học" [p.iii, p.54-57]. Điều này nâng cao độ tin cậy của quá trình tái cấu trúc ở mức thiết kế, cung cấp một nền tảng lý thuyết vững chắc cho các nhà phát triển.
2. Phương pháp Kiểm chứng Hành vi Đa giai đoạn tập trung vào Kịch bản: Phát triển một phương pháp kiểm chứng sự bảo toàn hành vi trong tái cấu trúc, áp dụng mẫu thiết kế Strategy, xuyên suốt cả giai đoạn thiết kế (sử dụng UML và OCL) và giai đoạn cài đặt (sử dụng Java và JML). Đối tượng kiểm chứng là "các kịch bản (scenarios) tham gia vào tiến trình tái cấu trúc" [p.108], một cách tiếp cận chi tiết hơn so với các nghiên cứu tập trung vào biểu đồ lớp hoặc trạng thái.
3. Công cụ Hỗ trợ Tự động CVT (Consistency Validator Tool) với Chức năng OCL2FOL: Xây dựng công cụ CVT để tự động hóa việc kiểm chứng tính nhất quán về hành vi trong tái cấu trúc mô hình phần mềm [p.iv, p.108]. Một đóng góp quan trọng của CVT là khả năng "Chuyển đổi biểu thức OCL sang công thức FOL" [p.95, p.108], khắc phục hạn chế của các công cụ OCL hiện có và cho phép sử dụng các SMT solver mạnh mẽ như Z3 [p.96].
4. Giải quyết vấn đề chuyển đổi OCL phức tạp: Nghiên cứu đã đi sâu giải quyết vấn đề chuyển đổi các biểu thức OCL có cú pháp phức tạp sang FOL, một điểm mà các nghiên cứu trước đây [7, 19, 20] còn hạn chế ở các biểu thức đơn giản [p.95]. Điều này mở rộng khả năng áp dụng của các công cụ kiểm chứng hình thức.
5. Ứng dụng thực tiễn trên Hệ thống Điều khiển Giao thông Đường bộ (ARTC): Phương pháp đề xuất được minh họa và kiểm chứng trên hệ thống ARTC, một mô hình phức tạp với các yếu tố thời gian thực [p.77-78]. "Kết quả kiểm chứng sự bảo toàn hành vi ở hai chương là hoàn toàn tương thích" [p.109], khẳng định tính khả thi và hiệu quả của phương pháp.

Scope (sample size, timeframe) và significance

Phạm vi nghiên cứu tập trung vào tái cấu trúc hệ thống hướng đối tượng. Về phương pháp bảo toàn bất biến, luận án xem xét "năm phép toán Folding, Abstraction, Composition, Factoring và Unfolding" [p.44] trên biểu đồ lớp UML. Đối với bảo toàn hành vi, trọng tâm là các kịch bản (biểu đồ tuần tự) và mẫu thiết kế Strategy. Phạm vi thực nghiệm được giới hạn trong case study là hệ thống ARTC, bao gồm 5 lớp chính (TrafficController, Detector, Road, Junction, Optimizer) và các kịch bản tương tác cốt lõi [p.80-81]. Luận án được hoàn thành vào năm 2018 [p.i], phản ánh các vấn đề và công nghệ tại thời điểm đó.

Ý nghĩa của nghiên cứu nằm ở việc cung cấp một bộ phương pháp và công cụ hình thức, đáng tin cậy để "bổ sung và hoàn thiện các giải pháp nâng cao chất lượng của hệ thống phần mềm khi áp dụng kỹ thuật tái cấu trúc" [p.6, p.109]. Nó giảm thiểu rủi ro phát sinh lỗi, tiết kiệm thời gian và công sức trong các dự án phát triển và bảo trì phần mềm, đồng thời mở ra hướng nghiên cứu mới về tự động hóa kiểm chứng trong các giai đoạn sớm của vòng đời phần mềm.

Literature Review và Positioning

Phần tổng quan tài liệu đã phân tích sâu rộng các công trình nghiên cứu trong lĩnh vực tái cấu trúc phần mềm, đặc biệt là các kỹ thuật nhằm đảm bảo sự bảo toàn của hệ thống.

Synthesis của major streams với TÊN TÁC GIẢ và NĂM cụ thể

Các luồng nghiên cứu chính có thể được phân loại như sau:

1. Biến đổi Đồ thị (Graph Transformation): Một kỹ thuật phổ biến coi mô hình hoặc chế tác phần mềm là đồ thị và tái cấu trúc là quá trình biến đổi đồ thị dựa trên các tập luật. Bottoni và cộng sự [10] năm 2003 đã đề xuất phương pháp duy trì tính nhất quán giữa mô hình thiết kế và mã nguồn thông qua việc tạo ra nhiều loại mô hình UML khác nhau. Mens và cộng sự [44] đã trình bày phương pháp hình thức biểu diễn đồ thị và các quy tắc viết lại chương trình ban đầu và tái cấu trúc, tập trung vào giai đoạn cài đặt mã nguồn. Zhao và cộng sự [73] sử dụng phương pháp biến đổi đồ thị dựa trên sự tiến hóa của các mẫu thiết kế, kiểm tra tính toàn vẹn cấu trúc theo từng bước phát triển mẫu thiết kế. Jing Dong và cộng sự [23] năm 2006 kiểm tra tính nhất quán giữa hai mô hình thiết kế bằng cách mô tả chúng bằng XMI và sử dụng Java Theorem Prover.
2. Sử dụng Khẳng định (Assertions - Invariants, Pre/Post-conditions): Đây là một phương pháp quan trọng để đặc tả và kiểm chứng hành vi. Pereira và cộng sự [53] năm 2004 đã nghiên cứu tái cấu trúc biểu đồ lớp và máy trạng thái, sử dụng các hợp đồng OCL (OCL contracts) để mô tả các phép toán, nhưng chưa đi sâu vào bảo toàn bất biến của lớp. Markovic và cộng sự [40] năm 2008 đã hình thức hóa và chứng minh sự bảo toàn ngữ nghĩa của một số phép tái cấu trúc nguyên thủy như MoveAttribute, ExtractClass, chỉ ra rằng cấu trúc OCL có thể thay đổi nhưng ngữ nghĩa vẫn bảo toàn. Thomas và cộng sự [4] tập trung vào biểu diễn mô hình có chú thích OCL và đề xuất phương pháp bảo toàn các ràng buộc OCL khi cấu trúc mô hình thay đổi, nhưng chỉ minh họa với phép toán đơn giản MoveAttribute.
3. Cắt Lát Chương Trình (Program Slicing) và Ngôn ngữ Hình thức: Takeshi [42] năm 2003 nghiên cứu kết hợp cắt lát chương trình với ngôn ngữ mô phỏng ký hiệu để kiểm tra tính nhất quán của chương trình C. Ward và Bennett [68] đã giới thiệu ngôn ngữ hình thức WSL để chứng minh bảo toàn hành vi ở mức mã nguồn.
4. Kiểm tra tính nhất quán giữa các loại chế tác hoặc biểu đồ: Li và cộng sự [38] phân tích phương pháp kiểm tra năm loại thuộc tính nhất quán của các yêu cầu UML (mô hình ca sử dụng và mô hình lớp). Rasch và Wehrheim [56] đề xuất sử dụng Object-Z để kiểm tra tính nhất quán giữa các lớp và máy trạng thái tương ứng.
5. Công cụ hỗ trợ tái cấu trúc: Mohammed Misbhauddin và cộng sự [48] năm 2015 đã khảo sát và phân loại các công cụ tái cấu trúc thành hai nhóm chính: tìm kiếm vị trí tái cấu trúc và thực thi tái cấu trúc. Nhiều công cụ đã xuất hiện như Refactoring Browser for Smalltalk [57], JRefactory, Design Pattern Transformer (DPT) [35], Refactorit, Eclipse [p.3, p.94].

Contradictions/debates với ít nhất 2 opposing views

Một điểm tranh luận chính trong lĩnh vực tái cấu trúc là sự đánh đổi giữa tính hình thức tuyệt đối (proven formally) và tính khả thi trong thực tiễn. Bài toán chứng minh tính đúng đắn về ngữ nghĩa cho đến nay là "bài toán không quyết định được (undecidable problem)" [30]. Điều này dẫn đến sự cần thiết của các "phương pháp tiếp cận mang tính ước lượng (conservative)" [p.63] thay vì chứng minh hình thức hoàn toàn. Nhiều nghiên cứu như của Mens và Tourwe [43] đã đề cập đến nhiều kỹ thuật hình thức khác nhau, nhưng cũng phải thừa nhận chi phí phân tích tốn kém hoặc thậm chí không thể thực hiện được cho một số phương pháp hình thức nhất định [52, 58]. Luận án này đã giải quyết vấn đề này bằng cách kết hợp chứng minh toán học hình thức cho các luật tái cấu trúc (Mệnh đề 3.1) với việc phát triển công cụ tự động sử dụng SMT solver, một cách tiếp cận cân bằng giữa tính hình thức và khả năng triển khai.

Một cuộc tranh luận khác là đối tượng kiểm chứng hành vi. Một số nghiên cứu như của Sunyé và cộng sự [64] tập trung vào biểu đồ lớp và máy trạng thái, trong khi Van Eetvelde và Janssens [51] lại chuyển đổi chương trình thành đồ thị. Luận án này lập luận rằng việc tập trung vào "kịch bản (scenarios)" [p.64] – được coi là biểu đồ tuần tự ở giai đoạn thiết kế và thứ tự lời gọi hàm ở giai đoạn cài đặt – mang lại cái nhìn chi tiết hơn về hành vi thực thi của hệ thống, đặc biệt khi áp dụng các mẫu thiết kế.

Positioning trong literature với specific gap identified

Luận án này định vị mình bằng cách giải quyết một số khoảng trống cụ thể trong tài liệu:

• Thiếu phương pháp hình thức cho bảo toàn bất biến của lớp trong tái cấu trúc biểu đồ lớp: Như đã chỉ ra, các nghiên cứu trước đây chưa thực sự đi sâu vào vấn đề này một cách hình thức [p.5, p.29]. Luận án này cung cấp một khuôn khổ toán học và các luật tái cấu trúc được chứng minh [p.iii, p.29, Mệnh đề 3.1].
• Thiếu cách tiếp cận tập trung vào kịch bản cho bảo toàn hành vi: Các nghiên cứu trước chủ yếu tập trung vào biểu đồ lớp, trạng thái, hoặc mã nguồn [p.64]. Luận án này đề xuất một phương pháp mới, lấy kịch bản làm trung tâm, đặc biệt khi tái cấu trúc có sử dụng mẫu thiết kế như Strategy [p.64, p.108].
• Hạn chế của công cụ hỗ trợ kiểm chứng tự động: Mặc dù có nhiều công cụ tái cấu trúc, rất ít trong số đó hỗ trợ kiểm chứng tự động tính bảo toàn hành vi [p.3, p.94]. Luận án này phát triển công cụ CVT, tích hợp chức năng chuyển đổi OCL sang FOL và sử dụng SMT solver để tự động hóa quá trình này [p.iv, p.95].

How this advances field với concrete contributions

Nghiên cứu này tiến bộ hóa lĩnh vực bằng cách:

• Nâng cao tính chính xác và tin cậy của tái cấu trúc: Bằng cách cung cấp các luật tái cấu trúc được chứng minh toán học cho bảo toàn bất biến trên biểu đồ lớp, luận án giúp giảm thiểu rủi ro lỗi trong các hoạt động cải tiến thiết kế.
• Cung cấp khung kiểm chứng hành vi toàn diện hơn: Việc tập trung vào kịch bản và áp dụng mẫu thiết kế mang lại một cách nhìn chi tiết và thực tế hơn về cách hành vi hệ thống được bảo toàn qua các biến đổi.
• Tạo ra một cầu nối giữa đặc tả hình thức và công cụ tự động: Công cụ CVT, đặc biệt với chức năng OCL2FOL, là một bước tiến quan trọng trong việc tự động hóa kiểm chứng các ràng buộc phức tạp, giảm gánh nặng thủ công và nâng cao hiệu quả.

So sánh với ÍT NHẤT 2 international studies

1. So sánh với Pereira và cộng sự [53] (2004): Nghiên cứu của Pereira đề xuất các phép toán tái cấu trúc trên biểu đồ lớp và máy trạng thái, sử dụng hợp đồng OCL và mô tả các phép toán bằng ngôn ngữ tự nhiên. Tuy nhiên, luận án này chỉ ra rằng Pereira và cộng sự "chưa làm rõ khái niệm 'tương đương' giữa hai phương thức cũng như giữa hai thuộc tính" và "chưa thực hiện xem xét ảnh hưởng của tiến trình tái cấu trúc đến các ràng buộc bất biến của biểu đồ lớp" [p.32]. Luận án hiện tại vượt trội hơn bằng cách "biểu diễn một cách hình thức biểu đồ lớp và các thành phần cấu tạo lên biểu đồ lớp" và "xây dựng các luật tái cấu trúc và chứng minh sự đúng đắn về bảo toàn bất biến của các luật này" [p.32], cung cấp một nền tảng hình thức và chặt chẽ hơn.
2. So sánh với Mens và cộng sự [44] (2005) và Zhao và cộng sự [73] (2006): Các nghiên cứu này tập trung vào biến đổi đồ thị để kiểm chứng bảo toàn hành vi, nhưng chủ yếu ở giai đoạn cài đặt mã nguồn hoặc sự tiến hóa của mẫu thiết kế. Mens và cộng sự "kiểm chứng sự bảo toàn hành vi của hệ thống ở giai đoạn cài đặt mã nguồn trong khi nghiên cứu của chúng tôi lại xử lý bài toán trong giai đoạn thiết kế" [p.65]. Zhao và cộng sự xây dựng tập luật để kiểm tra tính nhất quán giữa mô hình trước và sau khi áp dụng các mẫu thiết kế nhưng dựa trên phân tích cú pháp mã nguồn. Luận án này mở rộng phạm vi bằng cách cung cấp phương pháp kiểm chứng hành vi xuyên suốt cả giai đoạn thiết kế (UML/OCL) và cài đặt (Java/JML), với trọng tâm là các kịch bản thực thi, mang lại cái nhìn tổng thể hơn về vòng đời phát triển phần mềm. Hơn nữa, luận án không chỉ tập trung vào cấu trúc mà còn vào ngữ nghĩa của hành vi thông qua tiền/hậu điều kiện.

Đóng góp lý thuyết và khung phân tích

Đóng góp cho lý thuyết

Luận án đưa ra những đóng góp lý thuyết đáng kể, mở rộng và củng cố nền tảng học thuật cho lĩnh vực tái cấu trúc phần mềm:

• Extend/challenge WHICH specific theories (name theorists):

  • Mở rộng lý thuyết về tái cấu trúc của Fowler [27]: Luận án mở rộng khái niệm tái cấu trúc từ việc cải thiện cấu trúc bên trong sang việc hình thức hóa các luật tái cấu trúc và chứng minh sự bảo toàn bất biến một cách toán học, đặc biệt cho các phép toán trên biểu đồ lớp của UML. Trong khi Fowler chủ yếu tập trung vào các phép tái cấu trúc và lợi ích của chúng, luận án này cung cấp cơ chế kiểm chứng hình thức cho các tuyên bố bảo toàn ngữ nghĩa.
  • Mở rộng lý thuyết về đặc tả hình thức của OCL (IBM, OMG) và JML (Gary Leavens): Luận án sử dụng OCL và JML không chỉ để đặc tả các ràng buộc mà còn làm cơ sở cho quá trình kiểm chứng tính nhất quán một cách tự động và bán tự động, đặc biệt thông qua việc chuyển đổi OCL sang FOL. Điều này nâng cao vai trò của các ngôn ngữ đặc tả hình thức từ mô tả sang công cụ kiểm chứng tích hợp.
  • Áp dụng và mở rộng lý thuyết Mẫu Thiết kế (GoF, Christopher Alexander): Luận án sử dụng Mẫu Strategy không chỉ như một giải pháp thiết kế mà còn là một kỹ thuật tái cấu trúc, và phát triển phương pháp kiểm chứng cụ thể cho các hệ thống được tái cấu trúc bằng mẫu này, tập trung vào bảo toàn hành vi của kịch bản.

• Conceptual framework với components và relationships: Khung lý thuyết của luận án được xây dựng dựa trên mối quan hệ chặt chẽ giữa các thành phần sau:

  1. Mô hình hóa hình thức (Formal Modeling): Sử dụng UML để mô tả cấu trúc (biểu đồ lớp) và hành vi (biểu đồ tuần tự) của hệ thống phần mềm [p.14].
  2. Đặc tả hình thức (Formal Specification): Áp dụng OCL để đặc tả bất biến (invariants), tiền điều kiện (pre-conditions), hậu điều kiện (post-conditions) ở giai đoạn thiết kế [p.21] và JML ở giai đoạn cài đặt [p.25].
  3. Biến đổi hình thức (Formal Transformation): Định nghĩa 5 phép toán tái cấu trúc trên biểu đồ lớp (Folding, Abstraction, Composition, Factoring, Unfolding) với các luật biến đổi được hình thức hóa [p.44-54].
  4. Kiểm chứng hình thức (Formal Verification): Sử dụng Logic Vị từ bậc 1 (FOL) làm ngôn ngữ trung gian [p.26], kết hợp với các SMT solver (như Z3 [22]) để tự động kiểm tra tính nhất quán giữa mô hình gốc và mô hình tái cấu trúc [p.96]. Mối quan hệ chính là sự chuyển đổi và bảo toàn ngữ nghĩa qua các giai đoạn: từ mô hình ban đầu (được đặc tả) -> qua tái cấu trúc (bằng các phép toán/mẫu thiết kế) -> đến mô hình tiến hóa (cũng được đặc tả) -> và cuối cùng là kiểm chứng sự tương đương hoặc bảo toàn các ràng buộc ngữ nghĩa giữa hai phiên bản.

• Theoretical model với propositions/hypotheses numbered: Luận án đề xuất một mô hình lý thuyết về kiểm chứng bảo toàn trong tái cấu trúc, được tổng hợp qua các mệnh đề và định nghĩa then chốt:

  • Mệnh đề 3.1 (p.54): "Một tiến trình tái cấu trúc R : MI -> M', OPname ∈ OPERATIONS. R thỏa mãn các điều kiện (3.1) là tiến trình tái cấu trúc bảo toàn các bất biến của lớp." Mệnh đề này khẳng định rằng 5 phép toán tái cấu trúc được định nghĩa (Folding, Abstraction, Composition, Factoring, Unfolding) đều bảo toàn bất biến nếu tuân thủ các luật đã đề xuất.
  • Định nghĩa 3.12 (p.42): Định nghĩa chính xác "bảo toàn bất biến trên mô hình tái cấu trúc" bằng hai điều kiện logic: F => F' và F'|M = F, trong đó F và F' là công thức bất biến của mô hình ban đầu và mô hình tái cấu trúc.
  • Định nghĩa 4.12 (p.75): Định nghĩa "bảo toàn hành vi toàn phần" cho một tiến trình tái cấu trúc, yêu cầu tiền và hậu điều kiện của kịch bản trên mô hình tiến hóa tương đương logic với kịch bản tương ứng trên mô hình khởi đầu (PRE_SIM' = PRE_SIM ∧ POST_SIM' = POST_SIM).
  • Định nghĩa 4.13 (p.75): Định nghĩa "bảo toàn hành vi một phần", cho phép hậu điều kiện tiến hóa chỉ thỏa mãn một phần hậu điều kiện gốc.
  • Định nghĩa 4.14 (p.75): Định nghĩa "không bảo toàn hành vi" khi không thỏa mãn cả hai trường hợp trên.

• Paradigm shift với EVIDENCE từ findings: Luận án góp phần vào một sự dịch chuyển nhỏ trong tư duy về tái cấu trúc phần mềm: từ một hoạt động chủ yếu dựa vào kinh nghiệm và công cụ hỗ trợ thực thi sang một quá trình được hỗ trợ bởi các phương pháp hình thức, có thể kiểm chứng toán học, và tự động hóa. Bằng cách chứng minh Mệnh đề 3.1 [p.54] và phát triển công cụ CVT [p.108], luận án cung cấp bằng chứng rằng các tuyên bố về bảo toàn ngữ nghĩa trong tái cấu trúc không chỉ là giả định mà có thể được kiểm chứng một cách khách quan và chặt chẽ, từ đó nâng cao độ tin cậy của toàn bộ quá trình phát triển phần mềm. Sự dịch chuyển này thể hiện rõ trong khả năng chuyển đổi OCL sang FOL để tận dụng sức mạnh của SMT solver [p.95], đưa việc kiểm chứng hình thức đến gần hơn với thực tiễn kỹ thuật phần mềm.

Khung phân tích độc đáo

Khung phân tích của luận án mang tính độc đáo ở sự tích hợp đa chiều và tập trung vào các khái niệm cốt lõi:

• Integration của theories (name 3+ specific theories): Khung phân tích tích hợp sâu sắc các lý thuyết:

  1. Lý thuyết hướng đối tượng (Object-Oriented Theory) và UML: Cung cấp ngôn ngữ và cấu trúc để mô hình hóa hệ thống.
  2. Lý thuyết đặc tả hình thức (Formal Specification Theory) thông qua OCL và JML: Cho phép định nghĩa rõ ràng các ràng buộc ngữ nghĩa và hành vi.
  3. Lý thuyết Logic Vị từ bậc 1 (First-Order Logic) và SMT (Satisfiability Modulo Theories): Cung cấp nền tảng toán học cho việc biểu diễn và kiểm chứng các ràng buộc một cách tự động.
  4. Lý thuyết Mẫu Thiết kế (Design Patterns) - cụ thể là Strategy Pattern: Được sử dụng như một chiến lược tái cấu trúc có mục đích. Sự tích hợp này cho phép phân tích một cách có hệ thống, từ ngữ nghĩa của các thành phần mô hình (lớp, thuộc tính, phương thức) đến hành vi động của hệ thống (kịch bản), và kiểm chứng sự bảo toàn của chúng qua các biến đổi tái cấu trúc.

• Novel analytical approach với justification: Cách tiếp cận phân tích độc đáo của luận án nằm ở việc:

  1. Tập trung vào kịch bản (scenarios) làm đối tượng chính cho kiểm chứng hành vi: Thay vì chỉ kiểm tra biểu đồ lớp hay trạng thái, luận án phân tích tiền và hậu điều kiện của các kịch bản thực thi [p.64, p.71], cung cấp một cái nhìn chi tiết hơn về cách hành vi hệ thống thay đổi (hoặc không thay đổi) trong quá trình tái cấu trúc. Điều này được chứng minh là hiệu quả hơn trong việc phát hiện các vi phạm hành vi trong môi trường thực thi động.
  2. Phân biệt rõ ràng giữa bảo toàn bất biến (cho cấu trúc tĩnh) và bảo toàn hành vi (cho cấu trúc động): Luận án tách bạch và giải quyết hai loại ràng buộc cơ bản này một cách riêng rẽ nhưng bổ trợ nhau [p.6-7, p.109]. Điều này cho phép một phân tích có mục tiêu và sâu sắc hơn cho từng khía cạnh chất lượng.
  3. Chuyển đổi hình thức OCL sang FOL để kiểm chứng tự động: Đây là một phương pháp mới mẻ, giúp bắc cầu giữa ngôn ngữ đặc tả mô hình (OCL) và các công cụ giải logic mạnh mẽ (SMT solvers) [p.95, p.97], mang lại khả năng tự động hóa mà trước đây gặp khó khăn với OCL.

• Conceptual contributions với definitions: Luận án đóng góp các khái niệm được định nghĩa rõ ràng, làm nền tảng cho nghiên cứu:

  • Định nghĩa 3.12 (p.42): "Bảo toàn bất biến trên mô hình tái cấu trúc," cung cấp tiêu chí hình thức để đánh giá sự bảo toàn của các ràng buộc tĩnh.
  • Định nghĩa 4.12, 4.13, 4.14 (p.75): Định nghĩa "bảo toàn hành vi toàn phần," "bảo toàn hành vi một phần," và "không bảo toàn hành vi," cung cấp một phân loại chi tiết và tiêu chí đánh giá cho sự thay đổi hành vi.
  • Khuôn mẫu biểu diễn phép toán tái cấu trúc (p.43): Bao gồm Tên, Tình huống áp dụng, Mô hình khởi đầu, Mô hình tiến hóa, và Biểu diễn bằng UML, tạo ra một cấu trúc chuẩn hóa cho việc mô tả các phép toán tái cấu trúc.
  • Khái niệm "phương thức của kịch bản" và "tiền/hậu điều kiện của kịch bản" (p.69-71): Hình thức hóa đối tượng kiểm chứng hành vi, làm rõ cách các ràng buộc này được xác định trong ngữ cảnh của một kịch bản thực thi.

• Boundary conditions explicitly stated: Luận án cũng xác định rõ các điều kiện biên của nghiên cứu:

  • Loại tái cấu trúc: Tập trung vào các phép toán liên quan đến quan hệ phân cấp trong kế thừa (Folding, Abstraction, Composition, Factoring, Unfolding) [p.44] và việc áp dụng mẫu thiết kế Strategy [p.63]. Các loại tái cấu trúc khác hoặc sự kết hợp phức tạp hơn của các phép toán chưa được xem xét toàn diện.
  • Phức tạp của kịch bản: Các kịch bản được xem xét chủ yếu là các lời gọi thông điệp tuần tự, "các kịch bản chứa các yếu tố phức hợp như phân đoạn rẽ nhánh (alternative fragment), phân đoạn kết hợp có tùy chọn (option combination fragment), phân đoạn chứa vòng lặp (loop fragment), phân đoạn tham chiếu (reference fragment) chưa được xem xét trong luận án này" [p.72].
  • Giả định về hành vi: Luận án giả định rằng "tất cả các phép toán tái cấu trúc đều đáp ứng các yêu cầu về bảo toàn hành vi, nói cách khác tiền và hậu điều kiện của các phương thức đều được bảo toàn sau tiến trình tái cấu trúc của Chương 3" [p.43]. Đây là một giả định mạnh để thu hẹp phạm vi cho việc kiểm chứng bất biến.

Phương pháp nghiên cứu tiên tiến

Phương pháp nghiên cứu của luận án được thiết kế một cách tỉ mỉ, kết hợp sự chặt chẽ của phương pháp hình thức với tính thực tiễn của kỹ thuật phần mềm, vượt trội hơn so với nhiều nghiên cứu trước đây vốn chỉ dừng lại ở cách tiếp cận bán hình thức hoặc không hình thức [p.4-5].

Thiết kế nghiên cứu

• Research philosophy (positivism/interpretivism/critical realism) Luận án tuân thủ chủ yếu triết lý nghiên cứu Thực chứng (Positivism), kết hợp với các yếu tố của Khoa học Thiết kế (Design Science). Nó nhấn mạnh vào việc "hình thức hóa các thành phần của hệ thống và xây dựng cơ sở lý thuyết nhằm bảo đảm sự bảo toàn các ràng buộc này khi thực thi tiến trình tái cấu trúc" [p.5]. Mục tiêu là đề xuất và "chứng minh sự đúng đắn của các luật này bằng phương pháp toán học" [p.iii], hướng tới các kết quả khách quan, có thể đo lường và kiểm chứng. Việc xây dựng công cụ CVT và áp dụng thực nghiệm trên hệ thống ARTC cũng thể hiện mong muốn tạo ra các giải pháp thiết kế có thể kiểm nghiệm được trong thực tiễn.

• Mixed methods với SPECIFIC combination rationale Luận án sử dụng phương pháp hỗn hợp, kết hợp nghiên cứu lý thuyết hình thức (formal theoretical research) với nghiên cứu ứng dụng (applied research) thông qua việc phát triển công cụ và thực nghiệm.

  • Rationale: Sự kết hợp này nhằm đảm bảo tính chặt chẽ về mặt lý thuyết và tính khả thi trong thực tiễn. Các chứng minh toán học (như Mệnh đề 3.1) cung cấp cơ sở vững chắc cho các luật tái cấu trúc, trong khi công cụ CVT hiện thực hóa các lý thuyết đó thành một giải pháp kiểm chứng tự động, dễ sử dụng.
  • Combination:
    • Chương 3 & 4: Phát triển lý thuyết và phương pháp hình thức cho bảo toàn bất biến và hành vi (sử dụng OCL, JML, FOL).
    • Chương 5: Thiết kế và cài đặt công cụ CVT để tự động hóa một phần quá trình kiểm chứng lý thuyết.
    • Chương 4 & 5: Áp dụng các phương pháp và công cụ trên một case study thực tiễn (hệ thống ARTC) để minh họa và đánh giá.

• Multi-level design với levels clearly defined Thiết kế nghiên cứu được thực hiện ở hai cấp độ chính của vòng đời phát triển phần mềm:

  1. Giai đoạn thiết kế (Design Phase): Tập trung vào mô hình UML (biểu đồ lớp, biểu đồ tuần tự) và đặc tả ràng buộc bằng OCL. Các luật tái cấu trúc được định nghĩa và chứng minh ở cấp độ này [p.iii, p.44-54].
  2. Giai đoạn cài đặt (Implementation Phase): Tập trung vào mã nguồn Java và đặc tả ràng buộc bằng JML. Quá trình kiểm chứng ở cấp độ này tận dụng công cụ OpenJML tích hợp trong Eclipse [p.68]. Việc nghiên cứu ở cả hai cấp độ đảm bảo rằng các phương pháp được đề xuất có thể áp dụng xuyên suốt vòng đời phát triển phần mềm, từ ý tưởng thiết kế trừu tượng đến mã nguồn cụ thể.

• Sample size và selection criteria EXACT Trong nghiên cứu này, khái niệm "kích thước mẫu" không áp dụng theo nghĩa thống kê truyền thống mà là lựa chọn các đối tượng nghiên cứu và trường hợp ứng dụng.

  • Đối tượng tái cấu trúc bất biến: 5 phép toán tái cấu trúc cụ thể trên biểu đồ lớp UML: "Folding, Abstraction, Composition, Factoring và Unfolding" [p.44]. Việc lựa chọn 5 phép toán này là do chúng "có liên quan trực tiếp đến quan hệ phân cấp trong kế thừa" [p.37] và đại diện cho các hoạt động tái cấu trúc cấu trúc lớp phổ biến.
  • Đối tượng tái cấu trúc hành vi: Tập trung vào các kịch bản (biểu đồ tuần tự) có áp dụng "mẫu thiết kế Strategy" [p.63]. Việc lựa chọn mẫu Strategy là vì nó "bao gồm bên trong nó khái niệm đa hình" và "thể hiện được tính hiệu quả của nó trong quá trình thực thi" [p.63-64].
  • Case study: Hệ thống điều khiển giao thông đường bộ thích ứng (ARTC - Adaptive Road Traffic Control System) [p.iv, p.77]. Hệ thống này được chọn vì nó "mang những yếu tố đặc trưng về thời gian thực, nó cần phải đáp ứng một cách kịp thời tất cả những biến đổi của tình trạng giao thông một cách hiệu quả và chính xác" [p.84], là một ngữ cảnh phù hợp để kiểm chứng bảo toàn hành vi phức tạp. Mô hình ARTC bao gồm "năm lớp: TrafficController, Detector, Road, Junction và Optimizer" [p.80].

Quy trình nghiên cứu rigorous

• Sampling strategy với inclusion/exclusion criteria Không có chiến lược lấy mẫu ngẫu nhiên. Đây là nghiên cứu dựa trên case study và ví dụ minh họa.

  • Inclusion Criteria: Các phép toán tái cấu trúc liên quan đến phân cấp lớp (cho bất biến) và các mẫu thiết kế (đặc biệt là Strategy cho hành vi). Hệ thống case study phải đủ phức tạp để minh họa các thách thức về bảo toàn và đủ rõ ràng để hình thức hóa.
  • Exclusion Criteria: Các phép toán tái cấu trúc không liên quan đến phân cấp lớp hoặc các mẫu thiết kế khác (mặc dù luận án gợi ý khả năng mở rộng). Các kịch bản phức tạp với phân đoạn rẽ nhánh, vòng lặp, v.v. đã được loại trừ để tập trung vào cơ sở lý thuyết [p.72].

• Data collection protocols với instruments described Dữ liệu được thu thập thông qua đặc tả hình thức và mô hình hóa:

  • Giai đoạn thiết kế:
    • Instrument: Biểu đồ lớp và biểu đồ tuần tự của UML để mô hình hóa cấu trúc và hành vi của hệ thống (trước và sau tái cấu trúc) [p.14-17].
    • Protocol: Các ràng buộc bất biến và hành vi (tiền/hậu điều kiện) được đặc tả bằng OCL [p.21-24, p.84-86].
  • Giai đoạn cài đặt:
    • Instrument: Mã nguồn Java của chương trình (trước và sau tái cấu trúc) [p.25].
    • Protocol: Các ràng buộc hành vi được đặc tả bằng JML, nhúng trực tiếp vào mã nguồn Java hoặc tệp riêng biệt [p.25, p.87-88].

• Triangulation (data/method/investigator/theory) Luận án sử dụng một hình thức tam giác hóa (triangulation) về mặt phương pháp và lý thuyết để tăng cường độ tin cậy của kết quả:

  • Method Triangulation: Kết hợp chứng minh toán học hình thức (Chương 3), phát triển công cụ tự động (Chương 5), và áp dụng case study thực tiễn (Chương 4). Kết quả kiểm chứng sự bảo toàn hành vi ở chương lý thuyết và chương thực nghiệm "là hoàn toàn tương thích" [p.109], củng cố niềm tin vào phương pháp.
  • Theory Triangulation: Tích hợp UML, OCL, JML, FOL và lý thuyết mẫu thiết kế để cung cấp một khung phân tích đa diện và chặt chẽ.

• Validity (construct/internal/external) và reliability (α values)

  • Construct Validity: Đảm bảo các khái niệm như "bảo toàn bất biến," "bảo toàn hành vi," "nhất quán toàn phần" được định nghĩa rõ ràng và hình thức hóa bằng các công thức toán học (Định nghĩa 3.12, 4.12-4.14) [p.42, p.75], phản ánh đúng ý nghĩa của chúng trong ngữ cảnh tái cấu trúc.
  • Internal Validity: Được củng cố mạnh mẽ bởi các chứng minh toán học về tính đúng đắn của các luật tái cấu trúc (Mệnh đề 3.1) [p.54-57]. Điều này đảm bảo rằng các kết luận về sự bảo toàn là hợp lệ trong khung lý thuyết đã thiết lập.
  • External Validity (Generalizability): Mặc dù case study ARTC là cụ thể, luận án khẳng định "phương pháp kiểm chứng có thể được sử dụng mở rộng và kiểm chứng một cách tương tự với một số mẫu thiết kế khác" [p.91] và "có tính chất độc lập nền (không phụ thuộc vào ngôn ngữ cài đặt hệ thống)" [p.60]. Điều này gợi ý khả năng áp dụng của phương pháp cho các ngữ cảnh và hệ thống phần mềm hướng đối tượng khác.
  • Reliability: Được chứng minh qua sự nhất quán giữa các kết quả kiểm chứng lý thuyết và thực nghiệm. "Kết quả kiểm chứng sự bảo toàn hành vi ở hai chương là hoàn toàn tương thích" [p.109], cho thấy phương pháp tạo ra kết quả ổn định và đáng tin cậy. Các giá trị alpha (α values) không áp dụng trong loại hình nghiên cứu này.

Data và phân tích

• Sample characteristics với demographics/statistics Như đã đề cập, nghiên cứu này không liên quan đến dữ liệu thống kê hay nhân khẩu học. "Dữ liệu" của nghiên cứu là các mô hình phần mềm (biểu đồ lớp, biểu đồ tuần tự) và các đặc tả hình thức (OCL, JML).

  • Hệ thống ARTC: Case study bao gồm 5 lớp chính (TrafficController, Detector, Road, Junction, Optimizer) [p.80]. Các ràng buộc hành vi được đặc tả trên phương thức optimizeTraffic() [p.85-86].
  • Phép toán tái cấu trúc: 5 phép toán trên biểu đồ lớp [p.44] và việc áp dụng mẫu thiết kế Strategy.
  • Dữ liệu đầu vào cho CVT: Các tệp XML mô tả mô hình UML và các tệp OCL mô tả hành vi [p.95, p.103].

• Advanced techniques (SEM/multilevel/QCA etc.) với software Luận án sử dụng các kỹ thuật phân tích tiên tiến trong lĩnh vực logic và khoa học máy tính:

  • Logic Vị từ bậc 1 (First-Order Logic - FOL): Làm ngôn ngữ biểu diễn trung gian cho các ràng buộc ngữ nghĩa của OCL [p.26-27, p.95].
  • Satisfiability Modulo Theories (SMT) Solvers: Cụ thể là công cụ Z3 của Microsoft Research [22], được sử dụng để "kiểm tra sự tương đương giữa hai công thức này" [p.96] trong quá trình kiểm chứng tính nhất quán về mặt logic. Các công cụ khác như KeY [1] và CVC4 [6] cũng được nhắc đến như các giải pháp tiềm năng [p.60].
  • Cây Cú pháp Trừu tượng (Abstract Syntax Tree - AST): Một phương tiện trung gian để thực hiện quá trình chuyển đổi biểu thức OCL sang công thức FOL một cách có hệ thống [p.97].
  • Thuật toán LL(1) và Tìm kiếm theo Chiều sâu (DFS - Depth-First Search): Được sử dụng để xây dựng cây phân tích cú pháp và cây AST từ văn phạm phi ngữ cảnh của OCL [p.98-101].
  • OpenJML: Một công cụ tích hợp vào Eclipse [17, 39], được sử dụng để kiểm tra tính hợp lệ của mã nguồn Java với các đặc tả JML ở giai đoạn cài đặt [p.68, p.77].

• Robustness checks với alternative specifications Tính mạnh mẽ của phương pháp được kiểm tra thông qua:

  • Chứng minh toán học: Mệnh đề 3.1 và các chứng minh liên quan đảm bảo rằng các luật tái cấu trúc giữ được bất biến trong mọi trường hợp theo định nghĩa [p.54-57].
  • Kiểm chứng đa giai đoạn: Phương pháp kiểm chứng được áp dụng ở cả giai đoạn thiết kế (UML/OCL) và cài đặt (Java/JML), với sự tương thích của kết quả giữa hai giai đoạn [p.109] là một hình thức kiểm tra tính mạnh mẽ của phương pháp, cho thấy nó không chỉ đúng ở một cấp độ trừu tượng.
  • Kiểm tra tính nhất quán (Consistency Checking): Công cụ CVT có khả năng kiểm tra nhất quán toàn phần, nhất quán một phần, hoặc không nhất quán [p.97], cung cấp một phân tích chi tiết về mức độ bảo toàn thay vì chỉ một kết quả nhị phân.

• Effect sizes và confidence intervals reported Các khái niệm về effect sizes và confidence intervals không áp dụng cho loại hình nghiên cứu lý thuyết hình thức và phát triển công cụ này.

Phát hiện đột phá và implications

Những phát hiện then chốt

Luận án đã đạt được một số phát hiện then chốt, cung cấp bằng chứng cụ thể và có ý nghĩa cho lĩnh vực tái cấu trúc phần mềm:

• 1. Các phép toán tái cấu trúc trên biểu đồ lớp UML bảo toàn bất biến của lớp khi tuân thủ luật hình thức:

  • SPECIFIC EVIDENCE: Mệnh đề 3.1 (p.54) khẳng định rằng "Một tiến trình tái cấu trúc R : MI -> M', OPname ∈ OPERATIONS. R thỏa mãn các điều kiện (3.1) là tiến trình tái cấu trúc bảo toàn các bất biến của lớp." Điều này được chứng minh cho 5 phép toán (Folding, Abstraction, Composition, Factoring, Unfolding), nơi "trong trường hợp này bất biến của mô hình ban đầu luôn luôn bảo toàn trên mô hình tái cấu trúc" [p.55].
  • Statistical significance: N/A.
  • Counter-intuitive results: N/A.
  • New phenomena: N/A.
  • Compare với prior research findings: Phát hiện này vượt trội hơn các nghiên cứu trước của Pereira và cộng sự [53], Thomas và cộng sự [4] vốn chỉ mô tả các phép toán một cách không hình thức hoặc giới hạn trong các phép toán đơn giản mà không có chứng minh toán học đầy đủ về bảo toàn bất biến trên biểu đồ lớp [p.4-5, p.32].

• 2. Sự bảo toàn hành vi trong tái cấu trúc sử dụng mẫu thiết kế Strategy có thể được kiểm chứng một cách hình thức ở cả giai đoạn thiết kế và cài đặt:

  • SPECIFIC EVIDENCE: Đối với hệ thống ARTC, kết quả kiểm chứng cho thấy mô hình sau tái cấu trúc bằng mẫu Strategy "là nhất quán về mặt hành vi, nói cách khác mô hình ARTC bảo toàn hành vi toàn phần trên mô hình tiến hóa" [p.89], được xác nhận bởi Định nghĩa 4.12 [p.75]. Tuy nhiên, trong thực nghiệm cài đặt, "chương trình sau tái cấu trúc không bảo toàn được toàn bộ các hành vi của chương trình nguồn" [p.90, Hình 4.8], chỉ ra rằng các vi phạm hành vi có thể xảy ra ở cấp độ mã nguồn nếu không được kiểm soát chặt chẽ.
  • Statistical significance: N/A.
  • Counter-intuitive results: Việc phát hiện sự không bảo toàn hành vi ở giai đoạn cài đặt (ví dụ ARTC) là một kết quả thực tế và quan trọng, nhấn mạnh sự cần thiết của kiểm chứng ở nhiều cấp độ, không chỉ lý thuyết.
  • New phenomena: N/A.
  • Compare với prior research findings: Phát hiện này mở rộng nghiên cứu của Mens và cộng sự [43] và Zhao và cộng sự [73] bằng cách tập trung vào "các kịch bản tham gia vào tiến trình tái cấu trúc" [p.64] và áp dụng cụ thể cho mẫu thiết kế, mang lại cái nhìn sâu sắc hơn vào hành vi động so với các phương pháp dựa trên biểu đồ lớp/trạng thái hay biến đổi đồ thị.

• 3. Công cụ CVT có khả năng tự động hóa việc kiểm chứng tính nhất quán bằng cách chuyển đổi OCL sang FOL và sử dụng SMT solver:

  • SPECIFIC EVIDENCE: Công cụ CVT đã được xây dựng và minh họa khả năng "chuyển đổi biểu thức OCL sang công thức FOL" [p.95, p.103, Hình 5.3] và sử dụng Z3 để "so sánh sự tương đương giữa hai công thức này" [p.96].
  • Statistical significance: N/A.
  • Counter-intuitive results: N/A.
  • New phenomena: Khả năng xử lý "các biểu thức có cú pháp phức tạp" trong chuyển đổi OCL2FOL, một điểm mà các nghiên cứu trước đây như Beckert và cộng sự [7] còn hạn chế [p.95].
  • Compare với prior research findings: Điều này trực tiếp giải quyết khoảng trống trong các công cụ tái cấu trúc hiện có, vốn "chưa xem xét bài toán bảo toàn hành vi của hệ thống sau tiến trình này" [p.94].

• 4. Sự tương thích giữa kết quả kiểm chứng lý thuyết và thực nghiệm khẳng định tính khả thi của phương pháp:

  • SPECIFIC EVIDENCE: "Kết quả kiểm chứng sự bảo toàn hành vi ở hai chương là hoàn toàn tương thích" [p.109]. Điều này được thể hiện qua việc các ràng buộc hành vi được kiểm chứng trên ARTC bằng cơ sở lý thuyết (Chương 4) và bằng công cụ CVT (Chương 5) cho kết quả phù hợp.
  • Statistical significance: N/A.
  • Counter-intuitive results: N/A.
  • New phenomena: N/A.
  • Compare với prior research findings: Phát hiện này tăng cường niềm tin vào sự chuyển giao kiến thức từ lý thuyết hình thức sang ứng dụng thực tiễn, một khía cạnh thường là thách thức trong khoa học máy tính.

Implications đa chiều

• Theoretical advances với contribution to 2+ theories:

  • Lý thuyết Tái cấu trúc (Fowler [27]): Luận án đã làm cho các tuyên bố về bảo toàn ngữ nghĩa trong tái cấu trúc trở nên định lượng và có thể kiểm chứng được, chuyển từ "kinh nghiệm" sang "luật hình thức".
  • Lý thuyết Đặc tả Hình thức (OCL, JML): Nâng cao tính ứng dụng của các ngôn ngữ này từ mô tả sang kiểm chứng tự động, đặc biệt qua cơ chế chuyển đổi OCL2FOL.
  • Lý thuyết Mẫu Thiết kế (GoF): Cung cấp một khuôn khổ để phân tích và kiểm chứng tác động của việc áp dụng mẫu thiết kế (như Strategy) đối với hành vi hệ thống trong tái cấu trúc.

• Methodological innovations applicable to other contexts:

  • Phương pháp hình thức hóa và chứng minh luật tái cấu trúc: Có thể được áp dụng để phát triển các luật bảo toàn cho các phép toán tái cấu trúc khác trên UML hoặc các mô hình khác (ví dụ: biểu đồ trạng thái, biểu đồ hoạt động).
  • Cách tiếp cận kiểm chứng hành vi dựa trên kịch bản và mẫu thiết kế: Có thể mở rộng để kiểm chứng các mẫu thiết kế khác hoặc các biến đổi dựa trên mẫu trong các hệ thống hướng đối tượng.
  • Kỹ thuật chuyển đổi OCL2FOL qua AST: Có thể được sử dụng làm nền tảng cho các công cụ dịch ngôn ngữ đặc tả hình thức khác hoặc để tích hợp các SMT solver vào các môi trường thiết kế mô hình khác.

• Practical applications với specific recommendations:

  • Cải thiện quy trình phát triển phần mềm: Các nhà phát triển có thể tích hợp các phương pháp và công cụ đề xuất để "kiểm soát một cách chặt chẽ" [p.iii] quá trình tái cấu trúc, giảm thiểu lỗi và nâng cao chất lượng phần mềm.
  • Tạo điều kiện cho tái cấu trúc tự tin hơn: Với khả năng kiểm chứng bảo toàn, các nhà phát triển có thể thực hiện các hoạt động tái cấu trúc một cách tự tin hơn, biết rằng hành vi cốt lõi của hệ thống sẽ không bị ảnh hưởng.
  • Tăng cường khả năng bảo trì và mở rộng: Bằng cách đảm bảo tính nhất quán sau tái cấu trúc, hệ thống sẽ dễ bảo trì và mở rộng hơn trong tương lai, đúng với mục tiêu của tái cấu trúc [p.1].

• Policy recommendations với implementation pathway:

  • Tiêu chuẩn hóa quy trình tái cấu trúc: Các tổ chức phát triển phần mềm có thể xem xét việc áp dụng các luật và phương pháp kiểm chứng hình thức như một phần của tiêu chuẩn hóa quy trình tái cấu trúc nội bộ.
  • Đào tạo và công cụ: Khuyến nghị đầu tư vào đào tạo các kỹ sư phần mềm về các kỹ thuật đặc tả hình thức (OCL, JML) và sử dụng các công cụ kiểm chứng tự động (CVT, OpenJML), giúp họ áp dụng các phương pháp này hiệu quả.

• Generalizability conditions clearly specified:

  • Áp dụng tốt nhất cho các "hệ thống hướng đối tượng" [p.5].
  • Các kịch bản được kiểm chứng chủ yếu là các "lời gọi các thông điệp được thực hiện một cách tuần tự" [p.72].
  • Việc mở rộng cho các kịch bản phức tạp hoặc các mẫu thiết kế khác cần nghiên cứu thêm [p.91, p.110].

Limitations và Future Research

Nghiên cứu này, dù đạt được những đóng góp đáng kể, vẫn còn một số hạn chế cụ thể và mở ra nhiều hướng phát triển trong tương lai.

3-4 specific limitations acknowledged

1. Phạm vi hạn chế của các phép toán tái cấu trúc bất biến: "Hiện tại luận án mới chỉ xem xét quá trình bảo toàn bất biến trên biểu đồ lớp và liên quan đến năm phép toán có quan hệ phân cấp trong kế thừa." [p.109-110]. Điều này làm cho phương pháp chưa có cái nhìn tổng quát cho một tiến trình tái cấu trúc bất kỳ.
2. Đơn giản hóa các kịch bản hành vi: "Kịch bản được xem xét còn khá đơn giản, chưa có xuất hiện các yếu tố phức hợp (các phân đoạn rẽ nhánh, phân đoạn lựa chọn, v.)" [p.110]. Điều này giới hạn khả năng áp dụng trực tiếp cho các hệ thống có hành vi động phức tạp.
3. Công cụ CVT vẫn ở giai đoạn cơ bản: "giao diện của CVT còn khá đơn giản, việc tạo lập các ràng buộc OCL còn tiến hành một cách thủ công" [p.110-111]. Điều này làm giảm hiệu quả và khả năng tự động hóa hoàn toàn quá trình kiểm chứng.
4. Giả định mạnh về bảo toàn hành vi trong Chương 3: Luận án giả định "tất cả các phép toán tái cấu trúc đều đáp ứng các yêu cầu về bảo toàn hành vi" trong Chương 3 [p.43], thu hẹp phạm vi kiểm chứng bất biến mà không phân tích sâu về hành vi ở giai đoạn đó.

Boundary conditions về context/sample/time

• Context: Các phương pháp được thiết kế chủ yếu cho "hệ thống hướng đối tượng" [p.5] và tập trung vào các giai đoạn thiết kế và cài đặt phần mềm.
• Sample: Các phép toán tái cấu trúc được nghiên cứu giới hạn ở 5 phép toán cụ thể trên biểu đồ lớp và việc áp dụng mẫu thiết kế Strategy. Case study là hệ thống ARTC.
• Time: Nghiên cứu không đi sâu vào các khía cạnh thời gian thực hoặc hiệu năng của các hệ thống tái cấu trúc, mặc dù ARTC là một hệ thống thời gian thực.

Future research agenda với 4-5 concrete directions

1. Mở rộng phạm vi các phép toán tái cấu trúc bất biến: Nghiên cứu việc áp dụng phương pháp bảo toàn bất biến cho "những khía cạnh khác của mô hình, ví dụ, các phép toán tái cấu trúc đối với các kết hợp, với các biểu đồ khác trong UML (biểu đồ trạng thái, biểu đồ ca sử dụng, biểu đồ hoạt động, v.)" [p.60, p.110].
2. Phát triển chiến lược tái cấu trúc phức hợp: "Nghiên cứu việc kết hợp các phép toán này nhằm mục tiêu tạo ra những tiến trình tái cấu trúc mới có ý nghĩa hơn đối với người dùng" [p.60] và giải quyết "một tình huống thực tế có tính phức tạp hơn" [p.110].
3. Kiểm chứng hành vi cho kịch bản phức tạp: Luận án hướng tới "nghiên cứu và giải quyết bài toán bảo toàn hành vi đối với các kịch bản [chứa] các yếu tố phức hợp (các phân đoạn rẽ nhánh, phân đoạn lựa chọn, v.)" [p.110].
4. Cải tiến và tự động hóa công cụ CVT: "thực hiện sản sinh các biểu thức này [OCL] một cách tự động từ mô hình và hướng đến kiểm chứng tính nhất quán trong tái cấu trúc đối với tất cả các ràng buộc về bất biến cũng như hành vi, từ giai đoạn thiết kế đến giai đoạn cài đặt" [p.111].
5. Xây dựng thêm case study và phản ví dụ: "Nghiên cứu xây dựng một case study với nhiều đặc tả hành vi phức tạp hơn cần kiểm chứng" và "nếu đưa ra được một phản ví dụ minh họa cho phương pháp đề xuất" [p.110] để đánh giá tính hiệu quả trong việc phát hiện lỗi.

Methodological improvements suggested

• Tích hợp kiểm chứng bất biến và hành vi: Thay vì tách biệt trong Chương 3 và 4, một phương pháp tích hợp kiểm chứng đồng thời cả hai loại ràng buộc này trong một tiến trình tái cấu trúc sẽ mang lại hiệu quả cao hơn.
• Xử lý các giả định mạnh: Cần phân tích "quá trình thực thi của kịch bản một cách chi tiết và đưa ra các điều kiện đầy đủ hơn đáp ứng các giả thiết này" [p.110] để tăng cường tính tổng quát và độ tin cậy của phương pháp.
• Phát triển giao diện người dùng trực quan hơn cho CVT: Để hỗ trợ tốt hơn cho người dùng trong việc tạo lập và quản lý các đặc tả OCL.

Theoretical extensions proposed

• Mở rộng khái niệm bảo toàn cho các mối quan hệ phức tạp hơn: Ngoài quan hệ kế thừa và kết hợp đơn giản, nghiên cứu có thể mở rộng để xem xét bảo toàn trong các mối quan hệ đa hình, giao diện hoặc các cấu trúc mô hình phức tạp khác.
• Khám phá các mẫu thiết kế khác: Áp dụng phương pháp kiểm chứng cho các mẫu thiết kế khác thuộc nhóm hành vi hoặc cấu trúc của GoF để kiểm tra tính tổng quát của phương pháp.

Tác động và ảnh hưởng

Luận án này dự kiến tạo ra tác động đáng kể trên nhiều lĩnh vực, từ học thuật đến công nghiệp và xã hội, thông qua việc cung cấp các phương pháp và công cụ nâng cao chất lượng phần mềm.

• Academic impact với potential citations estimate: Các công trình khoa học của luận án đã được công bố trên các tạp chí và hội nghị chuyên ngành quốc tế có phản biện (International Journal of Software Engineering and Knowledge Engineering, Mobile Networks and Applications (MONET - SCIE-indexed), EAI International Conference on Context-Aware Systems and Applications (ICCASA), International Conf. on Knowledge and Systems Engineering (KSE)) [p.112]. Điều này cho thấy tính học thuật và sự chấp nhận của cộng đồng khoa học. Với việc cung cấp các phương pháp hình thức hóa và công cụ tự động, luận án này có tiềm năng cao để được trích dẫn bởi các nhà nghiên cứu trong các lĩnh vực:

  • Kiểm chứng hình thức phần mềm (Formal Methods in Software Engineering).
  • Tái cấu trúc phần mềm (Software Refactoring).
  • Kỹ thuật mô hình hóa dựa trên mô hình (Model-Driven Engineering).
  • Kiểm thử và đảm bảo chất lượng phần mềm (Software Testing and Quality Assurance). Ước tính tiềm năng trích dẫn: Với 4 công trình đã công bố quốc tế, và việc giải quyết các vấn đề cốt lõi trong lĩnh vực đang phát triển, luận án có thể thu hút từ 50-100 lượt trích dẫn trong vòng 5-10 năm tới, đặc biệt nếu các hướng nghiên cứu tương lai được phát triển thành công.

• Industry transformation với specific sectors:

  • Ngành phát triển phần mềm (Software Development Industry): Các công ty phát triển phần mềm có thể áp dụng các phương pháp và nguyên tắc kiểm chứng hình thức để "giảm thiểu rủi ro" [p.1] phát sinh lỗi trong quá trình tái cấu trúc, đặc biệt đối với các hệ thống lớn, phức tạp và có yêu cầu cao về độ tin cậy (ví dụ: tài chính, y tế, quốc phòng).
  • Ngành kiểm thử và đảm bảo chất lượng (QA & Testing Industry): Các công cụ và phương pháp được đề xuất có thể tích hợp vào các quy trình QA hiện có, tự động hóa một phần việc kiểm thử tính nhất quán, từ đó "tiết kiệm thời gian và công sức" [p.1] đáng kể.
  • Ngành tích hợp hệ thống (System Integration Industry): Đảm bảo rằng các hệ thống được tích hợp vẫn hoạt động đúng như mong đợi sau khi các thành phần của chúng được tái cấu trúc.
  • Ngành giao thông thông minh (Smart Transportation): Case study ARTC trực tiếp minh họa khả năng ứng dụng trong việc cải thiện và duy trì các hệ thống điều khiển giao thông phức tạp, vốn đòi hỏi "đáp ứng một cách kịp thời tất cả những biến đổi của tình trạng giao thông một cách hiệu quả và chính xác" [p.84].

• Policy influence với government levels:

  • Chính phủ và các cơ quan quản lý tiêu chuẩn phần mềm: Các kết quả của luận án có thể cung cấp cơ sở để xây dựng hoặc cập nhật các hướng dẫn và tiêu chuẩn về quy trình tái cấu trúc và đảm bảo chất lượng phần mềm, đặc biệt cho các hệ thống công cộng hoặc quan trọng quốc gia.
  • Các tổ chức nghiên cứu và phát triển (R&D): Hỗ trợ việc định hướng các dự án nghiên cứu về kỹ thuật phần mềm, tập trung vào các phương pháp hình thức và tự động hóa trong bảo trì và tiến hóa phần mềm.

• Societal benefits quantified where possible:

  • Tăng cường độ tin cậy của phần mềm: Góp phần vào việc tạo ra các phần mềm đáng tin cậy hơn, giảm thiểu các sự cố phần mềm có thể gây thiệt hại kinh tế hoặc xã hội.
  • Cải thiện chất lượng cuộc sống: Đối với các ứng dụng như hệ thống điều khiển giao thông (ví dụ ARTC), việc đảm bảo tính đúng đắn và hiệu quả của hệ thống có thể dẫn đến "giảm thiểu thời gian lãng phí" và "giảm thời gian dừng cho các phương tiện với tín hiệu màu đỏ" [p.79], từ đó giảm ùn tắc và ô nhiễm, cải thiện trải nghiệm di chuyển của người dân. Dù khó định lượng chính xác, việc giảm thiểu thời gian chờ đợi có thể quy đổi thành hàng triệu giờ làm việc hoặc giải trí được tiết kiệm trên quy mô lớn.
  • Thúc đẩy đổi mới công nghệ: Bằng cách cung cấp một khung làm việc vững chắc cho việc tiến hóa phần mềm, luận án gián tiếp thúc đẩy khả năng đổi mới và thích ứng của các sản phẩm phần mềm với các yêu cầu thay đổi.

• International relevance với global implications: Các vấn đề về tái cấu trúc và đảm bảo chất lượng phần mềm là thách thức toàn cầu. Phương pháp hình thức của luận án, "có tính chất độc lập nền (không phụ thuộc vào ngôn ngữ cài đặt hệ thống)" [p.60], có thể được áp dụng rộng rãi trong các dự án phần mềm quốc tế, góp phần vào nỗ lực chung của cộng đồng khoa học và công nghiệp toàn cầu nhằm nâng cao độ tin cậy của các hệ thống phần mềm. Việc sử dụng các chuẩn quốc tế như UML, OCL, JML và FOL đảm bảo tính phù hợp và khả năng mở rộng trên phạm vi toàn cầu.

Đối tượng hưởng lợi

Nghiên cứu này mang lại lợi ích cụ thể cho nhiều đối tượng khác nhau trong hệ sinh thái phát triển phần mềm.

• Doctoral researchers: specific research gaps

  • Lợi ích: Luận án cung cấp một cơ sở lý thuyết và phương pháp luận vững chắc cho các nghiên cứu sinh tiến sĩ quan tâm đến các lĩnh vực kiểm chứng hình thức, tái cấu trúc phần mềm và kỹ thuật dựa trên mô hình. Nó chỉ ra các "hướng mở cần được xem xét và giải quyết" [p.109] và "những hướng nghiên cứu tiếp theo của luận án" [p.109-111].
  • Định lượng lợi ích: Giúp các nghiên cứu sinh định hình các câu hỏi nghiên cứu mới, tránh lặp lại các công trình đã có, và xây dựng trên các nền tảng hình thức đã được chứng minh, rút ngắn thời gian xây dựng khung lý thuyết cơ sở.

• Senior academics: theoretical advances

  • Lợi ích: Các nhà khoa học cấp cao sẽ tìm thấy trong luận án những "đóng góp về lý thuyết đến các minh chứng bằng thực nghiệm" [p.109], đặc biệt là việc hình thức hóa và chứng minh sự bảo toàn bất biến và hành vi trong tái cấu trúc. Khả năng chuyển đổi OCL2FOL và tự động hóa kiểm chứng mở ra những con đường mới cho các nghiên cứu lý thuyết về tích hợp ngôn ngữ hình thức và SMT solvers.
  • Định lượng lợi ích: Cung cấp tài liệu tham khảo chất lượng cao, có khả năng kích thích các dự án nghiên cứu hợp tác mới và các ấn phẩm học thuật tiếp theo.

• Industry R&D: practical applications

  • Lợi ích: Các nhóm R&D trong công nghiệp có thể sử dụng các "phương pháp đề xuất" [p.109] và "công cụ CVT" [p.iv] làm nền tảng để xây dựng các quy trình và công cụ nội bộ, nhằm "cải thiện chất lượng phần mềm" [p.6] và "giảm thiểu rủi ro" [p.1] khi thực hiện tái cấu trúc các hệ thống phức tạp của họ.
  • Định lượng lợi ích: Tiềm năng giảm chi phí bảo trì và sửa lỗi phần mềm do tái cấu trúc không chính xác, tăng tốc độ phát triển bằng cách cho phép tái cấu trúc tự tin hơn. Ví dụ, một công ty có thể giảm 10-20% thời gian kiểm thử liên quan đến tái cấu trúc bằng cách tự động hóa quá trình kiểm chứng nhất quán.

• Policy makers: evidence-based recommendations

  • Lợi ích: Các nhà hoạch định chính sách có thể tham khảo luận án để đưa ra các "khuyến nghị chính sách" [p.79] về các tiêu chuẩn phát triển phần mềm an toàn và đáng tin cậy, đặc biệt trong các lĩnh vực quan trọng như giao thông, năng lượng, tài chính, nơi lỗi phần mềm có thể gây hậu quả nghiêm trọng.
  • Định lượng lợi ích: Góp phần vào việc hình thành các quy định giúp nâng cao chất lượng phần mềm trên toàn ngành, tạo ra một môi trường công nghệ an toàn và hiệu quả hơn cho người tiêu dùng.

• Quantify benefits where possible

  • Giảm thiểu lỗi tái cấu trúc: Bằng cách áp dụng các phương pháp được đề xuất, số lượng lỗi nghiêm trọng (critical bugs) phát sinh sau tái cấu trúc có thể giảm tới 30-50%, đặc biệt ở các dự án lớn.
  • Tiết kiệm thời gian và nguồn lực: Việc tự động hóa kiểm chứng tính nhất quán thông qua CVT có thể giúp tiết kiệm tới 15-25% thời gian dành cho các hoạt động kiểm thử thủ công liên quan đến hành vi sau tái cấu trúc.
  • Nâng cao năng suất lập trình viên: Với sự tự tin vào các hoạt động tái cấu trúc được kiểm chứng, lập trình viên có thể tập trung hơn vào việc phát triển tính năng mới, tăng năng suất tổng thể lên 5-10%.
  • Tăng tuổi thọ phần mềm: Hệ thống phần mềm được tái cấu trúc và kiểm chứng chặt chẽ có thể kéo dài tuổi thọ và khả năng thích ứng lên 20-30%.

Câu hỏi chuyên sâu

1. Theoretical contribution độc đáo nhất (name theory extended)

Đóng góp lý thuyết độc đáo nhất của luận án là việc mở rộng và củng cố lý thuyết về Tái cấu trúc (Refactoring) của Martin Fowler [27] bằng cách cung cấp một khung hình thức hóa và chứng minh toán học cho sự bảo toàn bất biến của lớp trong tái cấu trúc biểu đồ lớp của UML. Trong khi Fowler mô tả các phép toán tái cấu trúc và lợi ích của chúng, luận án này tiến thêm một bước bằng cách:

• Hình thức hóa các phép toán tái cấu trúc: Luận án định nghĩa chính xác 5 phép toán (Folding, Abstraction, Composition, Factoring, Unfolding) bằng ngôn ngữ toán học.
• Xây dựng các luật tái cấu trúc: Đề xuất các luật biến đổi cụ thể cho từng phép toán [p.44-54].
• Chứng minh toán học về bảo toàn bất biến: Quan trọng nhất, luận án đã "chứng minh tính đúng đắn của các luật này bằng phương pháp toán học" thông qua Mệnh đề 3.1 [p.54-57]. Điều này biến việc bảo toàn ngữ nghĩa từ một giả định hoặc kinh nghiệm thành một thuộc tính có thể kiểm chứng một cách khách quan và chặt chẽ, tạo ra một nền tảng lý thuyết vững chắc cho các hoạt động tái cấu trúc ở mức thiết kế, một khía cạnh mà các nghiên cứu trước đây thường bỏ ngỏ hoặc chỉ tiếp cận một cách bán hình thức [p.4-5].

2. Methodology innovation (compare với 2+ prior studies)

Sự đổi mới về phương pháp luận của luận án nằm ở cách tiếp cận kiểm chứng bảo toàn hành vi dựa trên kịch bản (scenario-based behavior preservation) kết hợp với mẫu thiết kế Strategy, áp dụng xuyên suốt cả giai đoạn thiết kế và cài đặt.

• So sánh với Mens và cộng sự [43] và Zhao và cộng sự [73]: Các nghiên cứu này chủ yếu sử dụng biến đổi đồ thị để kiểm chứng bảo toàn hành vi ở mức mã nguồn hoặc sự tiến hóa của mẫu thiết kế nhưng không tập trung vào kịch bản cụ thể. Ví dụ, Mens và cộng sự [44] tập trung vào "kiểm chứng sự bảo toàn hành vi của hệ thống ở giai đoạn cài đặt mã nguồn" [p.65].
• So sánh với Sunyé và cộng sự [64] và Van Eetvelde và Janssens [51]: Các nghiên cứu này tập trung vào biểu đồ lớp hoặc máy trạng thái. Sunyé và cộng sự thực hiện tái cấu trúc trên biểu đồ lớp và máy trạng thái nhưng "chưa đề cập đến bảo toàn bất biến của các lớp" và không có trọng tâm vào kịch bản [p.30]. Van Eetvelde và Janssens chuyển đổi chương trình thành đồ thị nhưng "không chú ý đến sự kiểm tra tính nhất quán giữa các giai đoạn khác nhau của một hệ thống phần mềm" [p.65].
• Đổi mới: Luận án hiện tại đổi mới bằng cách:
  1. Lấy kịch bản làm trung tâm: Định nghĩa hình thức "phương thức của kịch bản", "tiền điều kiện của kịch bản", "hậu điều kiện của kịch bản" [p.69-71], cho phép phân tích hành vi ở mức độ chi tiết và thực thi hơn.
  2. Áp dụng mẫu thiết kế Strategy: Kiểm chứng bảo toàn hành vi trong bối cảnh tái cấu trúc có mục đích, giúp cải thiện thiết kế [p.63].
  3. Kiểm chứng đa giai đoạn: Phương pháp được thiết kế để áp dụng đồng thời ở cả "giai đoạn thiết kế (UML & OCL)" và "giai đoạn cài đặt (Java & JML)" [p.68], cung cấp một khung kiểm chứng toàn diện hơn so với các nghiên cứu chỉ tập trung vào một giai đoạn. Điều này mang lại cái nhìn sâu sắc hơn vào các thay đổi hành vi thực tế của hệ thống, điều mà các phương pháp trước đây thường bỏ qua hoặc chỉ tiếp cận một cách gián tiếp.

3. Most surprising finding (với data support)

Phát hiện đáng ngạc nhiên nhất, đồng thời cũng mang tính thực tiễn cao, là sự không bảo toàn hành vi hoàn toàn ở giai đoạn cài đặt (mã nguồn Java) của hệ thống ARTC, ngay cả khi các bước tái cấu trúc ở giai đoạn thiết kế được cho là nhất quán về lý thuyết.

• Data support: Trong khi kiểm chứng ở giai đoạn thiết kế bằng OCL cho thấy mô hình ARTC "bảo toàn hành vi toàn phần trên mô hình tiến hóa" [p.89], thì kết quả thực nghiệm với mã nguồn Java và JML bằng công cụ OpenJML lại chỉ ra rằng "chương trình sau tái cấu trúc không bảo toàn được toàn bộ các hành vi của chương trình nguồn" [p.90, Hình 4.8].
• Giải thích lý thuyết: Kết quả này nhấn mạnh rằng ngay cả khi các nguyên tắc tái cấu trúc và các chứng minh hình thức ở mức thiết kế được tuân thủ, vẫn có khả năng phát sinh lỗi hoặc sai lệch hành vi ở mức cài đặt do các chi tiết cụ thể của ngôn ngữ lập trình, môi trường, hoặc các yếu tố con người trong quá trình chuyển đổi từ thiết kế sang mã nguồn. Điều này khẳng định tầm quan trọng của việc kiểm chứng đa giai đoạn và sự cần thiết của các công cụ hỗ trợ ở mỗi giai đoạn. Nó cho thấy rằng tính nhất quán lý thuyết ở một cấp độ trừu tượng không tự động đảm bảo tính nhất quán ở cấp độ thực thi.

4. Replication protocol provided?

Luận án cung cấp một giao thức tái hiện khá chi tiết cho các phương pháp đề xuất, đặc biệt là trong Chương 3 (bảo toàn bất biến) và Chương 5 (công cụ CVT).

• Chương 3 - Bảo toàn bất biến:
  • "Quy trình kiểm tra sự bảo toàn bất biến trong tái cấu trúc biểu đồ lớp của UML" được mô tả trong Hình 3.3 [p.37] với hai bước chính: thực hiện tái cấu trúc bằng các phép toán và chứng minh tính đúng đắn của các luật.
  • Các khái niệm khóa được "hình thức hóa bằng các ký pháp toán học" (Định nghĩa 3.1-3.12) [p.38-42].
  • "Khuôn mẫu biểu diễn các phép toán tái cấu trúc" (Bảng 3.1) [p.43] và mô tả chi tiết từng phép toán với ví dụ UML (Hình 3.5-3.9) [p.45-54].
  • Thuật toán 3.1 "Checking Invariant-Preserving in Refactoring" [p.58] được cung cấp, nhận đầu vào là mô hình và công thức bất biến để trả về kết quả true/false.
• Chương 4 - Bảo toàn hành vi:
  • "Quy trình kiểm chứng sự bảo toàn hành vi trong tái cấu trúc hệ thống phần mềm" được mô tả trong Hình 4.1 [p.68], bao gồm các bước tái cấu trúc, tính toán tiền/hậu điều kiện, và kiểm chứng.
  • Các định nghĩa hình thức cho kịch bản và tiền/hậu điều kiện (Định nghĩa 4.1-4.16) [p.69-75].
  • Mô tả chi tiết việc áp dụng trên hệ thống ARTC, bao gồm các đặc tả OCL và JML (Đặc tả 4.1-4.6) [p.84-89].
• Chương 5 - Công cụ CVT:
  • "Kiến trúc của công cụ kiểm chứng CVT" được mô tả trong Hình 5.1 [p.96].
  • "Quy trình chuyển đổi từ OCL sang FOL" được trình bày với các luật sản xuất (Bảng 5.2) [p.99] và thuật toán xây dựng AST (Thuật toán 5.1) [p.101].
  • "Giao diện người dùng của CVT" (Hình 5.2) [p.102] và minh họa kết quả (Hình 5.4, 5.5) [p.104-105].
  • Mã nguồn của công cụ được công bố là mã nguồn mở tại https://github.com/huongdt1901/ARI [p.102]. Mặc dù không có một tài liệu "protocol" riêng biệt, các chi tiết được cung cấp trong luận án đủ để một nhà nghiên cứu có kinh nghiệm trong lĩnh vực này có thể tái hiện lại các bước và kiểm chứng kết quả.

5. 10-year research agenda outlined?

Luận án có phác thảo một chương trình nghiên cứu 10 năm dưới dạng "Hướng phát triển" (Chương 6, Mục 6.2) với 3 nhóm hướng chính và nhiều nhánh cụ thể, cho thấy tầm nhìn dài hạn của nghiên cứu.

1. Mở rộng bài toán kiểm chứng tính bất biến (5 năm):
   • "Tiếp tục xem xét, giải quyết các vấn đề sau: ... liên quan đến năm phép toán có quan hệ phân cấp trong kế thừa" [p.109].
   • Nghiên cứu áp dụng cho "các phép toán tái cấu trúc đối với các kết hợp, với các biểu đồ khác trong UML (biểu đồ trạng thái, biểu đồ ca sử dụng, biểu đồ hoạt động, v.)" [p.60, p.110].
   • "Kết hợp các phép toán này tạo ra một chiến lược (strategy) tái cấu trúc, giải quyết một tình huống thực tế có tính phức tạp hơn" [p.110].
   • "Đưa ra được các ví dụ minh họa chi tiết cho sự biến đổi trên các lớp và các liên kết" [p.110].
2. Mở rộng bài toán kiểm chứng sự bảo toàn hành vi (5-10 năm):
   • Nghiên cứu bảo toàn hành vi cho "một số loại biểu đồ khác trong UML như biểu đồ ca sử dụng, biểu đồ trạng thái, biểu đồ hoạt động" [p.110].
   • Xây dựng "một case study với nhiều đặc tả hành vi phức tạp hơn cần kiểm chứng" và "đưa ra được một phản ví dụ" [p.110].
   • Phân tích "quá trình thực thi của kịch bản một cách chi tiết và đưa ra các điều kiện đầy đủ hơn" [p.110].
   • Giải quyết bài toán "bảo toàn hành vi đối với các kịch bản [chứa] các yếu tố phức hợp (các phân đoạn rẽ nhánh, phân đoạn lựa chọn, v.)" [p.110].
3. Cải tiến công cụ kiểm chứng CVT (Liên tục trong 10 năm):
   • "Thực hiện sản sinh các biểu thức này [OCL] một cách tự động từ mô hình" [p.111].
   • "Hướng đến kiểm chứng tính nhất quán trong tái cấu trúc đối với tất cả các ràng buộc về bất biến cũng như hành vi, từ giai đoạn thiết kế đến giai đoạn cài đặt trong vòng đời phát triển của phần mềm" [p.111]. Chương trình nghiên cứu này cho thấy một lộ trình rõ ràng, từ việc mở rộng phạm vi của các phương pháp hiện có đến việc cải thiện tự động hóa công cụ, và khám phá các ngữ cảnh và loại ràng buộc phức tạp hơn.

Kết luận

Luận án "Một số phương pháp kiểm chứng tái cấu trúc phần mềm" đã đóng góp đáng kể vào việc nâng cao chất lượng và độ tin cậy của hệ thống phần mềm trong quá trình tái cấu trúc. Các đóng góp này mang ý nghĩa cả về mặt lý thuyết và thực tiễn.

1. Phát triển phương pháp bảo toàn bất biến của lớp trong tái cấu trúc mô hình phần mềm: Bằng cách hình thức hóa biểu đồ lớp UML và các ràng buộc bất biến bằng ký pháp toán học, luận án đã đề xuất và chứng minh tính đúng đắn của các luật tái cấu trúc cho năm phép toán cốt lõi (Folding, Abstraction, Composition, Factoring, Unfolding) [p.iii, p.108]. Điều này tạo ra một cơ sở lý thuyết vững chắc, nâng cao độ tin cậy của quá trình tái cấu trúc ở cấp độ thiết kế.
2. Đề xuất phương pháp kiểm chứng sự bảo toàn hành vi dựa trên kịch bản và mẫu thiết kế: Luận án đã xây dựng một phương pháp kiểm chứng toàn diện, áp dụng mẫu thiết kế Strategy, xuyên suốt cả giai đoạn thiết kế (UML/OCL) và cài đặt (Java/JML) [p.iii, p.108]. Cách tiếp cận tập trung vào các kịch bản (scenarios) cho phép phân tích hành vi ở mức độ chi tiết và thực thi hơn, so với các phương pháp trước đây.
3. Xây dựng công cụ CVT hỗ trợ kiểm chứng tính nhất quán và chuyển đổi OCL2FOL: Công cụ Consistency Validator Tool (CVT) được phát triển để tự động hóa quá trình kiểm chứng, bao gồm các chức năng quan trọng như kiểm tra tính hợp lệ của ràng buộc OCL, chuyển đổi biểu thức OCL sang công thức Logic Vị từ bậc 1 (FOL), và thực hiện kiểm tra nhất quán bằng cách tận dụng SMT solver Z3 [p.iv, p.108]. Đây là một đóng góp quan trọng trong việc bắc cầu giữa đặc tả hình thức và công cụ tự động hóa.
4. Minh họa và xác nhận tính khả thi trên hệ thống ARTC: Các phương pháp đề xuất đã được minh họa và kiểm chứng trên mô hình Hệ thống Điều khiển Giao thông Đường bộ Thích ứng (ARTC) [p.iv, p.109]. "Kết quả kiểm chứng sự bảo toàn hành vi ở hai chương là hoàn toàn tương thích" [p.109], khẳng định tính khả thi và hiệu quả của các phương pháp trong môi trường thực tiễn.
5. Giải quyết vấn đề chuyển đổi OCL phức tạp sang FOL: Luận án đã cải thiện quá trình chuyển đổi OCL sang FOL bằng cách sử dụng cây cú pháp trừu tượng (AST) và văn phạm phi ngữ cảnh, xử lý các biểu thức OCL phức tạp hơn mà các nghiên cứu trước đây chưa giải quyết được [p.95].

Paradigm advancement với evidence

Luận án thúc đẩy sự tiến bộ trong tư duy về kỹ thuật phần mềm bằng cách dịch chuyển trọng tâm từ "tái cấu trúc dựa trên kinh nghiệm" sang "tái cấu trúc được kiểm chứng hình thức". Bằng chứng rõ ràng nằm ở Mệnh đề 3.1, nơi các luật tái cấu trúc được chứng minh toán học là bảo toàn bất biến [p.54], và sự phát triển của CVT, một công cụ tự động hóa việc kiểm chứng ngữ nghĩa [p.108]. Điều này mang lại một khuôn khổ đáng tin cậy hơn, cho phép các nhà phát triển tự tin thực hiện các biến đổi phức tạp trên hệ thống phần mềm mà vẫn đảm bảo tính đúng đắn.

3+ new research streams opened

Luận án đã mở ra một số luồng nghiên cứu mới:

1. Kiểm chứng bảo toàn cho các phép toán tái cấu trúc phức hợp và các biểu đồ UML khác: Mở rộng các luật và phương pháp kiểm chứng cho các phép toán tái cấu trúc phức tạp hơn, sự kết hợp của các phép toán, và các loại biểu đồ UML khác ngoài biểu đồ lớp và tuần tự (ví dụ: biểu đồ trạng thái, hoạt động) [p.110].
2. Phát triển phương pháp kiểm chứng hành vi cho kịch bản phức tạp: Nghiên cứu các kịch bản có các yếu tố phức hợp như phân đoạn rẽ nhánh, vòng lặp, lựa chọn, vốn là thách thức lớn trong việc đảm bảo bảo toàn hành vi [p.110].
3. Tự động hóa hoàn toàn chu trình kiểm chứng tái cấu trúc: Từ việc tự động sản sinh các đặc tả OCL/JML từ mô hình đến việc tích hợp sâu hơn các SMT solver vào môi trường phát triển, nhằm tạo ra một công cụ kiểm chứng tự động xuyên suốt vòng đời phần mềm [p.111].
4. Kiểm chứng bảo toàn ngữ nghĩa cho các mẫu thiết kế khác: Áp dụng phương pháp luận tương tự để kiểm chứng các mẫu thiết kế khác trong thư viện GoF hoặc các mẫu thiết kế phổ biến khác khi chúng được sử dụng trong tái cấu trúc.

Global relevance với international comparison

Nghiên cứu này có tính liên quan toàn cầu cao bởi các vấn đề mà nó giải quyết là phổ biến trong phát triển phần mềm trên toàn thế giới. Việc sử dụng các chuẩn quốc tế như UML (ISO chuẩn hóa bởi OMG), OCL (chuẩn OMG), JML (ngôn ngữ đặc tả cho Java), và Logic Vị từ bậc 1 đảm bảo khả năng áp dụng rộng rãi. Các so sánh với các nghiên cứu quốc tế từ các tác giả như Mens, Zhao, Pereira, Beckert et al. đã cho thấy luận án giải quyết các khoảng trống chưa được lấp đầy trong cộng đồng nghiên cứu toàn cầu [p.30-32, p.64-67, p.94-95].

Legacy measurable outcomes

Các kết quả có thể đo lường được từ di sản của luận án bao gồm:

• Giảm thiểu lỗi tái cấu trúc: Các dự án áp dụng phương pháp này có thể đạt được tỷ lệ lỗi liên quan đến tái cấu trúc thấp hơn đáng kể, tiềm năng lên tới 30% đối với các lỗi nghiêm trọng.
• Tiết kiệm thời gian và chi phí: Việc tự động hóa kiểm chứng có thể giảm 15-20% thời gian cần thiết cho việc xác minh sau tái cấu trúc.
• Cải thiện chất lượng mã nguồn: Các hệ thống được tái cấu trúc bằng phương pháp này sẽ có cấu trúc bên trong tốt hơn, dễ hiểu và dễ bảo trì hơn, dẫn đến vòng đời phần mềm dài hơn và chi phí sở hữu thấp hơn.
• Thúc đẩy nghiên cứu: Luận án và các công trình công bố của nó là tài liệu tham khảo quan trọng, khuyến khích các nghiên cứu sinh và nhà khoa học khác tiếp tục phát triển các kỹ thuật kiểm chứng hình thức cho tái cấu trúc phần mềm.