Tổng quan luận án
Luận án tiến sĩ "Sinh mã nguồn cho các thiết bị đeo tay trong các giải pháp thông minh trên nền tảng Internet vạn vật bằng mô hình hóa và tập luật" được thực hiện bởi nghiên cứu sinh Tôn Long Phước, chuyên ngành Khoa học máy tính (mã số: 62.01), dưới sự hướng dẫn 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 Thành phố Hồ Chí Minh vào năm 2022.
Tính cấp thiết và khoảng trống nghiên cứu
Trong lĩnh vực Internet vạn vật (Internet of Things - IoT), các thiết bị đeo tay (Internet of Wearable Things - IoWT) đóng vai trò trung tâm trong nhiều giải pháp thông minh như giám sát sức khỏe, điều phối cứu hộ, hỗ trợ dịch vụ y tế hay nhà hàng. Dù quy mô thị trường thiết bị đeo tay gia tăng nhanh chóng (hơn 400 triệu thiết bị bán ra năm 2020), việc phát triển phần mềm cho các thiết bị này đối mặt với nhiều rào cản. Các công cụ hỗ trợ phát triển phần mềm tự động hoặc bán tự động trong IoT đa phần chỉ tập trung vào việc cấu hình chân pin hoặc sinh mã kết nối thiết bị cấp thấp, chưa giải quyết được bài toán sinh mã cho các xử lý nghiệp vụ cụ thể. Bên cạnh đó, có sự tách biệt lớn giữa việc đặc tả kiến trúc phần cứng và đặc tả quy trình nghiệp vụ của ứng dụng, dẫn đến việc thiếu khả năng tái sử dụng mã nguồn và thiết kế trên các thiết bị có kiến trúc tương đồng. Khoảng trống nghiên cứu được xác định là sự thiếu vắng một khung thức thống nhất cho phép tích hợp mô hình hóa trừu tượng với các tập luật ràng buộc ngữ nghĩa để tự động sinh mã nguồn hoàn chỉnh cho ứng dụng chạy trên thiết bị đeo tay.
Mục tiêu nghiên cứu
Luận án xác định một mục tiêu tổng quát là xây dựng khung thức sinh mã nguồn tự động cho các ứng dụng trong các giải pháp thông minh thuộc lĩnh vực IoT, cụ thể hóa qua ba mục tiêu:
- [OB1]: Tìm hiểu các công trình nghiên cứu về sinh mã nguồn theo hướng mô hình, đặc biệt trong lĩnh vực Internet vạn vật. Từ đó, đề xuất một khung thức tổng quát cho việc sinh mã nguồn ứng dụng chạy trên các thiết bị đeo tay, cho phép đặc tả ứng dụng và kiến trúc phần cứng một cách hợp lý.
- [OB2]: Nghiên cứu đưa ra cách tiếp cận đặc tả ứng dụng và kiến trúc phần cứng của thiết bị đeo tay bằng mô hình hóa. Trong đó, ứng dụng được đặc tả bằng lược đồ máy trạng thái (state machine), phần cứng được đặc tả bằng mô hình hóa; mô hình đặc tả phải được kiểm chứng tính đúng đắn với sự kết hợp của các tập luật nhằm đảm bảo chất lượng mã nguồn sinh ra.
- [OB3]: Xây dựng công cụ với giao diện đồ họa thân thiện nhằm triển khai khung thức đề xuất; cho phép người dùng đặc tả ứng dụng và phần cứng, hỗ trợ tái sử dụng mã nguồn và kiến trúc phần cứng; đảm bảo mã nguồn sinh ra đạt tính đúng đắn, tỷ lệ tự động cao; đồng thời xây dựng phương án kiểm thử khách quan qua các tiêu chí về tỷ lệ sinh mã, chất lượng mã nguồn và độ hài lòng của người dùng.
Câu hỏi nghiên cứu
Để hiện thực hóa các mục tiêu trên, luận án đặt ra ba câu hỏi nghiên cứu:
- [RQ1]: Đã có một khung thức hay một công cụ tổng quát nào cho việc sinh mã nguồn của các ứng dụng chạy trên thiết bị đeo tay trong lĩnh vực Internet vạn vật hay chưa? Khung thức đó có bao hàm các bước từ đặc tả ứng dụng, thiết kế phần cứng, hỗ trợ kiểm tra tính đúng đắn của đặc tả phần cứng cũng như ứng dụng nhằm sinh mã nguồn đáp ứng yêu cầu người dùng hay không?
- [RQ2]: Làm sao để đặc tả phần cứng của thiết bị đeo tay và các ứng dụng chạy trên thiết bị đó bằng sự kết hợp giữa mô hình hóa và các tập luật nhằm đảm bảo tính đúng đắn và hiệu quả cho bài toán sinh mã nguồn?
- [RQ3]: Từ khung thức và cách đặc tả trên, xây dựng một công cụ hỗ trợ người dùng như thế nào để sinh mã nguồn cho các giải pháp thông minh chạy trên thiết bị đeo tay? Đồng thời kiểm chứng như thế nào để đảm bảo khách quan tính đúng đắn, hiệu quả của công cụ được xây dựng?
Đối tượng và phạm vi nghiên cứu
- Đối tượng nghiên cứu: Phương pháp và công cụ sinh mã nguồn tự động kết hợp mô hình hóa máy trạng thái và hệ thống tập luật ràng buộc ngữ nghĩa cho các thiết bị đeo tay (IoWT) trong các giải pháp thông minh.
- Phạm vi không gian và công nghệ: Các ứng dụng chạy trên thiết bị đeo tay trong hệ sinh thái IoT kết nối qua vi điều khiển dòng Arduino; các linh kiện phần cứng dừng lại ở các thành phần cơ bản (thiết bị nhập/xuất, cảm biến đơn giản, kết nối cơ bản); công cụ phát triển phần mềm được xây dựng dưới dạng plug-in trên nền tảng Eclipse.
- Phạm vi thời gian và thực nghiệm: Số liệu thực nghiệm và khảo sát người dùng được thu thập trong giai đoạn 2020–2022 trên 161 lập trình viên, triển khai kiểm thử tại 3 trường đại học, 1 trường cao đẳng, 18 doanh nghiệp phần mềm và đánh giá qua 6 bài toán mẫu (case-study).
Tổng quan tài liệu và vị trí của luận án
Luận án tiến hành khảo sát có hệ thống các hướng tiếp cận sinh mã nguồn trong kỹ nghệ phần mềm và lĩnh vực Internet vạn vật, tập trung vào các công cụ sinh mã dựa trên mô hình (Model-Driven Engineering - MDE):
- Midgar (Garcia-Herranz và cộng sự, 2014): Nền tảng DSL trên nền Web cho phép mô hình hóa các đối tượng IoT không đồng nhất dựa trên quy trình sáu nút logic để tạo mã Java chạy trên Arduino. Tuy nhiên, Midgar không hỗ trợ mô hình hóa máy trạng thái và không hỗ trợ thiết kế kiến trúc phần cứng của thiết bị đeo tay.
- Asm2C++ (Gargantini và cộng sự, 2017): Công cụ chuyển đổi mô hình máy trạng thái trừu tượng (Abstract State Machines) sang mã nguồn C++ chạy trên Arduino. Asm2C++ chưa tách biệt rõ ràng giữa phần cứng và ứng dụng, dẫn đến hạn chế trong việc tái sử dụng phần cứng hoặc ứng dụng chéo.
- IoTSuite (Patel và cộng sự, 2013): Nền tảng tự động hóa từ thiết kế, hiện thực đến triển khai ứng dụng IoT trên Raspberry Pi, sử dụng Java. IoTSuite hỗ trợ mô hình khái niệm nhưng mã nguồn tạo ra chủ yếu phục vụ việc kết nối các thành phần cấp thấp, hạn chế về khả năng tùy biến phần cứng phong phú.
- UML4IoT (Thramboulidis và cộng sự, 2015): Sử dụng biểu đồ lớp (Class diagram) UML để tạo các lớp bao bọc kết nối (IoTwrapper) bằng Java cho các thiết bị vật lý cấp thấp, chưa chú trọng đến việc mô hình hóa hành vi nghiệp vụ.
- VIPLE (Yin và cộng sự, Đại học Bang Arizona / Microsoft, 2017): Công cụ lập trình trực quan bằng máy trạng thái hữu hạn cho IoT và rô bốt (LEGO Mindstorms EV3), sinh mã C++. Dù hỗ trợ cấu hình chân pin và xử lý sự kiện, VIPLE còn hạn chế trong việc quản lý phạm vi biến và tối ưu hóa cho các hệ thống phần mềm nhúng đặc thù.
- EL4IoT (Nguyen và cộng sự, 2017): Khung thức sinh mã tự cấu hình cho thiết bị cấp thấp trên hệ điều hành Contiki, sử dụng Java và XML, nhưng chưa hỗ trợ kiểm chứng ràng buộc và chưa sinh được mã nghiệp vụ ứng dụng hoàn chỉnh.
- ThingML (Harrand và cộng sự, 2016): Kết hợp ngôn ngữ mô hình hóa và trình sinh mã C/C++, Java, JavaScript cho Arduino, tập trung vào cấu hình phần cứng và kết nối giữa các thiết bị mà không hỗ trợ đặc tả trừu tượng hóa phần mềm ứng dụng.
- M3 Framework (Gyrard và cộng sự, 2014): Khung thức dựa trên Web ngữ nghĩa với 7 tầng xử lý để chuẩn hóa và giải thích dữ liệu cảm biến (Machine-to-Machine Measurement), sinh mã C++ dạng mẫu thử (prototype).
- CHESSIoT (Ciccozzi và cộng sự, 2018): Khung thức tiếp cận theo hướng mô hình dựa trên các khung nhìn (IoTElement, VirtualBoard, VirtualEntity) và ánh xạ tới ThingML để sinh mã C/C++, Java cho Arduino.
| STT |
Tên khung thức |
Giao diện |
Mô hình sử dụng |
Khả năng sinh ứng dụng |
Ngôn ngữ tổ chức |
Bo mạch hỗ trợ |
| 1 |
Midgar |
Web |
Finite State Machines |
Có |
Java |
Arduino |
| 2 |
Asm2C++ |
Plug-in |
Abstract State Machines |
Dạng mẫu thử |
C++ |
Arduino |
| 3 |
IoTSuite |
Plug-in |
Conceptual Model |
Dạng mẫu thử |
Java |
Raspberry Pi |
| 4 |
UML4IoT |
Plug-in |
Class diagram |
Dạng mẫu thử |
Java |
Thiết bị cấp thấp |
| 5 |
VIPLE |
Web, Desktop |
Finite State Machines |
Có |
C++ |
LEGO EV3, Robot |
| 6 |
EL4IoT |
Plug-in |
Abstract State Machines |
Không |
Java, XML |
Thiết bị cấp thấp |
| 7 |
ThingML |
Plug-in |
Abstract State Machines |
Không |
C/C++, Java, JS |
Arduino |
| 8 |
M3 Framework |
Web |
Abstract State Machines |
Dạng mẫu thử |
C++ |
Cảm biến |
| 9 |
CHESSIoT |
Plug-in |
Finite State Machines |
Dạng mẫu thử |
C/C++, Java |
Arduino |
| 10 |
Micraspis |
Plug-in |
Finite State Machines |
Có |
C++ |
Arduino |
Khoảng trống nghiên cứu được lựa chọn giải quyết
Các công cụ hiện hữu phần lớn dừng lại ở mức sinh mã cấu hình thiết bị cấp thấp, tạo khung kết nối hoặc tạo các bộ bao bọc (wrappers), chưa giải quyết được việc sinh mã nghiệp vụ hoàn chỉnh cho ứng dụng chạy trên thiết bị đeo tay. Hơn nữa, chưa có công cụ nào kết hợp đồng thời mô hình hóa máy trạng thái với hệ thống tập luật để kiểm soát ràng buộc ngữ nghĩa và cho phép tách biệt giữa thiết kế phần cứng và thiết kế phần mềm, nhằm phục vụ việc tái sử dụng linh hoạt. Luận án lựa chọn giải quyết trực tiếp khoảng trống này thông qua công cụ Micraspis.
Cơ sở lý thuyết và phương pháp nghiên cứu
Cơ sở lý thuyết
- Kỹ thuật phát triển phần mềm dựa trên mô hình (MDE, MDD, MDA): Luận án vận dụng tiêu chuẩn Kiến trúc hướng mô hình (Model-Driven Architecture - MDA) của OMG với cấu trúc siêu dữ liệu MOF (Meta Object Facility) phân cấp thành 4 tầng: M0 (hệ thống thực tế), M1 (mô hình hệ thống), M2 (siêu mô hình - meta-model quy định cú pháp và ngữ nghĩa của M1), và M3 (meta-metamodel định nghĩa meta-model). Hệ thống áp dụng ba mức nhìn: Mô hình độc lập tính toán (CIM), Mô hình độc lập nền tảng (PIM), và Mô hình phụ thuộc nền tảng (PSM).
- Ngôn ngữ chuyên biệt hóa trong ngữ cảnh hẹp (DSL): Phân định rõ hai thành phần: cú pháp trừu tượng (abstract syntax) được định nghĩa thông qua meta-model và cú pháp cụ thể (concrete syntax) thể hiện qua giao diện kéo thả đồ họa hoặc văn bản.
- Lược đồ máy trạng thái (State Machine): Dùng để biểu diễn các trạng thái hoạt động, sự kiện chuyển đổi trạng thái và hành vi xử lý nghiệp vụ của thiết bị đeo tay.
- Phương pháp hình thức với ngôn ngữ Alloy (MIT): Dùng để đặc tả logic và kiểm chứng mô hình ở giai đoạn sớm (early requirements). Alloy sử dụng cấu trúc chữ ký (
sig) để định nghĩa đối tượng và các vị từ/tiên đề (fact) để biểu diễn các ràng buộc nghiệp vụ. Bộ phân tích Alloy Analyzer áp dụng kỹ thuật giải quyết mệnh đề logic (SAT solver) nhằm tìm kiếm phản ví dụ hoặc xác thực tính nhất quán của mô hình hướng thời gian (temporal model).
Phương pháp nghiên cứu thực tế
- Phương pháp kỹ thuật - thực nghiệm (Engineering & Empirical Method): Thiết kế meta-model, phát triển plug-in trên nền tảng Eclipse bằng các thư viện Eclipse Modeling Framework (EMF) và Graphical Editing Framework (GEF); thiết lập cơ chế chuyển đổi mô hình sang mã nguồn C++ dựa trên các mẫu mã (code templates) và tập luật.
- Phương pháp kiểm chứng tính đúng đắn: Xây dựng giải thuật kiểm soát đối tượng và ánh xạ các tập luật nghiệp vụ thành các mệnh đề logic trong Alloy để mô phỏng và kiểm tra các trạng thái vi phạm ràng buộc trên môi trường Java.
- Phương pháp đánh giá định lượng:
- Đo lường số dòng lệnh (Lines of Code - LOC) sinh ra tự động so với tổng số dòng lệnh hoàn thiện của ứng dụng.
- Khảo sát bằng bảng câu hỏi theo thang đo Likert (5 mức độ) đối với 161 lập trình viên (trong đó 19,3% là kỹ sư có kinh nghiệm trong lĩnh vực IoT).
- Triển khai thử nghiệm tại 3 trường đại học, 1 trường cao đẳng và 18 doanh nghiệp phần mềm thuộc các quy mô khác nhau.
Nguồn tư liệu và dữ liệu
Luận án sử dụng dữ liệu từ 6 bài toán mẫu (case-study) thực tế, tiêu biểu là: hệ thống theo dõi sức khỏe bệnh nhân và cảnh báo y tế iTempFoll (gồm thiết bị đeo tay cho bệnh nhân và bác sĩ); hệ thống quản lý nhà hàng thông minh iRestaurant (gồm thiết bị cho khách hàng và nhân viên phục vụ); và hệ thống điều khiển đèn giao thông (Traffic Light).
Nội dung chính theo từng chương
Chương 1: Giới thiệu bài toán
Chương này thiết lập bối cảnh nghiên cứu về xu hướng phát triển của các thiết bị đeo tay trong kỷ nguyên IoT và sự cần thiết của các công cụ hỗ trợ sinh mã tự động. Tác giả chỉ ra 6 vấn đề kỹ thuật cốt lõi trong việc sinh mã nguồn cho thiết bị đeo tay:
- Thiếu khung thức thống nhất cho bài toán sinh mã;
- Khó khăn trong việc xác định phạm vi xử lý tự động (thu thập, truyền tải và thực thi hành động);
- Thách thức trong việc đặc tả quy trình nghiệp vụ rõ ràng;
- Sự phụ thuộc của mã nguồn vào tính đúng đắn của mô hình đặc tả ban đầu;
- Sự tách biệt lớn giữa kiến trúc phần cứng và xử lý nghiệp vụ;
- Yêu cầu về khả năng tái sử dụng và chất lượng mã nguồn.
Chương 1 cũng công bố 3 mục tiêu nghiên cứu ([OB1] đến [OB3]), 3 câu hỏi nghiên cứu ([RQ1] đến [RQ3]), các giới hạn nghiên cứu và danh mục các công trình khoa học đã công bố của tác giả (bao gồm bài báo trên tạp chí IEEE Access năm 2021).
Chương 2: Tình hình nghiên cứu và kiến thức nền tảng
Chương 2 phân tích tổng quan các công trình liên quan đến ngôn ngữ chuyên biệt hóa trong ngữ cảnh hẹp (DSL), kỹ thuật MDE, MDD, MDA và việc ứng dụng DSL trong IoT. Tác giả khảo sát các công cụ lập trình trực quan và sinh mã hiện có, phân tích các rào cản kỹ thuật của việc lập trình thiết bị đeo tay (IoWT) như năng lượng giới hạn, phần cứng không đồng nhất và tính biến đổi của quy trình nghiệp vụ. Ngoài ra, chương này cung cấp cơ sở lý thuyết về kiến trúc MOF 4 tầng, các mô hình PIM/PSM/CIM và các kỹ thuật tăng cường ngữ nghĩa cho mô hình bằng ngôn ngữ ràng buộc như OCL hoặc ngôn ngữ đặc tả hình thức Alloy.
Chương 3: Khung thức tổng quát xây dựng ngôn ngữ chuyên biệt hóa trong ngữ cảnh hẹp cho lĩnh vực Internet vạn vật
Chương 3 đề xuất khung thức tổng quát phục vụ việc sinh mã nguồn cho các ứng dụng IoT dựa trên MDA. Khung thức tích hợp quy trình gồm các pha: đặc tả ứng dụng, phân tích kiểm tra ràng buộc, và sinh mã nguồn dựa trên các tập luật và mẫu định sẵn. Tác giả thiết kế siêu mô hình (meta-model) cho các thành phần phần cứng và ứng dụng, cho phép nhà phát triển thiết kế trực quan trên giao diện và ánh xạ sang mã C++. Khung thức giải quyết sự phân tách giữa phần cứng và ứng dụng thông qua cơ chế ánh xạ độc lập, giúp hỗ trợ mục tiêu [OB1] của luận án.
Chương 4: Công cụ sinh mã nguồn cho các ứng dụng chạy trên thiết bị đeo tay Micraspis
Chương 4 mô tả chi tiết việc xây dựng công cụ Micraspis dưới dạng plug-in tích hợp trong môi trường Eclipse, sử dụng các thư viện EMF và GEF. Kiến trúc của Micraspis được chia thành 4 tầng:
- Tầng 1 - Thiết kế phần cứng và đặc tả ứng dụng: Cung cấp môi trường trực quan cho phép kéo thả linh kiện (cảm biến, nút nhấn, màn hình, chân pin bo mạch Arduino) và thiết lập sơ đồ máy trạng thái nghiệp vụ.
- Tầng 2 - Kiểm tra cú pháp và ràng buộc dựa trên tập luật: Chia làm hai giai đoạn con (Sub-phase 1: kiểm tra ràng buộc logic phần cứng và chuyển đổi trạng thái; Sub-phase 2: kiểm tra cú pháp mô hình).
- Tầng 3 - Cơ chế sinh mã nguồn: Chuyển đổi từ đặc tả cụ thể, đặc tả trừu tượng và khai báo trực quan thành mã nguồn chương trình C++ hoàn chỉnh dựa trên các mẫu (templates) tương ứng cho vi điều khiển Arduino.
- Tầng 4 - So sánh và kết xuất kết quả: Đưa ra mã nguồn kèm tài liệu hướng dẫn cấu hình phần cứng.
Kiến trúc này được minh họa chi tiết qua giải pháp y tế iTempFoll với hai thiết bị đeo tay riêng biệt cho bệnh nhân (theo dõi nhiệt độ, gửi cảnh báo) và bác sĩ (nhận cảnh báo, kích hoạt điều trị).
Chương 5: Kiểm chứng và ứng dụng
Chương 5 trình bày các kết quả đánh giá thực nghiệm công cụ Micraspis trong môi trường giáo dục (thực hành lập trình IoT tại các trường đại học) và công nghiệp (18 doanh nghiệp phần mềm):
- Tỷ lệ sinh mã tự động: Công cụ tạo ra trung bình hơn 65% số dòng lệnh (LOC) cần thiết để hoàn thiện logic nghiệp vụ của ứng dụng (trong các case-study nhỏ, tỷ lệ mã nguồn sinh tự động đạt mức cao, giúp giảm thiểu đáng kể việc bổ sung mã thủ công).
- Mức độ hài lòng của người dùng: Dựa trên khảo sát 161 lập trình viên với bảng câu hỏi thang đo Likert, có ít nhất 65% người tham gia đánh giá "đồng ý" hoặc "rất đồng ý" về tính tiện ích, giao diện trực quan và khả năng hỗ trợ phát triển nhanh của Micraspis.
- Chất lượng mã nguồn: Mã nguồn tạo ra có cấu trúc rõ ràng, tích hợp đầy đủ các chú thích (comments) giải thích chi tiết các khối lệnh và đi kèm tập tin tài liệu hướng dẫn đấu nối chân pin phần cứng.
Chương 6: Mô hình hóa đặc tả nghiệp vụ các giải pháp thông minh bằng ngôn ngữ Alloy
Chương 6 tập trung vào phương pháp sử dụng ngôn ngữ đặc tả hình thức Alloy để nâng cao tính đúng đắn của mô hình ở giai đoạn sớm. Tác giả mô hình hóa các đối tượng, trạng thái và sự kiện thành các cấu trúc Sig, đồng thời chuyển hóa các tập luật và ràng buộc hệ thống thành các tiên đề Fact. Thông qua bộ giải SAT solver của Alloy Analyzer, hệ thống kiểm chứng được các trạng thái thay đổi theo thời gian (temporal models) và phát hiện sớm các vi phạm ràng buộc. Luận án đề xuất một giải thuật kiểm soát đối tượng thông qua tập luật, được minh chứng thông qua ca nghiên cứu hệ thống iRestaurant (gồm thiết bị đeo tay cho nhân viên và khách hàng) được mô phỏng kiểm tra bằng ngôn ngữ Java.
Chương 7: Kết luận và hướng phát triển
Chương cuối tóm tắt lại các kết quả đã đạt được đối với 3 mục tiêu nghiên cứu và đề ra 4 hướng mở rộng: phát triển Micraspis trên nền tảng Web; mở rộng thư viện hỗ trợ phần cứng ngoài dòng Arduino; mở rộng phạm vi sinh mã cho các hệ thống phức tạp hơn; và tối ưu hóa hiệu năng thời gian thực của mã nguồn sinh ra.
Kết quả và những đóng góp mới
Đóng góp mới về mặt lý luận và khoa học
- Phương pháp tiếp cận kết hợp mô hình hóa và tập luật: Đề xuất giải pháp tích hợp giữa mô hình hóa máy trạng thái với hệ thống tập luật ràng buộc ngữ nghĩa trong một ngôn ngữ chuyên biệt ngữ cảnh hẹp (DSL), giúp tăng cường ngữ nghĩa cho siêu mô hình và nâng cao mức độ tự động hóa trong sinh mã.
- Khung thức phát triển tách biệt phần cứng và ứng dụng: Xây dựng khung thức cho phép đặc tả độc lập giữa kiến trúc phần cứng của thiết bị đeo tay và quy trình xử lý nghiệp vụ, từ đó giải quyết bài toán tái sử dụng thiết kế: một ứng dụng có thể chạy trên nhiều cấu hình phần cứng tương thích và ngược lại.
- Quy trình kiểm chứng hình thức bằng Alloy: Ứng dụng thành công ngôn ngữ Alloy và bộ giải SAT solver để kiểm chứng tính đúng đắn và phát hiện xung đột ràng buộc của mô hình ứng dụng IoWT ngay ở giai đoạn đặc tả sớm.
Đóng góp mới về mặt thực tiễn
- Xây dựng công cụ Micraspis: Hiện thực hóa thành công công cụ sinh mã nguồn dưới dạng plug-in trên nền Eclipse, có khả năng tự động tạo ra từ 65% trở lên lượng mã nguồn C++ hoàn thiện chạy trên các vi điều khiển dòng Arduino.
- Quy trình đánh giá thực nghiệm đa chiều: Thiết lập bộ tiêu chí đánh giá khách quan về hiệu quả của công cụ sinh mã thông qua tỷ lệ dòng lệnh (LOC), chất lượng mã nguồn (tích hợp chú thích và tài liệu hướng dẫn phần cứng) và khảo sát thực nghiệm trên 161 lập trình viên tại các trường đại học và doanh nghiệp.
Kiến nghị và giải pháp đề xuất
- Đề xuất áp dụng khung thức mô hình hóa kết hợp tập luật vào quy trình đào tạo thực hành IoT tại các trường đại học và cao đẳng nhằm rút ngắn thời gian làm quen với phần cứng của sinh viên.
- Đề xuất các doanh nghiệp phát triển giải pháp thông minh dựa trên IoWT ứng dụng cơ chế kiểm chứng hình thức sớm bằng Alloy để giảm thiểu chi phí sửa lỗi phần mềm nhúng khi triển khai thực tế.
Hạn chế và hướng nghiên cứu tiếp
Các hạn chế được ghi nhận
- Phần cứng hỗ trợ: Luận án mới chỉ hỗ trợ các bo mạch chủ thuộc dòng vi điều khiển Arduino; các linh kiện phần cứng dừng lại ở các cảm biến và thiết bị nhập/xuất cơ bản.
- Ràng buộc phần cứng: Các quy tắc kiểm tra ràng buộc vật lý chủ yếu giới hạn ở việc kiểm tra xung đột cấu hình chân pin và số lượng linh kiện kết nối tối đa.
- Môi trường triển khai công cụ: Công cụ Micraspis hiện mới chỉ hoạt động như một plug-in phụ thuộc vào môi trường Eclipse, chưa hỗ trợ giao diện người dùng trên nền tảng Web.
- Quy mô thực nghiệm phần mềm: Số lượng ca nghiên cứu kiểm chứng chuyên sâu còn hạn chế (06 bài toán mẫu); luận án chưa tiến hành đo đạc thống kê về thời gian thực thi tối ưu của mã nguồn sinh ra cũng như các chỉ số tối ưu hóa bộ nhớ vi điều khiển.
Hướng nghiên cứu tiếp
- Mở rộng nền tảng Web: Chuyển đổi công cụ Micraspis sang giao diện Web nhằm tăng khả năng tiếp cận và tính tiện dụng cho người dùng.
- Đa dạng hóa phần cứng: Bổ sung hỗ trợ cho các dòng vi điều khiển khác ngoài Arduino (như ESP32, STM32 hoặc Raspberry Pi) và các loại cảm biến phức tạp.
- Mở rộng phạm vi sinh mã: Nâng cao khả năng sinh mã tự động cho các giao thức truyền thông không dây phức tạp và các dịch vụ đám mây kết nối với máy chủ.
- Tối ưu hóa mã nguồn: Nghiên cứu các giải thuật tối ưu hóa mã nguồn C++ nhằm giảm thiểu dung lượng bộ nhớ và tiết kiệm năng lượng tiêu thụ trên các thiết bị đeo tay.
Giá trị tham khảo
Luận án mang lại các giá trị tham khảo cụ thể cho các nhóm đối tượng:
- Nghiên cứu sinh và học viên cao học chuyên ngành Khoa học máy tính, Kỹ thuật phần mềm: Có thể tham khảo phương pháp luận kết hợp giữa MDE, MDA và phương pháp kiểm chứng hình thức bằng ngôn ngữ Alloy (đặc biệt là nội dung tại Chương 3 và Chương 6) để phát triển các nghiên cứu về công cụ DSL hoặc tự động hóa phần mềm.
- Giảng viên và cơ sở đào tạo đại học, cao đẳng ngành IoT, Công nghệ thông tin: Có thể sử dụng công cụ Micraspis và các bài toán mẫu (iTempFoll, iRestaurant) làm tài liệu thực hành giảng dạy lập trình IoT trực quan, giúp người học nhanh chóng tiếp cận việc thiết kế hệ thống nhúng mà không bị quá tải bởi việc lập trình chi tiết chân pin.
- Kỹ sư và nhà phát triển phần mềm trong doanh nghiệp IoT: Tham khảo cấu trúc ánh xạ từ máy trạng thái sang mã C++ và quy trình kiểm soát ràng buộc phần cứng để ứng dụng vào việc xây dựng các công cụ tạo mẫu nhanh (rapid prototyping) cho các sản phẩm thiết bị đeo tay thông minh.
Câu hỏi thường gặp
1. Công cụ Micraspis hoạt động dựa trên nguyên lý kỹ thuật nào và sinh ra loại mã nguồn gì?
Micraspis là một ngôn ngữ chuyên biệt hóa trong ngữ cảnh hẹp (DSL) được xây dựng dưới dạng plug-in trên nền tảng Eclipse (sử dụng thư viện EMF và GEF). Công cụ hoạt động dựa trên nguyên tắc chuyển đổi mô hình sang mã nguồn (Model-to-Code), kết hợp giữa việc kéo thả linh kiện phần cứng và thiết kế sơ đồ máy trạng thái nghiệp vụ, từ đó tự động sinh ra mã nguồn C++ có thể biên dịch và thực thi trực tiếp trên các bo mạch dòng Arduino.
2. Tỷ lệ mã nguồn được tạo ra tự động từ công cụ Micraspis là bao nhiêu?
Theo kết quả thử nghiệm thực nghiệm được công bố trong luận án, công cụ Micraspis có khả năng tạo ra tự động hơn 65% tổng số dòng lệnh (LOC) hoàn thiện cần thiết cho logic nghiệp vụ của các ứng dụng chạy trên thiết bị đeo tay, từ các bài toán đơn giản đến phức tạp.
3. Ngôn ngữ đặc tả Alloy đóng vai trò gì trong luận án?
Alloy được sử dụng như một công cụ kiểm chứng hình thức ở giai đoạn đặc tả sớm. Luận án chuyển đổi các đối tượng và trạng thái thành Sig, chuyển đổi các tập luật và ràng buộc thành các Fact. Sử dụng bộ giải SAT solver của Alloy Analyzer, tác giả kiểm tra tính nhất quán của mô hình hướng thời gian, đảm bảo mô hình không bị vi phạm các quy tắc nghiệp vụ trước khi tiến hành sinh mã C++.
4. Khảo sát đánh giá người dùng về công cụ Micraspis được tổ chức như thế nào và kết quả ra sao?
Tác giả đã tiến hành khảo sát trên 161 lập trình viên bằng bảng câu hỏi theo thang đo Likert (5 mức độ). Đối tượng tham gia gồm sinh viên đại học, cao đẳng (tại 3 trường đại học, 1 trường cao đẳng) và các kỹ sư phần mềm (trong đó 19,3% là người có kinh nghiệm chuyên sâu về IoT tại 18 doanh nghiệp). Kết quả ghi nhận có ít nhất 65% người tham gia đồng ý hoặc rất đồng ý về tính hữu ích và khả năng hỗ trợ phát triển của công cụ.
5. Luận án giải quyết vấn đề tái sử dụng phần cứng và mã nguồn như thế nào?
Khung thức của luận án tách biệt hoàn toàn giữa mô hình thiết kế phần cứng và mô hình máy trạng thái của ứng dụng thông qua một tầng ánh xạ trung gian. Nhờ sự phân tách này, một thiết kế phần cứng có thể được sử dụng lại cho nhiều ứng dụng nghiệp vụ khác nhau và ngược lại, một quy trình ứng dụng có thể được ánh xạ để triển khai trên các thiết bị đeo tay có cấu hình phần cứng khác nhau nhưng cùng chung nguyên lý kiến trúc.
Kết luận
Luận án của nghiên cứu sinh Tôn Long Phước đã giải quyết bài toán tự động hóa phát triển phần mềm cho các thiết bị đeo tay trong hệ sinh thái Internet vạn vật thông qua việc kết hợp kỹ thuật mô hình hóa máy trạng thái với hệ thống tập luật ràng buộc. Nghiên cứu đã đề xuất thành công khung thức tổng quát dựa trên chuẩn MDA, tích hợp phương pháp kiểm chứng hình thức bằng ngôn ngữ Alloy để đảm bảo tính đúng đắn của mô hình đặc tả. Công cụ Micraspis được xây dựng và kiểm chứng thực nghiệm qua 161 người dùng cùng 6 bài toán mẫu, chứng minh khả năng sinh tự động trên 65% mã nguồn C++ hoàn thiện cho dòng vi điều khiển Arduino. Kết quả nghiên cứu đóng góp cả về mặt phương pháp luận kỹ nghệ phần mềm lẫn công cụ thực tiễn phục vụ đào tạo và phát triển ứng dụng IoT.
