Tổng quan về luận án

Sự bùng nổ của các thiết bị di động thông minh trong kỷ nguyên số đặt ra những thách thức công nghệ nghiêm trọng về giới hạn thời lượng pin. Mặc dù công nghệ vi xử lý di động ngày càng được tối ưu hóa kiến trúc bởi các tập đoàn bán dẫn như ARM, dung lượng pin vật lý vẫn bị giới hạn nghiêm ngặt bởi kích thước nhỏ gọn của thiết bị. Trong bối cảnh nền tảng Android chiếm hơn 71% thị phần toàn cầu (tính đến tháng 3 năm 2021), phần mềm đóng vai trò quyết định và điều khiển trực tiếp mọi hoạt động phần cứng. Luận án tiến sĩ kỹ thuật phần mềm mang tên "Một số phương pháp tối ưu năng lượng tiêu thụ cho các thiết bị di động dựa trên phân tích mã nguồn" do Nghiên cứu sinh Bùi Anh Tú thực hiện dưới sự hướng dẫn khoa học của PGS. Trương Ninh Thuận tại Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội (2024) đã tạo ra bước tiến tiên phong trong lĩnh vực Kỹ thuật Phần mềm Xanh (Green Software Engineering). Luận án tiếp cận một cách toàn diện vấn đề năng lượng phần mềm thông qua kỹ thuật phân tích chương trình tĩnh, thiết lập một cầu nối toán học chuẩn xác giữa các câu lệnh điều khiển trong mã nguồn và trạng thái tiêu hao năng lượng vật lý của thiết bị.

Thực tiễn nghiên cứu quốc tế tồn tại một research gap mang tính then chốt: các mô hình năng lượng hiện hữu chưa biểu diễn được sự ảnh hưởng toàn diện, có cấu trúc ngữ nghĩa và tương tác hệ thống của mã nguồn tới mức tiêu thụ năng lượng của thiết bị di động. Cụ thể, các công trình ước lượng dòng lệnh độc lập của Li và cộng sự [66, 113] phân tích tiêu thụ năng lượng trên từng câu lệnh đơn lẻ nhưng thiếu sự liên kết ngữ nghĩa giữa các khối lệnh, dẫn tới sai lệch nghiêm trọng khi xuất hiện lỗi ngữ nghĩa hoặc câu lệnh xung đột. Mô hình trạng thái của Shin Nakajima và cộng sự [88] mô hình hóa được trạng thái phần cứng nhưng thiếu khả năng biểu diễn trạng thái năng lượng tổng thể của toàn thiết bị. Mặt khác, các nghiên cứu đo kiểm vật lý của Carroll và Heiser [26] hay Nichanametla [89] đưa ra công thức tiêu thụ cho phần cứng thông qua thiết bị đo chuyên dụng nhưng hoàn toàn tách rời khỏi sự tác động điều khiển của luồng mã nguồn. Luận án giải quyết triệt để khoảng trống này bằng cách đặt ra ba câu hỏi nghiên cứu cốt lõi:

  • RQ1: Làm thế nào để xây dựng một mô hình hình thức biểu diễn chính xác mối quan hệ nhân quả giữa mã nguồn phần mềm và trạng thái năng lượng của toàn bộ thiết bị di động mà không cần thực thi trực tiếp trên phần cứng?
  • RQ2: Làm thế nào để tối ưu hóa bộ kiểm thử tính chất năng lượng nhằm giảm thiểu chi phí thực thi kiểm thử nhưng vẫn bảo toàn tối đa năng lực phát hiện lỗi năng lượng (energy bugs/hotspots)?
  • RQ3: Làm thế nào để điều phối giảm tải tác vụ (computation offloading) trong môi trường Điện toán Đám mây Di động (Mobile Cloud Computing - MCC) dựa trên phân tích mã nguồn tĩnh nhằm tối ưu đồng thời thời gian thực thi và mức tiêu hao năng lượng?

Tương ứng với ba câu hỏi nghiên cứu, các giả thuyết khoa học được kiểm chứng bao gồm:

  • H1: Mô hình ôtômát năng lượng tích hợp trọng số thời gian và hệ số tiêu hao năng lượng có khả năng ước lượng mức tiêu thụ năng lượng của các ca sử dụng (Use-Case - UC) với sai số nhỏ chấp nhận được so với đo lường vật lý thực nghiệm.
  • H2: Đồ thị luồng điều khiển cải tiến bổ sung trọng số năng lượng ($CFG_{ew}$) kết hợp giải thuật lựa chọn tham lam (Greedy) cho phép cắt giảm vượt bậc kích thước bộ kiểm thử ban đầu trong khi duy trì hệ số bao phủ các nút tiêu hao năng lượng lớn tương đương 100%.
  • H3: Thuật toán ra quyết định giảm tải dựa trên giải thuật di truyền (Genetic Algorithm) tối ưu hóa hàm mục tiêu đa tiêu chí Pareto ($F(\alpha, \beta)$) mang lại hiệu quả tiết kiệm năng lượng và thời gian thực thi vượt trội so với các phương pháp giảm tải ngẫu nhiên hoặc thực thi cục bộ.

Khung lý thuyết của luận án được xây dựng dựa trên sự hợp nhất chặt chẽ giữa Lý thuyết Ôtômát hữu hạn đơn định (Deterministic Finite Automata - DFA) của Hopcroft, Motwani và Ullman [55], Lý thuyết Phân tích chương trình tĩnh và Đồ thị luồng điều khiển (Control Flow Graph - CFG) khởi xướng bởi Frances E. Allen [16], và Lý thuyết Tối ưu hóa đa mục tiêu trong Điện toán Đám mây Di động. Nghiên cứu xác lập phạm vi trên hệ sinh thái Android mã nguồn Java, khảo sát 6 thành phần phần cứng cốt lõi gồm Audio, GPS, 3G/Cellular, Wi-Fi, LCD và CPU, đóng góp công cụ thực nghiệm PCE (Power Consumption Estimator) tích hợp dạng plug-in vào IDE chuẩn công nghiệp (Android Studio, IntelliJ).

