Luận văn Thạc sĩ: Nghiên cứu phương pháp giải ràng buộc SMT và áp dụng để phát hiện lỗi tràn số cho mô hình Simulink

Trong bối cảnh cách mạng công nghiệp 4.0, các hệ thống nhúng ngày càng đóng vai trò thiết yếu, đặc biệt trong Internet of Things (IOT), đòi hỏi chất lượng và độ tin cậy cao. Tuy nhiên, một trong những thách thức nghiêm trọng là lỗi tràn số (overflow error), có thể dẫn đến sai lệch tính toán nghiêm trọng và rất khó phát hiện trong quá trình thực thi hệ thống. Phát hiện sớm các lỗi này là cực kỳ quan trọng để tránh chi phí sửa chữa đắt đỏ hoặc thu hồi sản phẩm. Luận văn này tập trung vào nghiên cứu và áp dụng phương pháp giải ràng buộc SMT (Satisfiability Modulo Theories), cụ thể là sử dụng công cụ Z3 Solver, để phát hiện hiệu quả lỗi tràn số trong các mô hình Simulink của hệ thống nhúng, nhằm nâng cao độ tin cậy và chất lượng phần mềm.

Các nhà nghiên cứu, kỹ sư phần mềm, và sinh viên chuyên ngành hệ thống nhúng, kỹ thuật máy tính, đặc biệt là những người làm việc với Matlab/Simulink và các công cụ kiểm chứng phần mềm.

Luận văn này trình bày một nghiên cứu chuyên sâu về phương pháp giải ràng buộc SMT nhằm giải quyết vấn đề quan trọng là phát hiện lỗi tràn số trong các mô hình Simulink của hệ thống nhúng. Mở đầu, luận văn khái quát về tầm quan trọng của hệ thống nhúng trong kỷ nguyên Cách mạng công nghiệp 4.0 và những rủi ro nghiêm trọng do lỗi tràn số gây ra, đặc biệt khi sử dụng các kiểu dữ liệu có giới hạn biểu diễn nhỏ. Phương pháp tiếp cận chính dựa trên việc kiểm chứng mô hình bằng cách chuyển đổi bài toán phát hiện lỗi tràn số thành bài toán thỏa mãn ràng buộc số. Trong phần phương pháp, luận văn đi sâu vào phân tích các nguyên nhân gây ra lỗi tràn số trong môi trường Matlab/Simulink và đề xuất cách biến đổi mô hình hệ thống nhúng thành các ràng buộc SMT tương ứng. Sau đó, các ràng buộc này được đưa vào một bộ giải SMT (SMT Solver), cụ thể là Z3 Solver của Microsoft, để kiểm tra tính thỏa mãn. Nếu bộ giải SMT tìm thấy một cấu hình đầu vào làm cho các ràng buộc bị vi phạm, điều đó có nghĩa là tồn tại lỗi tràn số trong mô hình. Giá trị ứng dụng của nghiên cứu này nằm ở khả năng cung cấp một công cụ hiệu quả và đáng tin cậy để tự động hóa quá trình phát hiện lỗi tràn số, giúp các nhà phát triển giảm thiểu đáng kể thời gian và công sức so với các phương pháp kiểm thử truyền thống vốn gặp khó khăn trong việc tạo ra các trường hợp kiểm thử phức tạp. Hàm ý của kết quả nghiên cứu là góp phần nâng cao chất lượng và độ an toàn cho các hệ thống nhúng, đặc biệt trong các ứng dụng yêu cầu tính chính xác cao, bằng cách tích hợp phương pháp kiểm chứng dựa trên SMT vào quy trình phát triển.