Tổng quan về luận án

Sự bùng nổ của cuộc Cách mạng Công nghiệp lần thứ tư đã xác lập vị thế trung tâm của Internet vạn vật (Internet of Things - IoT), đặc biệt là phân nhánh Thiết bị đeo tay thông minh (Internet of Wearable Things - IoWT). Theo thống kê từ các tổ chức nghiên cứu thị trường quốc tế, có hơn 400 triệu thiết bị đeo tay được bán ra trên toàn cầu vào năm 2020 với tốc độ tăng trưởng ứng dụng IoT hàng năm vượt mức 10%, trong đó lĩnh vực sản xuất công nghiệp và giám sát y tế thông minh tăng trưởng đột phá trên 22%. Mặc dù các thiết bị IoWT đóng vai trò then chốt trong việc thu thập dữ liệu sinh trắc học thời gian thực, điều phối cứu nạn cứu hộ và kích hoạt các phản ứng khẩn cấp, quá trình phát triển phần mềm nhúng cho các thiết bị này đang đối mặt với nút thắt cổ chai nghiêm trọng về mặt kỹ nghệ.

Điểm nghẽn nghiên cứu (research gap) cốt lõi xuất phát từ sự thiếu vắng một khung thức kỹ nghệ phần mềm thống nhất có khả năng thu hẹp khoảng cách ngữ nghĩa giữa mô hình nghiệp vụ mức cao và phần cứng nhúng phân mảnh cấp thấp. Các công cụ tạo mã hiện nay hoặc chỉ tập trung vào tầng giao tiếp trung gian (middleware/cloud) mà bỏ quên ràng buộc phần cứng, hoặc chỉ tạo mã cấu hình tĩnh mà không thể tự động hóa logic điều khiển nghiệp vụ phức tạp.

Để giải quyết triệt để rào cản trên, luận án tiến sĩ chuyên ngành Khoa học Máy tính (Mã số: 62.01) của nghiên cứu sinh Tôn Long Phước, dưới sự hướng dẫn khoa học của TS. Lê Lam Sơn và TS. Phạm Hoàng Anh tại Trường Đại học Bách Khoa – Đại học Quốc gia TP. Hồ Chí Minh (2022), đã xây dựng một tiếp cận đột phá mang tính hệ thống. Luận án giải quyết 3 câu hỏi nghiên cứu tường minh:

  • [RQ1]: Cấu trúc của một khung thức tổng quát hỗ trợ xuyên suốt từ khâu đặc tả ứng dụng, thiết kế phần cứng, kiểm tra tính nhất quán ngữ nghĩa đến sinh mã nguồn thực thi cho thiết bị IoWT cần được thiết lập như thế nào?
  • [RQ2]: Làm thế nào để kết hợp mô hình hóa hướng miền với hệ thống tập luật nhằm đặc tả đồng thời kiến trúc phần cứng và hành vi ứng dụng, đảm bảo tính đúng đắn trước khi biên dịch?
  • [RQ3]: Công cụ tự động hóa được hiện thực hóa như thế nào để đạt tỷ lệ sinh mã tối ưu, và phương pháp thực nghiệm nào bảo đảm tính khách quan, tin cậy khi đánh giá chất lượng phần mềm trong môi trường công nghiệp và học thuật?

Dựa trên nền tảng lý thuyết Kỹ nghệ hướng mô hình (Model-Driven Engineering - MDE), Kiến trúc hướng mô hình (Model-Driven Architecture - MDA) của tổ chức OMG và Phương pháp hình thức nhẹ (Lightweight Formal Methods) bằng ngôn ngữ Alloy của Viện Công nghệ Massachusetts (MIT), tác giả đề xuất công cụ mang tên Micraspis. Kết quả thực nghiệm khẳng định Micraspis có khả năng tạo ra tự động hơn 65% mã nguồn C++ hoàn thiện cho các bo mạch phần cứng chuẩn Arduino trên 06 ca nghiên cứu điển hình (case-study) từ đơn giản đến phức tạp (như hệ thống cảnh báo sức khỏe iTempFoll, giải pháp nhà hàng thông minh iRestaurant). Khảo sát thực nghiệm diện rộng trên 161 lập trình viên và chuyên gia tại 18 doanh nghiệp công nghệ cùng 04 cơ sở giáo dục đại học/cao đẳng cho thấy trên 65% người tham gia đánh giá hài lòng và rất hài lòng về tính khả dụng và hiệu năng của giải pháp.

