Tổng quan nghiên cứu

Trong bối cảnh cách mạng công nghiệp 4.0, các hệ thống nhúng đóng vai trò thiết yếu trong nhiều lĩnh vực như công nghiệp tự động hóa, y tế, giao thông và viễn thông. Theo ước tính, các hệ thống nhúng chiếm tỷ lệ lớn trong các thiết bị điện tử hiện đại, từ thiết bị gia dụng đến hệ thống điều khiển máy bay. Tuy nhiên, các hệ thống này thường gặp phải vấn đề lỗi tràn số (overflow), gây ảnh hưởng nghiêm trọng đến độ tin cậy và an toàn vận hành. Lỗi tràn số xảy ra khi giá trị số vượt quá giới hạn biểu diễn của kiểu dữ liệu, ví dụ như kiểu int8 chỉ biểu diễn được giá trị từ -128 đến 127. Việc phát hiện và kiểm chứng lỗi tràn số trong mô hình hệ thống nhúng là một thách thức lớn do tính phức tạp của các phép tính và giới hạn phần cứng.

Mục tiêu nghiên cứu của luận văn là phát triển phương pháp giải ràng buộc SMT (Satisfiability Modulo Theories) để phát hiện lỗi tràn số trong các mô hình hệ thống nhúng được xây dựng trên Matlab/Simulink. Nghiên cứu tập trung vào việc biến đổi mô hình Simulink thành các ràng buộc SMT, sử dụng bộ giải SMT Z3 của Microsoft để kiểm chứng tính thỏa mãn và phát hiện lỗi tràn số. Phạm vi nghiên cứu bao gồm các mô hình hệ thống nhúng đơn giản đến phức tạp, với các kiểu dữ liệu phổ biến như int8 và int16, thực hiện trong giai đoạn 2020-2021 tại Học viện Công nghệ Bưu chính Viễn thông.

Nghiên cứu có ý nghĩa quan trọng trong việc nâng cao độ tin cậy của hệ thống nhúng, giảm thiểu chi phí sửa chữa và thu hồi sản phẩm do lỗi tràn số, đồng thời góp phần phát triển các công cụ kiểm chứng tự động cho hệ thống nhúng trong công nghiệp và nghiên cứu khoa học.

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

Khung lý thuyết áp dụng

Luận văn dựa trên hai lý thuyết chính: lý thuyết hệ thống nhúng và lý thuyết giải ràng buộc SMT. Hệ thống nhúng được định nghĩa là hệ thống tích hợp phần cứng và phần mềm thực hiện chức năng chuyên biệt, với các giới hạn về bộ nhớ, xử lý và năng lượng. Lỗi tràn số là hiện tượng giá trị số vượt quá giới hạn biểu diễn của kiểu dữ liệu, gây sai lệch kết quả tính toán.

SMT là mở rộng của SAT (Satisfiability) trong logic vị từ cấp một, cho phép giải các bài toán thỏa mãn các ràng buộc logic và toán học phức tạp. Bộ giải SMT Z3 của Microsoft được sử dụng để kiểm tra tính thỏa mãn của các biểu thức logic được mã hóa từ mô hình Simulink. Các khái niệm chính bao gồm:

  • Block trong Simulink: Đơn vị chức năng trong mô hình, có thể là phép toán, so sánh, trễ thời gian, v.v.
  • Ràng buộc SMT: Biểu diễn các quan hệ giữa các biến đầu vào, đầu ra của block dưới dạng biểu thức logic.
  • Kiểm chứng lỗi tràn số: Xác định xem có tồn tại bộ giá trị đầu vào làm cho giá trị vượt quá giới hạn kiểu dữ liệu hay không.

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

Nguồn dữ liệu chính là các mô hình hệ thống nhúng được xây dựng trên Matlab/Simulink, bao gồm các mô hình Counter_harness, ControlSpeed_harness và SpeedCals_harness. Các mô hình này được lựa chọn dựa trên tính đại diện và mức độ phức tạp khác nhau.