Literature Review và Positioning

Tổng quan y văn quốc tế về năng lượng phần mềm di động được phân định thành ba dòng chảy học thuật chính:

  1. Dòng nghiên cứu mô hình hóa và ước lượng năng lượng phần mềm: Khởi đầu từ các nghiên cứu đo lường xung phần cứng như Carroll và Heiser [26] với phân tích chi tiết mức tiêu thụ của smartphone qua các đường ray điện áp, Pathak và cộng sự [93, 94] với công cụ eprof theo dõi lời gọi hệ thống (system calls), Li và cộng sự [66] tính toán năng lượng ở mức dòng lệnh (line-level energy estimation), và Hoque cùng cộng sự [46, 47] tổng quan toàn diện các kỹ thuật profiling.
  2. Dòng nghiên cứu kiểm thử và phát hiện lỗi năng lượng: Điển hình là các công trình phát hiện điểm nóng năng lượng của Banerjee và cộng sự [20], tối ưu bộ kiểm thử hướng năng lượng của Ding Li và cộng sự [61, 63], khung kiểm thử đột biến năng lượng μDroid và tạo oracle năng lượng tự động của Jabbarvand cùng cộng sự [50, 51, 52, 53], phân tích lỗi sleep conflicts Hypnos của Yoon et al. [54], và kỹ thuật ưu tiên hóa ca kiểm thử của Sagheer [96].
  3. Dòng nghiên cứu giảm tải tính toán trong MCC và MEC (Mobile Edge Computing): Bao gồm nghiên cứu cân bằng QoS và năng lượng của Li et al. [59], kiến trúc Mildip của Lu et al. [74], tối ưu hóa theo độ trễ và năng lượng của Lin et al. [68], Masoudi et al. [81, 82], và lập lịch đa tác vụ có ràng buộc thời gian của Wang et al. [106].
+-----------------------------------------------------------------------------------------+
|                                    Y VĂN HIỆN HỮU                                       |
|  - Đo kiểm vật lý (Carroll [26]): Chính xác cao nhưng phụ thuộc phần cứng cố định.      |
|  - Ước lượng dòng lệnh (Li [66]): Rời rạc, thiếu liên kết ngữ nghĩa điều khiển.         |
|  - Mô hình phần cứng (Nakajima [88]): Chưa mô hình hóa được trạng thái toàn hệ thống.   |
+--------------------------------------------+--------------------------------------------+
                                             |
                                     (Research Gap)
                                             |
                                             v
+-----------------------------------------------------------------------------------------+
|                                  ĐÓNG GÓP CỦA LUẬN ÁN                                    |
|  - Mô hình Ôtômát năng lượng hợp nhất (DFA): Ánh xạ ngữ nghĩa mã nguồn -> Phần cứng     |
|  - Đồ thị luồng điều khiển gán trọng số năng lượng (CFGew) & Hệ số phủ EPC              |
|  - Tối ưu giảm tải đa mục tiêu (Genetic Algorithm) cho toàn bộ tập tác vụ (Tasks)       |
+-----------------------------------------------------------------------------------------+

Y văn tồn tại hai cuộc tranh luận học thuật sâu sắc. Tranh luận thứ nhất xoay quanh phương pháp xác định năng lượng: Phương pháp đo lường vật lý trực tiếp (Hardware Profiling) khẳng định tính trung thực cao tiệm cận thực tế nhưng bị phê phán vì chi phí thiết bị đắt đỏ, không thể mở rộng và chỉ áp dụng được trên một cấu hình phần cứng cụ thể; ngược lại, phương pháp ước lượng tĩnh dựa trên mô hình (Model-based Static Estimation) cho phép đánh giá sớm trong chu trình phát triển (DevOps) mà không cần biên dịch hay chạy thiết bị, song bị hoài nghi về độ chính xác do bỏ qua các yếu tố nhiễu của môi trường thực thi. Tranh luận thứ hai diễn ra trong bài toán kiểm thử phần mềm: Các tiếp cận truyền thống ưu tiên độ bao phủ cấu trúc cổ điển (bao phủ câu lệnh, bao phủ nhánh/cạnh) dựa trên lý thuyết của Frances Allen [16], trong khi trường phái Kiểm thử Xanh (Green Testing) chỉ ra rằng các ca kiểm thử đạt 100% độ phủ nhánh vẫn có thể bỏ sót các chu trình kích hoạt ngoại vi (như giữ GPS hoặc Wi-Fi vô hạn) gây cạn kiệt pin nghiêm trọng.

Luận án định vị chính xác điểm nghẽn này và tạo ra bước đột phá vượt bậc khi so sánh trực tiếp với hai công trình quốc tế tiêu biểu:

  • So sánh với Li, Hao, Halfond và Govindan [66] (ISSTA 2013): Nghiên cứu của Li et al. tính toán năng lượng dòng lệnh bằng cách gán chi phí cố định cho bytecode mà không xem xét trạng thái tích lũy của phần cứng. Luận án của NCS. Bùi Anh Tú vượt trội hơn nhờ đề xuất cơ chế Ôtômát năng lượng hợp nhất từ các ôtômát thành phần, theo dõi chính xác sự chuyển dịch trạng thái phần cứng qua bộ đếm thời gian và hệ số tiêu thụ trạng thái ($k_i$).
  • So sánh với Reyhaneh Jabbarvand và cộng sự [53] (ISSTA 2016) & Sagheer [96] (2021): Các tác giả này tập trung vào thu nhỏ bộ kiểm thử dựa trên năng lượng tiêu thụ ước tính của phương thức, nhưng quy trình còn phụ thuộc nhiều vào dynamic execution traces. Luận án giải quyết bài toán hoàn toàn ở mức phân tích tĩnh mã nguồn thông qua cải tiến đồ thị $CFG_{ew}$ và xác lập hệ số ngưỡng $\epsilon$, giúp phát hiện chính xác các đường đi chứa câu lệnh tiêu hao năng lượng cực đại trước khi phần mềm được đóng gói và phát hành.

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

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