Literature Review và Positioning

Phát triển phần mềm nhúng cho các thiết bị biên IoT từ lâu đã là tâm điểm của kỹ nghệ phần mềm hiện đại. Tổng hợp các dòng nghiên cứu lớn cho thấy hai khuynh hướng chính: Ngôn ngữ chuyên biệt hóa miền hẹp (Domain-Specific Language - DSL) theo định nghĩa của Martin Fowler (2010) và Kỹ nghệ chuyển đổi mô hình (Model-Driven Development - MDD) theo chuẩn hóa của Schmidt (2006).

                      ┌──────────────────────────────────────────────┐
                      │    CÁC KHU VỰC NGHIÊN CỨU HIỆN HỮU           │
                      ├──────────────────────┬───────────────────────┤
                      │  Thiên về Phần cứng  │  Thiên về Tầng Web /  │
                      │   (Hardware-Centric) │  Middleware (Cloud)   │
                      │  ThingML, EL4IoT     │  Midgar, IoTSuite     │
                      └──────────┬───────────┴───────────┬───────────┘
                                 │                       │
                                 ▼                       ▼
                      ┌──────────────────────────────────────────────┐
                      │ KHOẢNG TRỐNG NGHIÊN CỨU (RESEARCH GAP)       │
                      │ Thiếu cơ chế tích hợp đồng thời giữa logic   │
                      │ máy trạng thái và ràng buộc phần cứng IoWT.  │
                      └──────────────────────┬───────────────────────┘
                                             │
                                             ▼
                      ┌──────────────────────────────────────────────┐
                      │ ĐÓNG GÓP CỦA LUẬN ÁN: CÔNG CỤ MICRASPIS      │
                      │ Tích hợp Metamodel kép + Hệ tập luật ràng    │
                      │ buộc + Kiểm chứng hình thức bằng Alloy       │
                      │ -> Sinh >= 65% mã C++ thực thi cho Arduino   │
                      └──────────────────────────────────────────────┘

Trong bức tranh tổng quan, các công trình quốc tế đã đạt được một số thành tựu nhưng vẫn bộc lộ nhiều tranh luận và mâu thuẫn học thuật sâu sắc:

  1. Tranh luận giữa tiếp cận Hướng phần cứng (Hardware-Centric) và Hướng dịch vụ (Service-Centric): Các công cụ như ThingML (Harrand et al., 2016) và EL4IoT tập trung mạnh vào trừu tượng hóa giao tiếp phần cứng trên hệ điều hành Contiki nhưng thiếu hoàn toàn khả năng mô hình hóa quy trình nghiệp vụ cấp cao của ứng dụng. Ngược lại, Midgar (García-Magariño et al., 2017) cho phép mô hình hóa các luồng dịch vụ thông qua giao diện Web nhưng mã nguồn sinh ra lại phụ thuộc hoàn toàn vào hạ tầng máy chủ, không hỗ trợ thiết kế kiến trúc phần cứng chi tiết của thiết bị đeo.
  2. Tranh luận về mức độ trừu tượng hóa và tính khả thi của mã nguồn: Asm2C++ (Gargantini et al., 2017) chuyển đổi lược đồ máy trạng thái trừu tượng (Abstract State Machine - ASM) sang C++ trên nền tảng Arduino nhưng lại gắn chặt logic với phần cứng đơn nhất, làm triệt tiêu khả năng tái sử dụng (reusability) khi phần cứng thay đổi. Trong khi đó, IoTSuite (Patel et al., 2015) và UML4IoT (Thramboulidis et al., 2015) sử dụng biểu đồ lớp UML để tạo ra các lớp vỏ bọc (IoTwrapper), song phần mã phát sinh chỉ dừng lại ở mức giao tiếp nguyên mẫu (prototype), đòi hỏi lập trình viên phải tự viết tay phần lớn logic nghiệp vụ thời gian thực.
  3. Khoảng trống kiểm chứng ngữ nghĩa hình thức: Các công cụ lập trình trực quan như VIPLE (Yin et al., 2017 tại Đại học Bang Arizona) hay CHESSIoT (Cicchetti et al., 2019) dù hỗ trợ mô hình hóa trực quan nhưng lại thiếu cơ chế kiểm chứng ràng buộc hình thức tự động ở giai đoạn tiền biên dịch (pre-compilation phase), dẫn đến nguy cơ tiềm ẩn các lỗi xung đột chân cắm (pin conflict) hoặc bế tắc trạng thái (deadlock).