Phương pháp nghiên cứu gồm các bước:

  1. Phân tích mô hình Simulink: Xác định các block có nguy cơ gây lỗi tràn số, chủ yếu là các block thuộc nhóm Math Operations.
  2. Biến đổi mô hình thành ràng buộc SMT: Mỗi block và bước thời gian được mã hóa thành các biến và hàm trong ngôn ngữ SMT-LIB, theo chuẩn SMT-LIB và sử dụng cú pháp tương tự Lisp.
  3. Sử dụng bộ giải SMT Z3: Giải các ràng buộc để kiểm tra tính thỏa mãn (SAT/UNSAT), từ đó phát hiện lỗi tràn số.
  4. Thực nghiệm và đánh giá: Thực hiện trên các mô hình thực tế với các khoảng giá trị đầu vào khác nhau, đánh giá kết quả phát hiện lỗi.

Cỡ mẫu nghiên cứu gồm 3 mô hình với các kiểu dữ liệu int8 và int16, thực hiện kiểm chứng trên các khoảng giá trị đầu vào [-10, 10], [-100, 100], [-256, 255]. Phương pháp chọn mẫu dựa trên tính đại diện và khả năng mô phỏng các tình huống lỗi tràn số thực tế. Thời gian nghiên cứu kéo dài trong năm 2021.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

  1. Phát hiện lỗi tràn số hiệu quả trên mô hình Counter_harness: Với kiểu dữ liệu int8 và khoảng giá trị đầu vào [-256, 255], hệ thống phát hiện lỗi tràn số thành công, trong khi với các khoảng nhỏ hơn [-10, 10] và [-100, 100] không phát hiện lỗi. Điều này chứng tỏ phương pháp có khả năng phát hiện lỗi khi giá trị vượt giới hạn kiểu dữ liệu.

  2. Mô hình ControlSpeed_harness có lỗi tràn số với cả int8 và int16: Kết quả thực nghiệm cho thấy lỗi tràn số xuất hiện ở tất cả các khoảng giá trị đầu vào thử nghiệm, phản ánh tính phức tạp và nguy cơ cao của mô hình này trong thực tế.

  3. Mô hình SpeedCals_harness cũng phát hiện lỗi tràn số với các kiểu dữ liệu và khoảng giá trị đầu vào khác nhau: Điều này khẳng định tính ứng dụng rộng rãi của phương pháp trong các mô hình hệ thống nhúng đa dạng.

  4. Hệ thống phát hiện lỗi tràn số cho phép xuất dữ liệu lỗi dưới dạng file Excel: Giúp người dùng dễ dàng kiểm thử lại và phân tích nguyên nhân lỗi, tăng tính thực tiễn của công cụ.

Thảo luận kết quả

Nguyên nhân chính của các lỗi tràn số là do các phép toán cộng, trừ, nhân trong các block Math Operations làm tăng giá trị vượt quá giới hạn kiểu dữ liệu. So sánh với các nghiên cứu trước đây, phương pháp sử dụng SMT Solver Z3 cho phép kiểm chứng tự động và chính xác hơn so với kiểm thử truyền thống, vốn chỉ giảm thiểu lỗi mà không thể khẳng định hệ thống không có lỗi.

Kết quả thực nghiệm được trình bày qua bảng kết quả và các ví dụ test case cụ thể, minh họa rõ ràng các giá trị vượt giới hạn. Biểu đồ phân bố giá trị đầu ra của các block có thể được sử dụng để trực quan hóa mức độ rủi ro tràn số theo từng bước thời gian.

Phương pháp này có ý nghĩa quan trọng trong việc nâng cao độ tin cậy của hệ thống nhúng, đặc biệt trong các ứng dụng yêu cầu an toàn cao như y tế, hàng không và công nghiệp tự động.

Đề xuất và khuyến nghị

  1. Tự động hóa mã hóa mô hình Simulink sang định dạng SMT: Phát triển công cụ hỗ trợ tự động chuyển đổi mô hình để giảm thiểu sai sót và tăng hiệu quả kiểm chứng, dự kiến hoàn thành trong 1-2 năm tới, do các nhóm nghiên cứu và phát triển phần mềm thực hiện.

  2. Mở rộng kiểm chứng cho các mô hình hệ thống nhúng phức tạp hơn: Áp dụng phương pháp cho các mô hình lớn, đa dạng hơn nhằm đánh giá khả năng mở rộng và hiệu quả thực tế, ưu tiên trong các dự án nghiên cứu tiếp theo.

  3. Tích hợp hệ thống phát hiện lỗi tràn số vào quy trình phát triển phần mềm nhúng: Đề xuất các doanh nghiệp và tổ chức phát triển hệ thống nhúng áp dụng để nâng cao chất lượng sản phẩm, giảm thiểu chi phí sửa chữa và thu hồi.

  4. Đào tạo và nâng cao nhận thức về lỗi tràn số trong cộng đồng kỹ sư phát triển hệ thống nhúng: Tổ chức các khóa học, hội thảo nhằm phổ biến kiến thức và công cụ kiểm chứng tự động, giúp giảm thiểu lỗi trong thiết kế và triển khai.