Luận án mở rộng Lý thuyết Ôtômát hữu hạn đơn định (DFA) của Hopcroft et al. [55] vào miền quản lý tài nguyên phi chức năng (Non-functional Resource Management) trong Kỹ thuật Phần mềm. Bằng cách định nghĩa hình thức bộ 5 thành phần của Ôtômát năng lượng phần cứng $M_h = (Q_h, \Sigma_h, \delta_h, q_{0h}, F_h)$ và Ôtômát năng lượng hợp nhất của toàn thiết bị $M_{dev} = \bigotimes M_h$, luận án chứng minh rằng trạng thái năng lượng tổng thể của một thiết bị di động tại thời điểm bất kỳ là tích Descartes của các trạng thái năng lượng thành phần của các mô-đun phần cứng: $$Q_{dev} = Q_{Audio} \times Q_{GPS} \times Q_{3G} \times Q_{Wifi} \times Q_{LCD} \times Q_{CPU}$$

Hơn thế nữa, luận án thách thức và mở rộng Lý thuyết Đồ thị luồng điều khiển truyền thống của Frances E. Allen [16] bằng việc thiết lập mô hình Đồ thị luồng điều khiển có trọng số năng lượng ($CFG_{ew} = (V, E, W_e)$). Trong đó, mỗi nút $v \in V$ không chỉ đại diện cho một khối lệnh cơ bản (basic block) mà còn được gán một hàm trọng số năng lượng $W_e(v)$ phản ánh mức công suất tiêu thụ của phần cứng bị kích hoạt bởi các câu lệnh điều khiển nằm trong nút đó.

+------------------------------------------------------------------------------------------+
|                             MÔ HÌNH HỢP NHẤT ÔTÔMÁT NĂNG LƯỢNG                           |
+------------------------------------------------------------------------------------------+
|  [Mã nguồn Java/Android] ---> (AST / JavaParser) ---> [Trích xuất Lời gọi API Ngoại vi]  |
|                                                                 |                        |
|                                                                 v                        |
|  +--------------------+   +--------------------+   +----------------------------------+  |
|  |  Ôtômát Audio (Ma)  |   |   Ôtômát GPS (Mg)  |   |  Ôtômát Mạng (Mw: Wifi/3G/4G)    |  |
|  +---------+----------+   +---------+----------+   +-----------------+----------------+  |
|            |                        |                                |                   |
|            +------------------------+--------------------------------+                   |
|                                     | (Tích Descartes Ôtômát)                            |
|                                     v                                                    |
|                   +------------------------------------+                                 |
|                   | Ôtômát Năng lượng Thiết bị (Mdev)   |                                 |
|                   |  Qdev = Qa x Qg x Mw x Mlcd x Mcpu |                                 |
|                   +-----------------+------------------+                                 |
|                                     |                                                    |
|                                     v                                                    |
|           [Gán Hệ số Tiêu thụ ki & Bộ đếm Thời gian Delta_t]                             |
|                                     |                                                    |
|                                     v                                                    |
|          [Công thức Ước lượng Năng lượng Ca sử dụng E(UC)]                               |
+------------------------------------------------------------------------------------------+

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

Khung phân tích của luận án tích hợp ba lý thuyết nền tảng: Lý thuyết Ôtômát hình thức, Phân tích luồng dữ liệu/dòng điều khiển tĩnh, và Quy hoạch tối ưu hóa đa mục tiêu (Multi-objective Evolutionary Optimization). Bốn đóng góp khái niệm mang tính đột phá bao gồm:

  1. Ôtômát năng lượng thành phần và hợp nhất ($M_h, M_{dev}$): Công cụ toán học ánh xạ chính xác lời gọi API từ framework Android (như MediaPlayer.start(), LocationManager.requestLocationUpdates(), WifiManager.setWifiEnabled()) thành các biến đổi trạng thái công suất năng lượng rời rạc.
  2. Đồ thị $CFG_{ew}$ và Khái niệm Nút tiêu thụ năng lượng đủ lớn: Định nghĩa tập các đỉnh $V_{heavy} = {v \in V \mid W_e(v) \ge \epsilon}$, trong đó $\epsilon$ là ngưỡng tiêu thụ năng lượng quy định bởi kỹ sư kiểm thử nhằm khoanh vùng các điểm nóng gây hao pin.
  3. Hệ số phủ năng lượng ca kiểm thử ($EPC$ - Energy Path Coefficient): Thước đo định lượng chất lượng của một ca kiểm thử $TC$ dựa trên mật độ và độ lớn của các trọng số năng lượng mà đường thực thi $path(TC)$ duyệt qua trên đồ thị $CFG_{ew}$: $$EPC(TC) = \frac{\sum_{v \in path(TC)} W_e(v)}{\sum_{u \in V} W_e(u)}$$
  4. Hàm mục tiêu Pareto giảm tải hai tiêu chí ($F(\alpha, \beta)$): Hàm toán học đánh giá tổng tỷ suất lợi nhuận khi chuyển giao tập tác vụ $Tasks$ lên đám mây, tích hợp hệ số ưu tiên về thời gian ($\alpha$) và năng lượng ($\beta$) với điều kiện chuẩn hóa $\alpha + \beta = 1$: $$F(X) = \alpha \cdot \frac{T_{local} - T_{offload}(X)}{T_{local}} + \beta \cdot \frac{E_{local} - E_{offload}(X)}{E_{local}}$$ Điều kiện biên (Boundary conditions): Phương pháp áp dụng cho các ứng dụng Android viết bằng Java, thực thi trên kiến trúc đa luồng với các khối tác vụ có thể phân rã độc lập và kết nối mạng không dây xác định.

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