Luận án của NCS. Tôn Long Phước định vị chính xác vào khoảng trống này bằng cách thiết lập mô hình siêu dữ liệu kép (Dual Metamodel) kết hợp hệ thống tập luật ràng buộc ngữ nghĩa và kiểm chứng tự động bằng bộ giải SAT của Alloy Analyzer. Đây là bước tiến vượt bậc so với các công bố của Midgar và Asm2C++, mang lại khả năng tái sử dụng độc lập: một kiến trúc phần cứng có thể thực thi nhiều ứng dụng khác nhau và ngược lại.

Đó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 khung lý thuyết Kỹ nghệ hướng mô hình (MDE) và kiến trúc 4 tầng siêu mô hình (MOF: M0–M3) của Object Management Group (OMG) vào miền tính toán biên cực hạn của thiết bị đeo tay IoWT:

  • Tách biệt mối quan tâm (Separation of Concerns): Mở rộng lý thuyết của Martin Fowler và Harel Statecharts thông qua việc phân rã toàn diện hệ thống IoWT thành hai không gian mô hình trực giao: Siêu mô hình Phần cứng ($M_{HW}$) và Siêu mô hình Ứng dụng nghiệp vụ ($M_{APP}$).
  • Cơ chế ánh xạ ngữ nghĩa dựa trên tập luật (Rule-based Semantic Mapping): Xây dựng mô hình quan hệ toán học biểu diễn mối liên kết giữa các trạng thái điều khiển, các sự kiện chuyển tiếp với các chân vào/ra (I/O pins) của vi điều khiển, được chuẩn hóa thông qua hệ thống mệnh đề:

$$\mathcal{S}{code} = \mathcal{T}{gen}\Big( \mathcal{M}{APP} \bowtie{\mathcal{R}{rules}} \mathcal{M}{HW} \Big)$$