Đối tượng nên tham khảo luận văn

  1. Kỹ sư phát triển hệ thống nhúng: Nắm bắt phương pháp kiểm chứng lỗi tràn số tự động, áp dụng vào thiết kế và kiểm thử sản phẩm nhằm nâng cao độ tin cậy.

  2. Nhà nghiên cứu và giảng viên trong lĩnh vực kỹ thuật phần mềm và hệ thống nhúng: Tham khảo phương pháp giải ràng buộc SMT và ứng dụng thực tiễn trong kiểm chứng mô hình Simulink.

  3. Doanh nghiệp phát triển phần mềm và phần cứng nhúng: Áp dụng công cụ và quy trình kiểm chứng để giảm thiểu rủi ro lỗi tràn số, tiết kiệm chi phí bảo trì và nâng cao chất lượng sản phẩm.

  4. Sinh viên và học viên cao học chuyên ngành hệ thống thông tin và kỹ thuật phần mềm: Học tập phương pháp nghiên cứu, kỹ thuật kiểm chứng tự động và ứng dụng SMT trong thực tế.

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

  1. Phương pháp SMT có thể áp dụng cho các mô hình nhúng phức tạp như thế nào?
    Phương pháp có thể mở rộng cho các mô hình phức tạp bằng cách tăng số bước trải mô hình (k) và tối ưu hóa mã hóa SMT. Ví dụ, các mô hình công nghiệp lớn có thể được kiểm chứng từng phần hoặc theo module.

  2. Lỗi tràn số có thể được phát hiện hoàn toàn bằng SMT không?
    SMT giúp phát hiện lỗi tràn số trong phạm vi mô hình và ràng buộc đã mã hóa. Tuy nhiên, các lỗi phát sinh ngoài mô hình hoặc do phần cứng thực tế cần kết hợp thêm kiểm thử thực nghiệm.

  3. Có thể tự động hóa toàn bộ quy trình từ Simulink sang SMT không?
    Hiện tại, việc mã hóa còn thủ công hoặc bán tự động. Luận văn đề xuất phát triển công cụ tự động hóa để tăng hiệu quả và giảm sai sót.

  4. Phương pháp này có phù hợp với các hệ thống nhúng sử dụng kiểu dữ liệu khác không?
    Có, phương pháp có thể điều chỉnh ràng buộc SMT cho các kiểu dữ liệu khác nhau, miễn là giới hạn biểu diễn được xác định rõ.

  5. Làm thế nào để sử dụng kết quả phát hiện lỗi tràn số trong thực tế?
    Kết quả có thể xuất ra file Excel chứa giá trị gây lỗi, dùng để kiểm thử lại hoặc điều chỉnh thiết kế mô hình nhằm loại bỏ lỗi trước khi triển khai thực tế.

Kết luận

  • Luận văn đã giới thiệu và phân tích chi tiết về hệ thống nhúng, lỗi tràn số và tầm quan trọng của việc phát hiện lỗi này trong mô hình Matlab/Simulink.
  • Phương pháp giải ràng buộc SMT và ứng dụng bộ giải Z3 được triển khai thành công để kiểm chứng lỗi tràn số trong các mô hình hệ thống nhúng.
  • Hệ thống phát hiện lỗi tràn số được xây dựng và thử nghiệm trên ba mô hình thực tế, cho kết quả chính xác và khả năng phát hiện lỗi hiệu quả.
  • Kết quả nghiên cứu góp phần nâng cao độ tin cậy và chất lượng của hệ thống nhúng, đồng thời mở ra hướng phát triển công cụ kiểm chứng tự động.
  • Hướng phát triển tiếp theo là tự động hóa mã hóa mô hình và mở rộng kiểm chứng cho các mô hình phức tạp hơn, nhằm ứng dụng rộng rãi trong công nghiệp và nghiên cứu.

Để nâng cao chất lượng hệ thống nhúng của bạn, hãy áp dụng phương pháp kiểm chứng lỗi tràn số dựa trên SMT và bộ giải Z3 ngay hôm nay!