Thiết kế nghiên cứu

Luận án tuân thủ triệt để thế giới quan khoa học thực chứng (Positivism) kết hợp phương pháp luận Khoa học Thiết kế (Design Science Research) đặc trưng của ngành Kỹ thuật Phần mềm. Nghiên cứu sử dụng thiết kế hỗn hợp (Mixed-methods Design) kết hợp giữa chứng minh hình thức toán học (Formal Methods), phân tích mã nguồn tĩnh trên Cây cú pháp trừu tượng (AST), và đo kiểm thực nghiệm vật lý đối chứng.

Thiết kế đa cấp độ (Multi-level design) được triển khai qua 4 tầng phân tích:

  • Cấp độ 1 (Statement-level): Phân tích cú pháp trừu tượng AST nhằm phát hiện các câu lệnh điều khiển ngoại vi bằng thư viện JavaParser.
  • Cấp độ 2 (Method/CFG-level): Xây dựng đồ thị luồng điều khiển và gán nhãn trọng số năng lượng cho từng khối lệnh bằng CFGBuilder.
  • Cấp độ 3 (Use-Case/App-level): Mô hình hóa kịch bản người dùng thành các chuỗi chuyển trạng thái ôtômát để ước lượng năng lượng tiêu thụ toàn cục.
  • Cấp độ 4 (System/Cloud-level): Thiết kế mô hình điều phối phân tán giữa thiết bị di động và máy chủ đám mây trong mô hình MCC.
+------------------------------------------------------------------------------------+
|                         QUY TRÌNH PHÂN TÍCH VÀ ĐO KIỂM                             |
+------------------------------------------------------------------------------------+
|                                                                                    |
|  [Mã nguồn Ứng dụng]                                                              |
|          |                                                                         |
|          +---> (JavaParser AST) ---> [Sinh Ôtômát Năng lượng Ứng dụng]             |
|          |                                          |                              |
|          |                                          v                              |
|          |                            [Công cụ Ước lượng Tĩnh PCE]                 |
|          |                                          | (Dữ liệu ước lượng Epce)     |
|          |                                          v                              |
|          +---> [Thực thi trên Thiết bị] ---> [Đo Vật lý: KWS-MX18 & AccuBattery]   |
|                                                     | (Dữ liệu thực tế Ereal)      |
|                                                     v                              |
|                                        [Kiểm định Đối chứng & Sai số]              |
|                                        Delta_E = |Epce - Ereal| / Ereal            |
|                                                                                    |
+------------------------------------------------------------------------------------+

Quy trình nghiên cứu rigorous

Quy trình thu thập và xử lý dữ liệu được thiết kế chặt chẽ qua các giai đoạn:

  • Trích xuất đặc trưng tĩnh: Sử dụng thư viện JavaParser để duyệt AST của các ứng dụng mã nguồn mở phổ biến (như OpenCamera [34, 35], Osmdroid [91]). Xác định các giao diện lập trình API của Android Framework quản lý năng lượng: android.media.MediaPlayer [7], android.location.LocationManager [6], android.net.wifi.WifiManager [9], android.net.ConnectivityManager [1].
  • Mô hình hóa đồ thị: Sử dụng công cụ CFGBuilder để chuyển đổi mã nguồn thành đồ thị luồng điều khiển cơ sở, sau đó chạy thuật toán gán trọng số năng lượng để xây dựng đồ thị $CFG_{ew}$.
  • Giao thức đo lường thực nghiệm đối chứng (Triangulation): Để kiểm chứng độ chính xác của công cụ ước lượng PCE, luận án thiết lập tam giác đo lường đa phương pháp:
    1. Đo lường mức vật lý: Sử dụng thiết bị đo dòng và điện áp chuyên dụng Keweisi KWS-MX18 USB Tester [5] nối tiếp giữa nguồn cung cấp và thiết bị di động để lấy mẫu điện năng tiêu thụ tiêu chuẩn theo thời gian thực.
    2. Đo lường mức hệ điều hành: Sử dụng công cụ giám sát pin AccuBattery [10] theo dõi dòng xả (discharge current tính bằng mA/mAh) trực tiếp từ kernel Android.
    3. Mô phỏng tự động hóa: Sử dụng công cụ AutoClick [19] và Randoop [36] để tái lập chính xác các ca sử dụng UC nhằm loại bỏ sai số do thao tác thủ công của con người.

Độ tin cậy và tính giá trị (Construct, Internal, External Validity) được bảo đảm thông qua việc kiểm tra tính đơn định của các ôtômát sinh ra, chứng minh tính dừng của các thuật toán tối ưu, và thực nghiệm lặp lại nhiều lần trên các kịch bản phần mềm thực tế.

Data và phân tích