Trong đó $\mathcal{T}{gen}$ là hàm chuyển đổi mẫu khuôn (template transformation) và $\mathcal{R}{rules}$ là tập hợp các tiên đề ràng buộc ngữ nghĩa.

  • Tích hợp logic quan hệ bậc nhất (First-Order Relational Logic): Chuyển đổi trạng thái động của hệ thống thời gian thực sang không gian trạng thái của ngôn ngữ đặc tả Alloy do Daniel Jackson (MIT) phát triển, chứng minh tính đúng đắn của việc chuyển đổi mô hình mà không cần phụ thuộc vào trình biên dịch phần cứng.
       ┌─────────────────────────────────────────────────────────┐
       │                MICRASPIS 4-TIER FRAMEWORK               │
       └────────────────────────────┬────────────────────────────┘
                                    │
 ┌──────────────────────────────────┴──────────────────────────────────┐
 │ TẦNG 1: THIẾT KẾ & ĐẶC TẢ TRỰC QUAN (Eclipse GEF / EMF Metamodels) │
 │  ┌───────────────────────────────┐ ┌──────────────────────────────┐ │
 │  │  Hardware Spec Metamodel (M2) │ │ App State Machine Metamodel  │ │
 │  │   (Sensors, Actuators, Pins)  │ │   (States, Transitions, Evt) │ │
 │  └───────────────┬───────────────┘ └──────────────┬───────────────┘ │
 └──────────────────┼────────────────────────────────┼─────────────────┘
                    ▼                                ▼
 ┌─────────────────────────────────────────────────────────────────────┐
 │ TẦNG 2: KIỂM TRA CÚ PHÁP & RÀNG BUỘC (Semantic & Rule Verification) │
 │  - Sub-phase 1: Kiểm tra ràng buộc phần cứng & ánh xạ nghiệp vụ     │
 │  - Sub-phase 2: Kiểm tra cú pháp biểu diễn & tính đầy đủ            │
 │  - Formal Engine: Tích hợp Alloy Analyzer kiểm tra bế tắc (SAT)     │
 └──────────────────────────────────┬──────────────────────────────────┘
                                    │
                                    ▼
 ┌─────────────────────────────────────────────────────────────────────┐
 │ TẦNG 3: BỘ SINH MÃ NGUỒN TỰ ĐỘNG (Template-Driven Code Generator)   │
 │  - Khớp nối mẫu mã C++ tối ưu hóa bộ nhớ cho Arduino                │
 │  - Tự động sinh mã cấu hình phần cứng, vòng lặp xử lý & ngắt        │
 └──────────────────────────────────┬──────────────────────────────────┘
                                    │
                                    ▼
 ┌─────────────────────────────────────────────────────────────────────┐
 │ TẦNG 4: MÃ NGUỒN THỰC THI & TÀI LIỆU HƯỚNG DẪN LẮP RÁP (C++ Engine) │
 │  - Mã nguồn C++ hoàn thiện >= 65%                                   │
 │  - Tài liệu sơ đồ lắp chân phần cứng (Pin Configuration Guide)      │
 └─────────────────────────────────────────────────────────────────────┘

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

Khung phân tích của luận án hiện thực hóa một kiến trúc 4 tầng hoàn chỉnh:

  1. Tầng Thiết kế và Đặc tả trực quan: Xây dựng trên nền tảng Eclipse Modeling Framework (EMF) và Graphical Editing Framework (GEF), cung cấp cú pháp cụ thể dạng đồ họa cho phép kéo-thả các linh kiện phần cứng (cảm biến nhiệt độ, nhịp tim, màn hình OLED, còi buzzer, nút bấm) và vẽ lược đồ máy trạng thái biểu diễn nghiệp vụ.
  2. Tầng Kiểm tra Cú pháp và Đánh giá Ràng buộc: Vận hành qua 2 pha phụ: Pha 1 thực hiện đánh giá các tập luật ràng buộc phần cứng (như giới hạn số chân analog/digital, mức tiêu thụ năng lượng) và Pha 2 kiểm tra cú pháp chuyển trạng thái, ngăn ngừa các chu trình kín vô hạn.
  3. Tầng Sinh mã chuyển đổi (Code Generation Engine): Sử dụng cơ chế ánh xạ mẫu (code templates) viết bằng ngôn ngữ C++ để biến đổi các phần tử mô hình đã được xác thực thành các cấu trúc mã nguồn hướng sự kiện.
  4. Tầng Kiểm chứng Hình thức với Alloy: Chuyển đổi cấu trúc mô hình sang các khối sig (signature) và tập luật sang các khối fact, assert trong Alloy nhằm kiểm chứng tính toàn vẹn thời gian thực (temporal state validity) thông qua bộ giải SAT (SAT-solver).

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

Thiết kế nghiên cứu

Nghiên cứu tuân thủ chặt chẽ phương pháp luận Khoa học Thiết kế (Design Science Research Methodology - DSRM) kết hợp lập trường nhận thức luận Thực chứng Thực dụng (Pragmatic Positivism). Hệ thống nghiên cứu được thiết kế theo phương pháp hỗn hợp đa mức (Multi-level Mixed-Methods Design), dung hòa giữa việc chứng minh hình thức toán học trừu tượng với đánh giá thực nghiệm kỹ thuật và điều tra xã hội học định lượng.

Quy trình nghiên cứu rigorous

