Phát hiện lỗi tràn số trên mô hình hệ thống nhúng sử dụng phương pháp phân tích tĩnh

Bài viết Phát hiện lỗi tràn số trên mô hình hệ thống nhúng sử dụng phương pháp phân tích tĩnh đề xuất một phương pháp phát hiện lỗi tràn số cho các mô hình hệ thống nhúng dựa trên phương pháp phân tích tĩnh (static analysis) kết hợp với công cụ giải các ràng buộc SMT.
Nội dung trích xuất từ tài liệu:
Phát hiện lỗi tràn số trên mô hình hệ thống nhúng sử dụng phương pháp phân tích tĩnh Đỗ Thị Bích Ngọc PHÁT HIỆN LỖI TRÀN SỐ TRÊN MÔ HÌNH HỆ THỐNG NHÚNG SỬ DỤNG PHƯƠNG PHÁP PHÂN TÍCH TĨNH Đỗ Thị Bích Ngọc Học Viện Công Nghệ Bưu Chính Viễn Thông + Tóm tắt: Ngày nay, các hệ thống nhúng đòi hỏi tính an tràn số được cần được kiểm tra, đánh giá thường xuyên. toàn ngày cao, bên cạnh độ phức tạp cũng tăng theo. Vì Lỗi tràn số (number overflow) vậy, phân tích, đánh giá ngay từ mô hình hệ thống nhúng đã và đang thu hút sự quan tâm của cả giới nghiên cứu và Lỗi tràn số xảy ra khi giá trị số trong hệ thống vượt quá công nghiệp. Trong đó, việc phát hiện nguy cơ lỗi tràn số khả năng biểu diễn như trong thiết kế. Ví dụ số integer 8 trong các hệ thống nhúng là quan trọng và cần thiết vì nó bit chỉ có thể biểu diễn giá trị lớn nhất là 28 -1 = 255, trường có thể dẫn tới sai lệch nghiêm trọng trong hệ thống. Lỗi hợp số lớn hơn sẽ vượt quá khả năng biểu diễn. Lỗi tràn số tràn số có thể xảy ra do kiểu dữ liệu trong các hệ thống có dẫn tới hệ thống tính toán sai lệch nghiêm trọng. Một số nhúng thường bị giới hạn số bít. Thêm vào đó, các tính toán ví dụ về lỗi tràn số sau đây cho thấy tầm nghiêm trọng của bên trong hệ thống có thể dẫn tới các giá trị quá lớn so với chúng: phạm vi biểu diễn. Bài báo này đề xuất một phương pháp - Vào tháng 8/2016, một máy casino ở Resorts World phát hiện lỗi tràn số cho các mô hình hệ thống nhúng dựa Casino đã in 1 giải thưởng trị giá $42,949,672.76 do trên phương pháp phân tích tĩnh (static analysis) kết hợp lỗi tràn số. Phía Casino về sau đã xảy ra kiện tụng với công cụ giải các ràng buộc SMT. với khách hàng với giải thích là giải thưởng lớn nhất Từ khoá: ràng buộc SMT, mô hình hệ thống nhúng, lỗi chỉ có $10.000, bất kì giải thưởng nào lớn hơn là do tràn số, MATLAB/Simulink, phân tích tĩnh. lỗi của hệ thống.[1] - Vào tháng 6/1996, tên lửa Ariane 5 đã phát nổ sau I. GIỚI THIỆU khi được phóng 37 giây, gây thiệt hại 370 triệu $. Hệ thống nhúng Một lỗi tràn số đã xảy ra khi chuyển đổi số 64 bit sang số 16 bit dẫn tới điều khiển bị sai lêch. [2] Hệ thống nhúng đang phát triển mạnh mẽ và ngày càng đóng vai trò quan trọng trong cuộc sống của con người. Lỗi Vì vậy việc kiểm soát để hệ thống không bị tràn số là của hệ thống nhúng có thể gây ra tai nạn khủng khiếp, đặc quan trọng, đặc biệt trong các hệ thống cần dùng các kiểu biệt là các hệ thống điều khiển máy bay, tên lửa, hệ thống dữ liệu với khả năng biểu diễn giá trị nhỏ (8 bit, 16 bit). điều khiển động cơ ô tô... Vì vậy, nhiều hệ thống nhúng có Lỗi tràn số thường khó có thể phát hiện. Lý do là lỗi yêu cầu cao về chất lượng, tính ổn định và độ tin cậy. Bên tràn số thường xảy ra sau một chuỗi các tính toán số học cạnh đó, lỗi trên hệ thống nhúng có thể không sửa được, trong quá trình hệ thống thực hiện, chứ không phải chỉ xảy nếu sửa được thì chi phí cũng rất cao, phải thu hồi sản phẩm ra ngay từ input đầu vào. Việc kiểm thử để phát hiện lỗi hoặc thiết kế lại toàn bộ. Đó là lý do các công cụ hỗ trợ tràn số cũng gặp thách thức lớn vì phải nghĩ ra các bộ dữ thiết kế mô hình các hệ thống nhúng được áp dụng ngày liệu để có thể dẫn tới các giá trị tràn số. càng nhiều. Việc thiết kế mô hình hệ thống nhúng trên các công cụ trước khi thiết kế mẫu thật là cần thiết để dễ dàng Một số phương pháp phổ biến được dùng để phát hiện phát hiện, sửa lỗi cũng như chỉnh sửa thiết kế nhằm đảm lỗi tràn số: bảo chất lượng. Có nhiều nghiên cứu, công cụ hỗ trợ việc Phân tích tĩnh (static analysis): đây là một phương pháp đánh giá, kiểm tra các mô hình các hệ thống nhúng hiệu quả để phát hiện lỗi tràn số một cách tự động thông [7,8,9,10,13,14]. Trong các loại lỗi của hệ thống nhúng, lỗi qua phân tích các luồng dữ liệu hoặc áp dụng các kĩ thuật dựa trên ràng buộc (constraint-based techinque) [3,4,6]. Tác giả liên hệ: Đỗ Thị Bích Ngọc, ...