Dữ liệu phân tích bao gồm hàng nghìn dòng lệnh mã nguồn từ các dự án mã nguồn mở Android, đồ thị luồng điều khiển chứa hàng trăm đỉnh và cạnh, cùng các vết thực thi tác vụ tính toán phức tạp. Các kỹ thuật tính toán tiên tiến bao gồm:

  • Thuật toán sinh và rút gọn Ôtômát năng lượng (Algorithms 3.1 & 3.2): Tự động loại bỏ các trạng thái không thể đạt tới (unreachable states) và hợp nhất các trạng thái tương đương dựa trên ngôn ngữ chấp nhận của DFA.
  • Thuật toán tối ưu hóa bộ kiểm thử (Algorithms 4.1 - 4.5): Sử dụng chiến lược tham lam (Greedy approach) để tìm tập con các ca kiểm thử $T_{opt} \subset T_{orig}$ sao cho $|T_{opt}| \ll |T_{orig}|$ nhưng đảm bảo bao phủ 100% tập đỉnh $V_{heavy}$.
  • Thuật toán Di truyền (Genetic Algorithm) trong MCC (Algorithm 5.1): Khởi tạo quần thể nhiễm sắc thể nhị phân biểu diễn phân bố thực thi của tập $n$ tác vụ ($x_i \in {0, 1}$ tương ứng thực thi cục bộ hay chuyển giao lên đám mây), trải qua các toán tử chọn lọc bánh xe roulette, lai ghép đơn điểm và đột biến nhằm tối đa hóa hàm thích nghi Pareto $F(\alpha, \beta)$ dưới các ràng buộc thời gian nghiêm ngặt ($T_{total} \le T_{deadline}$).

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

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

Luận án công bố bốn phát hiện thực nghiệm mang tính đột phá với bằng chứng số liệu rõ ràng:

Trích dẫn phát hiện 1 (Tính chính xác của phương pháp ước lượng tĩnh PCE): "Nghiên cứu ảnh hưởng của phần mềm đối với sự tiêu thụ năng lượng trên các thiết bị di động được coi là hướng tiếp cận hiệu quả để cải thiện hiệu năng, đồng thời giảm thiểu sự tiêu thụ năng lượng trên các thiết bị di động... Công cụ ước lượng đã chứng minh tính đúng đắn và tính hiệu quả của phương pháp với kết quả ước lượng có độ sai số nhỏ so với số liệu đo lường bằng thiết bị chuyên dụng." Bằng chứng thực nghiệm đối chứng giữa công cụ PCE và thiết bị đo Keweisi KWS-MX18 cho thấy công cụ ước lượng dựa trên ôtômát năng lượng phản ánh chính xác xu hướng tiêu hao điện năng của các Use-Case phức tạp mà không phát sinh độ trễ hay chi phí thực thi phần cứng.

Trích dẫn phát hiện 2 (Hiệu quả tối ưu năng lượng cực đại trong mô hình MCC): "Trong trường hợp $\beta = 1$ và $\alpha = 0$, việc giảm tải theo phương pháp đã đề xuất đã tiết kiệm được 24,1% năng lượng so với phương pháp giảm tải ngẫu nhiên là 15,1%." Kết quả này chỉ ra rằng việc lựa chọn thông minh các tác vụ dựa trên phân tích chi phí mã nguồn tĩnh mang lại mức tiết kiệm điện năng cao hơn 9% tuyệt đối (tương đương cải thiện hơn 59.6% hiệu suất giảm tải) so với các giải pháp heuristics ngẫu nhiên.

Trích dẫn phát hiện 3 (Cân bằng tối ưu đa mục tiêu thời gian - năng lượng): "Trường hợp cân bằng nhất khi $\alpha = 0.6$, thiết bị di động sẽ tiết kiệm được 21% thời gian thực thi và 18% chi phí năng lượng." Phát hiện này chứng minh sự tồn tại của điểm tối ưu Pareto thực tế trong điều phối tác vụ di động, đập tan định kiến cho rằng việc giảm tải lên đám mây luôn gây hao tổn năng lượng truyền thông mạng lớn hơn lợi ích xử lý.

+-----------------------------------------------------------------------------------------+
|                  SO SÁNH HIỆU QUẢ GIẢM TẢI TRONG MÔ HÌNH MCC                            |
+----------------------------------------------------+------------------------------------+
|  Kịch bản Giảm tải / Thông số Tối ưu               |  Tỷ lệ Tiết kiệm Thực nghiệm       |
+----------------------------------------------------+------------------------------------+
|  - Ưu tiên Năng lượng Tuyệt đối (\beta=1, \alpha=0)|  Tiết kiệm 24.1% Năng lượng        |
|  - Giảm tải Ngẫu nhiên 50% Tác vụ                  |  Tiết kiệm 15.1% Năng lượng        |
|  - Cân bằng Đa mục tiêu (\alpha=0.6, \beta=0.4)    |  Tiết kiệm 21% Thời gian & 18% NL  |
+----------------------------------------------------+------------------------------------+
  • Phát hiện then chốt 4 (Thu nhỏ đột phá kích thước bộ kiểm thử năng lượng): Thực nghiệm trên các module mã nguồn có mật độ tiêu thụ năng lượng cao chứng minh rằng: Bằng cách sử dụng đồ thị $CFG_{ew}$ và hệ số $EPC$, thuật toán tối ưu đã loại bỏ tới hơn 60% các ca kiểm thử trùng lặp hoặc không đi qua các nút kích hoạt phần cứng $V_{heavy}$, trong khi vẫn bảo toàn nguyên vẹn 100% năng lực phát hiện các lỗi rò rỉ năng lượng và giữ vững độ bao phủ cấu trúc trọng yếu.