Quy trình nghiên cứu trải qua các giai đoạn được kiểm soát nghiêm ngặt:

  • Xây dựng Siêu mô hình: Định nghĩa cú pháp trừu tượng bằng mô hình Ecore trong EMF. Siêu mô hình phần cứng quản lý các lớp Device, Board, Pin, Sensor, Actuator. Siêu mô hình ứng dụng quản lý State, InitialState, FinalState, Transition, Event, Action.
  • Hệ thống hóa Tập luật và Biện giải: Thiết lập bảng luật ánh xạ logic nghiệp vụ vào các chân ngắt phần cứng, ngăn ngừa sai sót cấu hình vật lý.
  • Kỹ thuật Tam giác đạc (Triangulation):
    • Tam giác đạc phương pháp: Kết hợp giữa chứng minh logic hình thức tự động (Alloy SAT Solver), phân tích độ phức tạp mã tĩnh (Static Code Analysis - LOC, tỷ lệ dòng chú thích), và khảo sát người dùng thực tế.
    • Tam giác đạc dữ liệu: Thu thập dữ liệu từ các dự án giả lập chuẩn hóa, đồ án môn học của sinh viên, và các dự án R&D thực tế tại doanh nghiệp.

Data và phân tích

Đặc tính tập dữ liệu và kỹ thuật phân tích được thực hiện với độ chính xác cao:

  • Tập mẫu khảo sát: Quy mô mẫu $N = 161$ đối tượng hợp lệ. Trong đó có 19.3% là các kỹ sư phần mềm, kiến trúc sư hệ thống giàu kinh nghiệm làm việc tại 18 doanh nghiệp công nghệ; 80.7% là sinh viên chuyên ngành Khoa học Máy tính, Kỹ thuật Máy tính và Công nghệ Phần mềm tại 03 trường đại học và 01 trường cao đẳng kỹ thuật.
  • Công cụ đo lường: Sử dụng thang đo khoảng Likert 5 mức độ (từ Rất không đồng ý đến Rất đồng ý). Độ tin cậy thang đo và tính hợp lệ nội dung được kiểm soát thông qua cấu trúc câu hỏi phân tách rõ rệt giữa tính tiện dụng giao diện, độ chính xác của mã sinh ra và khả năng ứng dụng thực tế.
  • Phân tích Mã nguồn (LOC Benchmark): Phân tích định lượng số dòng mã lệnh (Lines of Code - LOC) được tạo ra tự động so với tổng số LOC cần thiết để hoàn thành ứng dụng. Kết quả được kiểm chứng chéo trên 06 dự án mẫu điển hình.

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

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

Quá trình nghiên cứu và thực nghiệm đã mang lại 4 phát hiện mang tính đột phá với bằng chứng thực nghiệm rõ ràng:

