CHƯƠNG I: TỔNG QUAN 1. Hệ thống nhúng và vấn đề lỗi tràn số 1. Hệ thống nhúng Hệ thống nhúng là một hệ thống được tích hợp cả phần cứng và phần mềm phục vụ cho các bài toán chuyên dụng trong nhiều lĩnh vực công nghiệp, tự động hóa điều khiển, quan trắc và truyền thông. Hệ thống nhúng hiện diện khắp nơi trong thế giới hiện đại, ví dụ như: - Các hệ thống dẫn đường trong không lưu, hệ thống định vị toàn cầu, vệ tinh.
- Các thiết bị gia dụng: tủ lạnh, lò vi sóng, lò nướng,… - Các thiết bị kết nối mạng: router, hub, gateway,… - Các thiết bị văn phòng: máy photocopy, máy fax, máy in, máy scan,… - Các thiết bị y tế: máy thẩm thấu, máy điều hòa nhịp tim,… - Các máy trả lời tự động. - Dây chuyền sản xuất tự động trong công nghiệp, robots. Hình 1: Một số ví dụ điển hình về hệ thống nhúng Hệ thống này đòi hỏi độ ổn định và tự động hóa cao. Do sử dụng cho các nhiệm vụ chuyên biệt và được sản xuất với số lượng lớn nên chúng được thiết kế một cách tối ưu nhằm giảm thiểu kích thước cũng như giá thành sản xuất.
Độ phức tạp là khác nhau theo yêu cầu của công việc mà chúng đảm nhận, hệ thống nhúng có thể rất đơn giản với một vi điều khiển hoặc rất phức tạp với nhiều đơn vị, các thiết bị ngoại vi và mạng lưới được nằm gọn trong một lớp vỏ máy lớn. Các hệ thống nhúng bị giới hạn nhiều hơn về phần cứng và chức năng phần mềm so với máy tính cá nhân. Giới hạn phần cứng có thể bao gồm giới hạn về khả năng xử lý, tiêu thụ điện năng, bộ nhớ, chức năng phần cứng,… Còn giới hạn phần mềm thường liên quan đến việc hỗ trợ ít ứng dụng, ứng dụng bị thu gọn tính năng, không có hệ điều hành hoặc hệ điều hành có nhiều hạn chế. Tuy nhiên, ngày nay, những giới hạn này đã được khắc phục đáng kể bằng các hệ thống nhúng được thiết kế 4 phức tạp và đầy đủ tính năng hơn.
Phần mềm của hệ thống nhúng được lưu trữ trên các bộ nhớ ROM, Flash và được gọi là Firmware. Hệ thống nhúng được thiết kế để thực hiện một chức năng chuyên biệt nào đó. Đây là điểm khác biệt so với các hệ thống máy tính khác như máy tính cá nhân hoặc các siêu máy tính có thể thực hiện nhiều chức năng khác nhau với những phép tính phức tạp, chuyên dụng giúp nâng cao tính dễ sử dụng và tiết kiệm tài nguyên. Nhiều loại thiết bị nhúng có những yêu cầu rất cao về chất lượng, tính ổn định và độ tin cậy.
Lỗi của hệ thống nhúng có thể gây ra tai nạn khủng khiếp: Hệ thống điều khiển máy bay, tên lửa, hệ thống điều khiển động cơ ô tô…Lỗi trên hệ thống nhúng có thể không sửa được (vd: vệ tinh nhân tạo), nếu sửa được thì chi phí cũng rất cao (thu hồi sản phẩm hoặc thiết kế lại toàn bộ…) Vì vậy việc phát triển hệ thống nhúng yêu cầu quy trình kiểm tra - kiểm thử rất cẩn thận. Vấn đề lỗi tràn số Khi sử dụng dữ liệu trên hệ thống nhúng, dữ liệu sẽ được mã hoá về dạng nhị phân (bit). Trong Matlab [7], một biến dạng số khi được khai báo sẽ phải khai báo cùng kiểu dữ liệu, máy tính sẽ cấp cho biến đó một số lượng bit nhất định để lưu trữ, ví dụ : int8 – 8 bit, int16 – 16 bit, … nên giá trị của số mà những biến này biểu diễn được sẽ có giới hạn : [-128, 127] với 8 bit, [-32768, 32767] với 16 bit, … Sử dụng kiểu dữ liệu hợp lý sẽ giúp mô hình tiết kiệm bộ nhớ và tối ưu tốc độ, tuy nhiên việc lựa chọn kiểu dữ liệu đòi hỏi người lập trình có kinh nghiệm, lường được hết trước các khả năng có thể xảy ra, nếu không, khi cố gắng tạo một giá trị số nằm ngoài của phạm vi có thể được biểu diễn bằng một số chữ số nhất định - cao hơn giá trị tối đa hoặc thấp hơn giá trị nhỏ nhất có thể biểu diễn, hiện tượng tràn số sẽ xảy ra. Hậu quả phổ biến nhất của tràn là các chữ số có nghĩa nhỏ nhất có thể biểu diễn của kết quả được lưu trữ; kết quả được cho là bao quanh mức tối đa (tức là modulo một lũy thừa của cơ số , thường là hai trong các máy tính hiện đại, nhưng đôi khi là mười hoặc một cơ số khác).
Vấn đề này ảnh hưởng đến độ tin cậy và bảo mật của mô hình. Vì vậy việc kiểm soát để hệ thống không bị tràn số là quan trọng, đặc biệt trong các hệ thống nhúng thường cần dùng các kiểu dữ liệu với khả năng biểu diễn giá trị nhỏ (8 bit, 16 bit). Tuy nhiên, lỗi tràn số thường khó có thể phát hiện. Lý do là lỗi tràn số thường xảy ra sau một chuỗi các tính toán số học trong quá trình hệ thống thực hiện, chứ không phải chỉ xảy ra ngay từ input đầu vào.
Việc kiểm tra để phát hiện lỗi tràn số cũng gặp thách thức lớn vì phải nghĩ ra tất cả các trường hợp có thể dẫn tới tràn số. Mô hình hệ thống nhúng MATLAB/Simulink Matlab (Matrix Laboratory) là một phần mềm khoa học được thiết kế để cung cấp việc tính toán số và hiển thị đồ họa bằng ngôn ngữ lập trình cấp cao. Matlab cung cấp các tính năng tương tác tuyệt vời cho phép người sử dụng thao tác dữ liệu linh 5 hoạt dưới dạng mảng ma trận để tính toán và quan sát. Các dữ liệu vào của Matlab có thể được nhập từ "Command line" hoặc từ "mfiles", trong đó tập lệnh được cho trước bởi Matlab.
Matlab cung cấp cho người dùng các toolbox tiêu chuẩn tùy chọn. Người dùng cũng có thể tạo ra các hộp công cụ riêng của mình gồm các "mfiles" được viết cho các ứng dụng cụ thể. Người dùng có thể sử dụng các tập tin trợ giúp của Matlab cho các chức năng và các lệnh liên quan với các toolbox có sẵn (dùng lệnh help). Ví dụ: Command Window: >> help plot Màn hình tiêu chuẩn sau khi khởi động Matlab: Hình 2: Màn hình tiêu chuẩn sau khi khởi động MATLAB Simulink [11] là một công cụ trong Matlab dùng để mô hình, mô phỏng và phân tích các hệ thống động với môi trường giao diện sử dụng bằng đồ họa.
Việc xây dựng mô hình được đơn giản hóa bằng các hoạt động nhấp chuột và kéo thả. Simulink bao gồm một bộ thư viện khối với các hộp công cụ toàn diện cho cả việc phân tích tuyến tính và phi tuyến. Simulink là một phần quan trọng của Matlab và có thể dễ dàng chuyển đổi qua lại trong quá trình phân tích, và vì vậy người dùng có thể tận dụng được ưu thế của cả hai môi trường. Để khởi động Simulink, click vào biểu tượng Simulink trên thanh công cụ hoặc sử dụng lệnh simulink trong Command Window: 6 Hình 3: Khởi động Simulink Giao diện khởi động của Simulink: Hình 4: Giao diện khởi động của Simulink Mô hình Simulink [2] bao gồm hai yếu tố chính: khối (block) và đường (line).
Khối là các đơn vị chức năng, được sử dụng để tạo, điều khiển và xuất tín hiệu. Các khối được kết nối bằng các đường cung cấp cơ chế truyền tín hiệu qua kết nối. Một khối có thể là một khối cha chứa các khối con khác, mỗi khối mô hình hóa một hệ 7 thống phụ hoặc chức năng phụ. Các khối được lấy từ các thư viện khối có sẵn (bao gồm các hàm chung như các toán tử cộng hoặc logic, nhưng cũng là các miền như logic mờ hoặc truyền thông mạng) và nhận một số tín hiệu đầu vào cụ thể mà từ đó tín hiệu đầu ra được tính toán.
Các mô hình Simulink bao gồm một tập các khối được kết nối bằng các tín hiệu xác định luồng dữ liệu. Nhìn chung, một mô hình Simulink nhận được một số luồng (các giá trị đầu vào vô hạn) bằng cách sử dụng các khối Inport và tạo ra một số luồng đầu ra được đại diện bởi các khối Outport. Simulink đóng một vai trò ngày càng quan trọng trong kỹ thuật hệ thống, và việc xác minh và xác nhận các mô hình Simulink đang trở nên quan trọng đối với người dùng. Phân loại blocks: Block đơn: là các block đơn không có trạng thái con bên trong, thường thay đổi giá trị output khi input thay đổi.
Ví dụ: relational (phép quan hệ), logic (phép logic), arithmetics (phép số học)… Delay block: là các block làm chậm giá trị input 1 khoảng thời gian. Có nhiều block thuộc loại này, ví dụ: UnitDelay, RateTransition,… SFunction: là các block được định nghĩa bởi người dùng thực hiện 1 tính năng/nhiệm vụ nhất định. Sfunction là một subsystem gồm nhiều block con hợp thành, và gồm các inputs và outputs tương ứng. Cách kết hợp blocks: có 2 cách kết hợp các block chính: tuần tự và lặp.
Với cách kết hợp tuần tự, dữ liệu đi từ block này sang block kia nhưng không tạo thành vòng lặp. Với cách kết hợp lặp, tồn tại 1 vòng lặp trong quá trình dữ liệu truyền trong mô hình. Lỗi tràn số trên MATLAB/Simulink Xét một ví dụ đơn giản, mô hình Simulink tính tổng của 2 số: Hình 5: Mô hình Simulink tính tổng hai số 8 Giá trị của Variable 1, Variable 2 và Add đều để kiểu uint8, có giới hạn từ 0- 255, vì vậy khi không xảy ra lỗi tràn số (tổng của hai biến không vượt quá 255) thì kết quả sẽ ra đúng. Tuy nhiên, khi tổng của hai biến vượt quá 255, kết quả không còn chính xác nữa.
Hình 6: Kết quả khi xảy ra tràn số Kết quả chính xác là 310 nhưng mô hình lại đưa ra là 54. Nguyên nhân chính là do tràn số. Khi thực hiện tính toán, Simulink đổi các giá trị input ra nhị phân sau đó tính tổng: 21010 = 101111112, 10010 = 11001002 => 101111112 + 11001002 = 1001101102. 1001101102 = 31010 có tới 9 bit, vượt quá giới hạn lưu trữ của kiểu int8, nên kết quả sẽ bỏ đi bit đầu tiên 00110110 = 54.
Lỗi tràn số trong Matlab/Simulink rất dễ xảy ra nên việc phát hiện vô cùng quan trọng để đảm bảo mô hình hoạt động chính xác. Tuy nhiên Matlab/Simulink lại chưa hỗ trợ tính năng này. Vì vậy luận văn đã sử dụng ràng buộc SMT để giải quyết vấn đề này. Mô hình Matlab/Simulink sẽ được encode thành định dạng SMT sau dó dùng một SMT Solver để kiểm tra SAT/unSAT hay chính là lỗi tràn số của mô hình.