Implications đa chiều

  • Về mặt Lý thuyết (Theoretical Advances): Đặt nền móng lý thuyết vững chắc cho ngành Kỹ thuật Phần mềm Xanh, chứng minh rằng các thuộc tính phi chức năng như năng lượng hoàn toàn có thể được hình thức hóa, phân tích cú pháp và kiểm chứng tĩnh tương tự như các thuộc tính chức năng cổ điển. Mở rộng biên giới của Lý thuyết Ôtômát và Lý thuyết Đồ thị luồng điều khiển trong phân tích hệ thống nhúng/di động.
  • Về mặt Phương pháp luận (Methodological Innovations): Cung cấp một framework phương pháp luận mẫu mực về kiểm thử cấu trúc định hướng năng lượng ($CFG_{ew}$ và $EPC$) có khả năng tái sử dụng và chuyển giao trực tiếp cho các hệ điều hành di động và nhúng khác (như iOS, HarmonyOS, FreeRTOS, Linux Embedded).
  • Về mặt Ứng dụng Thực tiễn (Practical Applications): Giúp các doanh nghiệp công nghệ và lập trình viên cắt giảm triệt để thời gian và chi phí kiểm thử phần mềm di động. Bộ công cụ PCE tích hợp dưới dạng plug-in cho phép lập trình viên nhận biết các "điểm nóng tiêu hao năng lượng" ngay trong quá trình gõ mã nguồn (tương tự như linter kiểm tra lỗi cú pháp), ngăn chặn từ sớm các lỗ hổng hao pin trước khi phát hành ứng dụng ra thị trường.
  • Về mặt Chính sách và Tiêu chuẩn Công nghệ (Policy & Standards): Đóng góp cơ sở khoa học định lượng để các cơ quan quản lý tiêu chuẩn phần mềm ban hành các chỉ số đánh giá và chứng nhận "Phần mềm Xanh / Nhãn năng lượng Ứng dụng di động", góp phần giảm phát thải carbon gián tiếp từ hạ tầng thiết bị thông minh toàn cầu.

Limitations và Future Research

Nhằm duy trì tính khách quan khoa học và sự khiêm tốn học thuật, luận án chỉ rõ bốn giới hạn (limitations) cốt lõi:

  1. Phạm vi phần cứng khảo sát: Mô hình ôtômát năng lượng hiện tại mới tích hợp 6 mô-đun phần cứng cơ bản (Audio, GPS, 3G/Cellular, Wi-Fi, LCD, CPU). Các thành phần phần cứng thế hệ mới như Camera độ phân giải cao, chip xử lý trí tuệ nhân tạo (NPU/TPU), cảm biến sinh trắc học, Bluetooth năng lượng thấp (BLE) và modem 5G NR chưa được tích hợp đầy đủ.
  2. Bộ ký hiệu đầu vào của Ôtômát: Tập ký hiệu đầu vào $\Sigma$ được xây dựng dựa trên việc trích xuất các API phổ biến của Android SDK. Do các thư viện bên thứ ba và SDK nền tảng liên tục cập nhật, tập ký hiệu này cần liên tục được cập nhật thủ công để tránh hiện tượng bỏ sót lệnh điều khiển.
  3. Ràng buộc phụ thuộc tác vụ trong MCC: Mô hình giảm tải tác vụ hiện thời giả định các tác vụ trong tập $Tasks$ là độc lập. Trong các ứng dụng phức tạp, các tác vụ thường có quan hệ phụ thuộc dữ liệu tuần tự hoặc lồng nhau (biểu diễn dưới dạng đồ thị có hướng không chu trình - DAG), đòi hỏi cơ chế đồng bộ hóa thời gian phức tạp hơn.
  4. Thiết lập trọng số thủ công: Hệ số ngưỡng năng lượng $\epsilon$ trong kiểm thử cũng như các trọng số ưu tiên $\alpha$ (thời gian) và $\beta$ (năng lượng) trong giảm tải hiện vẫn do lập trình viên thiết lập thủ công dựa trên kinh nghiệm chủ quan, chưa phản ánh tự động theo ngữ cảnh người dùng thời gian thực.

Từ những hạn chế trên, chương trình nghị sự nghiên cứu tương lai (Future Research Agenda) mở ra 4 hướng đột phá:

  • Tự động hóa học hệ số thông minh qua Machine Learning: Nghiên cứu ứng dụng Học máy và Học tăng cường (Reinforcement Learning) để tự động hóa việc nhận diện và tối ưu các tham số $\epsilon, \alpha, \beta$ dựa trên thói quen người dùng và mức pin thực tế của thiết bị.
  • Mở rộng mô hình năng lượng đa ứng dụng và hệ điều hành: Xây dựng khung ước lượng năng lượng đồng thời cho môi trường đa tiến trình (multi-tenant/background apps) có tính tới sự can thiệp của bộ điều phối hệ điều hành Android (Doze Mode, App Standby).
  • Mở rộng mô hình giảm tải cho đồ thị phụ thuộc DAG: Nâng cấp giải thuật di truyền và quy hoạch động để tối ưu hóa việc phân tán các luồng tác vụ có ràng buộc phụ thuộc dữ liệu phức tạp trong mô hình Tính toán Biên di động (Mobile Edge Computing - MEC) và mạng 6G.
  • Tự động hóa hoàn toàn quy trình Tái cấu trúc mã nguồn Xanh (Automated Green Refactoring): Phát triển công cụ tự động đề xuất và tự động sửa đổi mã nguồn (Automated Code Repair) khi phát hiện các mẫu lệnh gây rò rỉ năng lượng.

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

  • Tác động Học thuật (Academic Impact): Đóng góp trực tiếp vào kho tàng tri thức thế giới với 04 công trình khoa học chất lượng cao, bao gồm các bài báo xuất bản trên các tạp chí quốc tế uy tín (như Mobile Networks and Applications - Springer, International Journal of Future Computer and Communication - IJFCC) và kỷ yếu hội thảo quốc tế chuyên ngành (Springer LNICST, IEEE NICS/NAFOSTED). Các công trình này mở ra hướng trích dẫn tiềm năng cho các nghiên cứu tiếp theo về Phân tích chương trình tĩnh hướng năng lượng và Kiểm chứng hình thức phần mềm di động.
  • Chuyển đổi Ngành Công nghiệp Phần mềm (Industry Transformation): Thay đổi tư duy phát triển phần mềm di động từ việc chỉ tập trung vào chức năng (Functionality) và hiệu năng thời gian (Performance) sang tích hợp chỉ số bền vững năng lượng (Energy Sustainability) xuyên suốt vòng đời phát triển phần mềm (SDLC).
  • Lợi ích Xã hội và Môi trường (Societal & Environmental Benefits): Kéo dài tuổi thọ sử dụng pin vật lý của hàng tỷ thiết bị di động, giảm tần suất sạc điện hàng ngày của người dùng, qua đó giảm tiêu thụ điện năng từ lưới điện và giảm thiểu lượng rác thải điện tử (E-waste) từ pin lithium bị chai hỏng ra môi trường tự nhiên.

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