┌────────────────────────────────────────────────────────────────────────┐
│               TỔNG HỢP CÁC KẾT QUẢ THỰC NGHIỆM ĐỘT PHÁ                 │
├────────────────────────────────────────────────────────────────────────┤
│ 1. TỶ LỆ SINH MÃ TỰ ĐỘNG: >= 65% mã C++ hoàn thiện cho các ứng dụng    │
│    (Đo lường trên 06 ca nghiên cứu thực tế như iTempFoll, iRestaurant) │
│                                                                        │
│ 2. ĐỘ HÀI LÒNG CỦA CHUYÊN GIA & NGƯỜI DÙNG: >= 65% Đồng ý / Rất đồng ý │
│    (Khảo sát 161 lập trình viên, bao gồm 19.3% kỹ sư IoT kinh nghiệm)  │
│                                                                        │
│ 3. ĐỘ PHỦ KHẢO SÁT DOANH NGHIỆP & HỌC THUẬT:                           │
│    - 18 Doanh nghiệp công nghệ phần mềm                                │
│    - 03 Trường Đại học + 01 Trường Cao đẳng                            │
│                                                                        │
│ 4. HIỆU QUẢ KIỂM CHỨNG HÌNH THỨC (ALLOY):                              │
│    100% các vi phạm logic & xung đột chân cắm được phát hiện trước biên│
│    dịch thông qua bộ giải SAT (MiniSat / SAT4J).                       │
└────────────────────────────────────────────────────────────────────────┘
  1. Hiệu suất sinh mã vượt trội ($\ge 65%$): Khung thức Micraspis chứng minh khả năng tạo ra tự động hơn 65% tổng số dòng mã nguồn C++ hoàn chỉnh phục vụ trực tiếp cho logic nghiệp vụ thời gian thực của thiết bị đeo, vượt xa mức cấu hình chân cắm 15–20% của các công cụ tiền nhiệm.
  2. Khả năng kiểm soát bế tắc hình thức tuyệt đối: Khi mô hình hóa ứng dụng iRestaurant và iTempFoll bằng Alloy, bộ giải SAT phân tích chính xác toàn bộ không gian trạng thái trong thời gian tính toán dưới 1.5 giây, phát hiện sớm 100% các vi phạm logic chuyển trạng thái hoặc tranh chấp chân tín hiệu mà không cần nạp mã lên phần cứng.
  3. Tính độc lập và tái sử dụng đa chiều: Mô hình kiến trúc phần cứng của một thiết bị đo nhiệt độ/nhịp tim có thể được tái cấu hình để thực thi các ứng dụng khác nhau mà không cần thiết kế lại phần cứng; ngược lại, cùng một kịch bản cảnh báo y tế có thể chuyển dịch sang các dòng vi điều khiển khác bằng cách cập nhật tập luật ánh xạ.
  4. Mức độ sẵn sàng tiếp nhận công nghiệp: Khảo sát định lượng trên 161 lập trình viên chỉ ra rằng hơn 65% đánh giá tích cực (Đồng ý và Rất đồng ý) về khả năng rút ngắn thời gian phát triển dự án và tính minh bạch của mã nguồn được chú thích đầy đủ.

Implications đa chiều

  • Về mặt Lý thuyết: Luận án mở ra một hướng tích hợp mới giữa Kỹ nghệ hướng mô hình (MDE) và các phương pháp hình thức (Formal Methods), minh chứng rằng việc lồng ghép logic mệnh đề quan hệ vào siêu mô hình là hoàn toàn khả thi và cần thiết để đảm bảo tính an toàn cho hệ thống phần mềm nhúng IoT.
  • Về mặt Phương pháp luận: Cung cấp một quy trình mẫu mực về việc thiết kế DSL trong ngữ cảnh hẹp, bao gồm việc xây dựng siêu mô hình kép, định nghĩa hệ luật ràng buộc và thiết lập bộ sinh mã hướng mẫu.
  • Về mặt Thực tiễn và Công nghiệp: Giúp các doanh nghiệp IoT cắt giảm hơn 50% thời gian đưa sản phẩm ra thị trường (Time-to-Market), giảm thiểu chi phí nhân công lập trình cấp thấp và loại bỏ các lỗi nghiêm trọng trong quá trình lắp ráp phần cứng nhờ tập tin hướng dẫn cấu hình tự động.
  • Về mặt Chính sách và Xã hội: Thúc đẩy tiêu chuẩn hóa quy trình phát triển các thiết bị y tế cá nhân và thiết bị bảo hộ thông minh, hỗ trợ hiệu quả cho các chương trình ứng phó thảm họa và y tế cộng đồng (đặc biệt trong bối cảnh các đại dịch như Covid-19).

Limitations và Future Research

Mặc dù đạt được những kết quả xuất sắc, luận án thẳng thắn thừa nhận các giới hạn kỹ thuật:

  • Phạm vi nền tảng phần cứng: Công cụ Micraspis hiện tại mới chỉ tối ưu hóa sinh mã cho các dòng vi điều khiển chuẩn kiến trúc Arduino (AVR/ARM cơ bản) và các ngoại vi I/O thông dụng, chưa mở rộng sang các kiến trúc chip SoC đa lõi phức tạp (như ESP32, STM32 chạy FreeRTOS).
  • Môi trường triển khai: Micraspis hiện hoạt động dưới dạng trình cắm (plugin) tích hợp trên nền tảng máy trạm Eclipse RCP, chưa được chuyển đổi thành nền tảng Web-based IDE hoàn chỉnh trên nền điện toán đám mây.
  • Tối ưu hóa mã nguồn nâng cao: Chưa tích hợp các giải thuật tối ưu hóa mức tiêu thụ năng lượng (Low-Power Optimization) và cấp phát bộ nhớ động trong quá trình sinh mã tự động.

Chương trình nghiên cứu tương lai (Future Research Agenda):

  1. Mở rộng khung thức sinh mã lên nền tảng Web và đám mây, tích hợp công nghệ WebAssembly và Cloud IDE.
  2. Bổ sung các siêu mô hình hỗ trợ hệ điều hành thời gian thực (RTOS), xử lý song song và quản lý năng lượng thông minh.
  3. Ứng dụng trí tuệ nhân tạo (AI-assisted MDE) để tự động sinh các tập luật kiểm chứng từ tài liệu mô tả yêu cầu người dùng bằng ngôn ngữ tự nhiên.
  4. Mở rộng thư viện linh kiện phần cứng cho các thiết bị sinh trắc học y tế chuyên sâu và các giao thức kết nối công nghiệp không dây (Zigbee, LoRaWAN, BLE Mesh).

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

Các kết quả nghiên cứu của luận án đã được công bố trên các diễn đàn khoa học uy tín cao nhất thế giới:

  • Tạp chí quốc tế hàng đầu: 01 bài báo đăng trên IEEE Access (Tập 9, 2021, tr. 13129–13141) thuộc danh mục SCIE, Q1, Impact Factor: 3.367, khẳng định chất lượng và đóng góp khoa học tầm quốc tế.
  • Hội thảo quốc tế chuyên ngành danh giá: 01 công trình tại IEEE EDOC 2019 (Paris, Pháp - Hội nghị hạng A2 theo chuẩn Qualis), 01 công trình tại Springer FDSE 2017, và nhiều bài báo trên các hội thảo của IEEE Computer Society (ACOMP).
  • Tác động chuyển giao: Công cụ Micraspis đã được thử nghiệm thực tế tại 18 doanh nghiệp phần mềm và đưa vào giảng dạy thực hành tại các cơ sở đào tạo đại học, chứng minh tính ứng dụng thực tiễn vượt bậc trong việc đào tạo kỹ sư công nghệ phần mềm IoT.

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

  • Nghiên cứu sinh và Giới học thuật: Tiếp cận một khung lý thuyết vững chắc kết hợp giữa MDE và Alloy, gợi mở nhiều hướng nghiên cứu mới về kiểm chứng phần mềm nhúng.
  • Kỹ sư và Trưởng nhóm R&D tại Doanh nghiệp IoT: Sở hữu một công cụ mạnh mẽ giúp tự động hóa khâu viết mã, giảm thiểu lỗi phần mềm và chi phí thử nghiệm.
  • Giảng viên và Sinh viên CNTT: Sử dụng Micraspis như một công cụ trực quan sinh động trong giảng dạy và học tập các môn học Kỹ nghệ phần mềm, Thiết kế hệ thống nhúng và Lập trình IoT.
  • Các Cơ quan Quản lý và Tổ chức Y tế/Cứu trợ: Tiếp cận phương án phát triển nhanh các giải pháp thiết bị đeo tay thông minh phục vụ cộng đồng với chi phí thấp và độ tin cậy cao.

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ì?

Đóng góp độc đáo nhất là việc thiết lập mô hình ánh xạ ngữ nghĩa hình thức giữa hai siêu mô hình độc lập trực giao (Siêu mô hình Phần cứng và Siêu mô hình Ứng dụng máy trạng thái) thông qua hệ thống tập luật ràng buộc, được bảo đảm tính toàn vẹn bằng phương pháp hình thức của ngôn ngữ Alloy (Daniel Jackson, MIT). Điều này giải quyết trọn vẹn sự mâu thuẫn giữa tính trừu tượng mức cao và tính khả thi mức thấp trong kỹ nghệ phần mềm IoWT.

2. Đột phá về phương pháp luận của Micraspis so với các nghiên cứu quốc tế tiền nhiệm?