+------------------------------------------------------------------------------------+
|                                ĐỐI TƯỢNG HƯỞNG LỢI                                 |
+------------------------------------------------------------------------------------+
|                                                                                    |
|  [Nghiên cứu sinh & Nhà khoa học] ---> Khung lý thuyết Ôtômát Năng lượng & CFGew    |
|                                                                                    |
|  [Kỹ sư R&D & Lập trình viên]     ---> Công cụ Plug-in PCE & Phát hiện Điểm nóng   |
|                                                                                    |
|  [Chuyên gia QA & Tester]         ---> Thuật toán Tối ưu Bộ kiểm thử (EPC & Greedy)|
|                                                                                    |
|  [Kiến trúc sư Hệ thống Cloud]    ---> Giải thuật Di truyền Giảm tải Pareto MCC    |
|                                                                                    |
|  [Người dùng & Xã hội]            ---> Tiết kiệm 18-24.1% Pin, Kéo dài Tuổi thọ TB |
|                                                                                    |
+------------------------------------------------------------------------------------+
  • Nghiên cứu sinh và Giới học thuật: Tiếp cận một khung lý thuyết hình thức hoàn chỉnh, kế thừa các thuật toán hợp nhất ôtômát và cải tiến đồ thị luồng điều khiển để mở rộng cho các bài toán phân tích tài nguyên phi chức năng khác như bộ nhớ (RAM), băng thông mạng và bảo mật luồng thông tin.
  • Kỹ sư R&D và Lập trình viên Ứng dụng Di động: Sở hữu công cụ PCE cài cắm trực tiếp trên Android Studio/IntelliJ, cho phép trực quan hóa mức tiêu hao năng lượng của từng dòng lệnh và từng Use-Case ngay trong quá trình code, loại bỏ nhu cầu trang bị các dàn máy đo vật lý cồng kềnh và đắt tiền.
  • Đội ngũ Kiểm thử Chất lượng Phần mềm (QA/QC Engineers): Cắt giảm hơn 60% thời gian chạy kiểm thử hồi quy (Regression Testing) đối với các thuộc tính năng lượng nhờ bộ kiểm thử tối ưu, nâng cao năng suất kiểm thử và độ tin cậy của sản phẩm.
  • Các Nhà hoạch định Chính sách và Quản lý Tiêu chuẩn Công nghệ: Nắm giữ cơ sở lý luận và công cụ đo kiểm khách quan để ban hành các khung đánh giá phần mềm thân thiện với môi trường, thúc đẩy nền kinh tế số phát triển bền vững.

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

1. Đóng góp lý thuyết độc đáo nhất của luận án là gì và đã mở rộng lý thuyết nền tảng nào?

Đóng góp lý thuyết độc đáo nhất là việc đề xuất mô hình Ôtômát Năng lượng Hợp nhất ($M_{dev}$) dựa trên việc mở rộng Lý thuyết Ôtômát hữu hạn đơn định (DFA) của Hopcroft, Motwani và Ullman [55]. Luận án đã hình thức hóa việc ánh xạ các câu lệnh điều khiển API trong mã nguồn thành các sự kiện chuyển trạng thái công suất rời rạc của 6 phần cứng cốt lõi, tích hợp trực tiếp bộ đếm thời gian thực thi ($\Delta t_i$) và hệ số tiêu thụ đặc trưng ($k_i$) vào từng trạng thái của ôtômát để giải bài toán ước lượng năng lượng toàn cục mà không cần thực thi chương trình.

2. Sự đổi mới trong phương pháp nghiên cứu của luận án khi so sánh với ít nhất 2 công trình quốc tế đi trước?

So với nghiên cứu của Ding Li và cộng sự [66] (chỉ ước lượng năng lượng ở mức dòng lệnh đơn lẻ, thiếu ngữ nghĩa liên kết) và công trình của Shin Nakajima [88] (chỉ mô hình hóa trạng thái năng lượng riêng rẽ cho từng phần cứng), luận án của NCS. Bùi Anh Tú đã đổi mới phương pháp luận khi:

  • Tự động sinh Ôtômát năng lượng tổng thể của thiết bị thông qua tích Descartes của các ôtômát phần cứng thành phần.
  • Cải tiến đồ thị luồng điều khiển thành đồ thị có trọng số năng lượng ($CFG_{ew}$) kết hợp hệ số bao phủ năng lượng $EPC$, cho phép tối ưu hóa bộ kiểm thử hoàn toàn bằng phân tích tĩnh trước khi đóng gói ứng dụng.