So với Midgar (chỉ hỗ trợ sinh mã Web/Middleware không có FSM) và Asm2C++ (chỉ chuyển đổi FSM đơn thuần mà không tách biệt kiến trúc phần cứng), Micraspis là công cụ đầu tiên tích hợp trọn vẹn quy trình 4 tầng: Đặc tả trực quan $\to$ Đánh giá tập luật $\to$ Kiểm chứng hình thức Alloy $\to$ Sinh mã nguồn C++ đạt tỷ lệ hoàn thiện $\ge 65%$, kèm theo tài liệu hướng dẫn cấu hình chân cắm vật lý tự động.

3. Phát hiện bất ngờ nhất trong quá trình phân tích dữ liệu thực nghiệm là gì?

Phát hiện bất ngờ nhất là tỷ lệ dòng mã tạo ra tự động cho các xử lý nghiệp vụ thời gian thực đạt mức rất cao ($\ge 65%$) ngay cả trên các ca nghiên cứu có độ phức tạp trạng thái cao như hệ thống giám sát y tế đa kênh iTempFoll. Điều này phá vỡ quan niệm truyền thống cho rằng các công cụ MDE chỉ sinh được các khung mã tĩnh (boilerplate code).

4. Giao thức tái lập nghiên cứu (Replication Protocol) có được cung cấp minh bạch không?

Luận án cung cấp đầy đủ và chi tiết toàn bộ các siêu mô hình Ecore, bảng định nghĩa tập luật cú pháp/ràng buộc, các đoạn mã đặc tả mẫu trên ngôn ngữ Alloy, cấu trúc mã nguồn C++ mẫu và bảng câu hỏi khảo sát 5-point Likert scale. Toàn bộ 06 case-studies (bao gồm iTempFoll và iRestaurant) đều có đặc tả trạng thái và sơ đồ phần cứng chi tiết trong phụ lục.

5. Tầm nhìn nghiên cứu 10 năm (10-year Research Agenda) được hoạch định ra sao?

Tầm nhìn 10 năm định hướng phát triển một Hệ sinh thái Kỹ nghệ Phần mềm Đám mây cho IoT Tự hành, nơi các siêu mô hình có khả năng tự thích ứng (Self-adaptive Metamodeling), tích hợp mô hình ngôn ngữ lớn để tự động sinh mã nhúng tối ưu hóa năng lượng cho các chip thần kinh (Neuromorphic/Edge-AI Chips) trên thiết bị đeo thế hệ mới.

Kết luận

Luận án tiến sĩ của NCS. Tôn Long Phước là một công trình nghiên cứu khoa học công phu, nghiêm túc và mang tính đột phá cao trong lĩnh vực Khoa học Máy tính. Tóm lược 5 đóng góp cốt lõi của công trình:

  1. Xây dựng hoàn chỉnh khung thức tổng quát cho bài toán sinh mã nguồn trong ngữ cảnh hẹp dành cho các thiết bị đeo tay thông minh IoWT.
  2. Đề xuất hướng tiếp cận kết hợp sáng tạo giữa mô hình hóa máy trạng thái, siêu mô hình phần cứng và hệ thống tập luật ngữ nghĩa.
  3. Hiện thực hóa thành công công cụ Micraspis trên nền tảng Eclipse, cho phép sinh tự động trên 65% mã nguồn C++ thực thi cho dòng bo mạch Arduino.
  4. Ứng dụng thành công phương pháp hình thức Alloy vào việc phát hiện sớm 100% các lỗi xung đột ngữ nghĩa và bế tắc trạng thái ở giai đoạn tiền biên dịch.
  5. Tiến hành thực nghiệm quy mô và khách quan với 161 chuyên gia, kỹ sư và sinh viên tại 18 doanh nghiệp và 04 trường đại học/cao đẳng, được bảo chứng bằng công bố quốc tế uy tín trên tạp chí đầu ngành IEEE Access (Q1).

Công trình không chỉ giải quyết triệt để một bài toán kỹ thuật cấp thiết mà còn đặt nền móng lý thuyết vững chắc cho sự phát triển của kỹ nghệ phần mềm nhúng IoT trong tương lai.