3. Phát hiện thực nghiệm gây bất ngờ nhất được hỗ trợ bởi dữ liệu là gì?

Phát hiện bất ngờ nhất nằm ở mối quan hệ đánh đổi phi tuyến tính trong bài toán giảm tải tác vụ (MCC): Khi thiết lập hệ số ưu tiên năng lượng tuyệt đối ($\beta = 1, \alpha = 0$), phương pháp đề xuất giúp thiết bị tiết kiệm tới 24,1% năng lượng so với mức 15,1% của phương pháp ngẫu nhiên. Đặc biệt, khi thiết lập mức cân bằng đa mục tiêu $\alpha = 0.6$ và $\beta = 0.4$, hệ thống đồng thời tiết kiệm được 21% thời gian thực thi và 18% chi phí năng lượng, chứng minh rằng việc phân tích mã nguồn tĩnh có thể xóa bỏ hoàn toàn sự xung đột giữa bài toán tối ưu tốc độ và bài toán bảo toàn năng lượng.

4. Luận án có cung cấp giao thức tái lặp nghiên cứu (Replication Protocol) không?

Luận án cung cấp giao thức thực nghiệm hoàn chỉnh và minh bạch:

  • Các thuật toán sinh ôtômát (Thuật toán 3.1, 3.2), tính toán trọng số $CFG_{ew}$ (Thuật toán 4.1, 4.2), chọn ca kiểm thử tham lam (Thuật toán 4.5) và giải thuật di truyền giảm tải (Thuật toán 5.1) đều được đặc tả chi tiết từng bước bằng mã giả toán học.
  • Định danh rõ ràng các công cụ phân tích tĩnh mã nguồn mở gồm JavaParser [4] và CFGBuilder [28], cùng các phần mềm kiểm chứng đối chứng như AccuBattery [10], Randoop [36] và thiết bị đo Keweisi KWS-MX18 [5].

5. Chương trình nghị sự nghiên cứu 10 năm tới được phác thảo như thế nào?

Chương trình nghị sự 10 năm tới tập trung vào:

  1. Tích hợp mô hình mạng nơ-ron học sâu (Deep Learning/LLMs) để tự động phát hiện mã nguồn "xấu xí" về năng lượng (Energy Code Smells) và tự động tái cấu trúc mã nguồn (Automated Refactoring).
  2. Xây dựng lý thuyết Ôtômát năng lượng mở rộng cho các kiến trúc tính toán biên phân tán (Edge-Fog-Cloud Computing) trên nền tảng mạng 5G/6G.
  3. Chuẩn hóa bộ công cụ phân tích năng lượng tĩnh PCE thành tiêu chuẩn quốc tế mở cho cộng đồng phát triển ứng dụng di động toàn cầu.

Kết luận

Luận án tiến sĩ của NCS. Bùi Anh Tú đã giải quyết xuất sắc bài toán tối ưu năng lượng tiêu thụ cho thiết bị di động từ góc độ kỹ thuật phần mềm thông qua các đóng góp cụ thể sau:

  1. Xây dựng mô hình Ôtômát năng lượng hình thức: Khắc phục triệt để các nhược điểm rời rạc của các mô hình y văn quốc tế, biểu diễn chính xác mối quan hệ tác động giữa mã nguồn và trạng thái năng lượng của toàn bộ phần cứng thiết bị.
  2. Phát triển phương pháp và công cụ ước lượng tĩnh PCE: Cho phép ước lượng mức tiêu thụ năng lượng theo từng ca sử dụng UC với độ chính xác cao, sai số nhỏ chấp nhận được so với đo kiểm vật lý chuyên dụng mà không cần biên dịch hay chạy chương trình trên thiết bị thực.
  3. Đề xuất kỹ thuật tối ưu hóa bộ kiểm thử năng lượng qua đồ thị $CFG_{ew}$: Đưa ra định nghĩa trọng số năng lượng, tập đỉnh tiêu thụ lớn $V_{heavy}$, hệ số phủ $EPC$ và giải thuật tham lam giúp cắt giảm vượt bậc số lượng ca kiểm thử trong khi duy trì 100% độ phủ các câu lệnh tiêu hao năng lượng cao.
  4. Thiết lập giải pháp giảm tải tác vụ đa mục tiêu trong mô hình MCC: Xây dựng hàm mục tiêu thích nghi Pareto $F(\alpha, \beta)$ và giải thuật di truyền giúp tiết kiệm tới 24.1% năng lượng (khi $\beta=1$) và đạt mức tối ưu cân bằng tiết kiệm 21% thời gian cùng 18% năng lượng (khi $\alpha=0.6$).
  5. Đóng góp công cụ thực tiễn cho ngành công nghiệp: Chuyển giao các thuật toán thành công cụ plug-in hỗ trợ trực tiếp các kỹ sư phần mềm trên Android Studio và IntelliJ.

Công trình tạo ra bước chuyển đổi hệ hình (Paradigm Advancement) mạnh mẽ từ "Đo kiểm năng lượng thực nghiệm thụ động" sang "Mô hình hóa và Kiểm chứng năng lượng tĩnh chủ động", mở ra 3 nhánh nghiên cứu học thuật then chốt: Kiểm thử phần mềm định hướng năng lượng, Tối ưu hóa phân tán đa mục tiêu trong điện toán đám mây di động, và Tái cấu trúc mã nguồn tự động vì môi trường bền vững. Với 04 công trình khoa học đã công bố và các kết quả định lượng chuẩn xác, luận án khẳng định vị thế học thuật vững chắc, đóng góp lâu dài và thiết thực cho sự phát triển của ngành Kỹ thuật Phần mềm Xanh trên phạm vi quốc tế.