Nghiên cứu hình thức đồng kiểm tra hệ thống sử dụng giao thức LIN (Local Interconnect Network)

Tài liệu phân tích, đặc tính hóa lưu lượng các dịch vụ đa phương tiện trong mạng IMS 3G. Đề xuất mô hình QoE nhằm tối ưu trải nghiệm người dùng.

• Tác giả: Nguyễn Khắc Thành
• Người hướng dẫn: TS. Nguyễn Đức Minh
• Trường học: Trường Đại học Bách khoa Hà Nội
• Chuyên ngành: Kỹ thuật truyền thông
• Đề tài: Nghiên cứu hình thức đóng kiểm tra hệ thống sử dụng giao thức LIN (Local Interconnect Network)
• Loại tài liệu: Luận văn thạc sĩ kỹ thuật
• Năm xuất bản: 2014
• Địa điểm: Hà Nội

Tóm tắt

I. Giới thiệu về Kiểm tra Hệ thống Dùng Giao thức LIN

Giao thức LIN (Local Interconnect Network) là một tiêu chuẩn truyền thông được phát triển để kết nối các thiết bị điện tử trong các hệ thống tự động hóa, đặc biệt là trong ngành công nghiệp ô tô. Luận văn này tập trung vào kiểm tra hệ thống sử dụng giao thức LIN thông qua các phương pháp kiểm tra hình thức. Nghiên cứu được thực hiện tại Trường Đại học Bách Khoa Hà Nội, chuyên ngành Kỹ thuật Truyền thông, nhằm xây dựng khuôn khổ kiểm tra mô hình cụ thể cho node chủ LIN. Phương pháp này đảm bảo tính chính xác và an toàn của hệ thống truyền thông, giảm thiểu lỗi phần mềm và phần cứng trong quá trình triển khai.

1.1. Khái niệm Giao thức LIN

Giao thức LIN là một giao thức truyền thông nối tiếp được thiết kế để thay thế các hệ thống dây dò phức tạp. LIN hoạt động với tốc độ truyền thấp, tiêu thụ năng lượng thấp và chi phí triển khai hạ. Giao thức này sử dụng kiến trúc master-slave, trong đó một node chủ điều khiển việc truyền dữ liệu và các node phụ phản hồi. Các khung dữ liệu được truyền qua bus LIN với cấu trúc chuẩn, bao gồm trường đồng bộ, ID được bảo vệ, dữ liệu và checksum.

1.2. Tầm quan trọng của Kiểm tra Hình thức

Kiểm tra hình thức là quy trình xác minh tính đúng đắn của hệ thống thông qua các phương pháp toán học. Trong bối cảnh hệ thống LIN, kiểm tra hình thức giúp phát hiện lỗi tiềm ẩn trong node chủ LIN và các thành phần phần mềm/phần cứng khác. Phương pháp này đặc biệt quan trọng để đảm bảo an toàn và độ tin cậy của các ứng dụng thực tế.

II. Phương pháp Kiểm tra Hình thức Dùng Trừu tượng ITL

Luận văn đề xuất sử dụng phương pháp trừu tượng ITL (Intermediate Testing Language) để kiểm tra mô hình cụ thể của node chủ LIN. Phương pháp này bao gồm các bước chính: phân tích chương trình, trích xuất Control Flow Graph (CFG), xây dựng Concrete Execution Graph (CEG), và cuối cùng tạo ra Finite State Machine (FSM) của các thuộc tính. Khuôn khổ CEGAR (Counterexample Guided Abstraction Refinement) được áp dụng để tinh chỉnh mô hình trừu tượng và loại bỏ các lỗi giả. Cách tiếp cận này cho phép kiểm tra hệ thống một cách toàn diện và hiệu quả.

2.1. Quy trình Trích xuất Mô hình Cụ thể

Quy trình bắt đầu bằng phân tích chương trình C của trình điều khiển thiết bị LIN. Từ mã nguồn, các công cụ tạo ra Control Flow Graph mô tả luồng điều khiển. Tiếp theo, Concrete Execution Graph được hình thành để biểu diễn tất cả các đường thực thi có thể. Các thuộc tính cần kiểm tra được định nghĩa dựa trên CFG và ánh xạ thành biểu đồ thuộc tính, cuối cùng chuyển đổi thành Property FSM.

2.2. Công cụ và Thành phần Kiểm tra

Thành phần phần cứng của node chủ LIN bao gồm CPU Aquarius, bộ nhớ RAM/ROM, UART, và IRQCTL. Các công cụ kiểm thử được phát triển để hỗ trợ quá trình kiểm tra mô hình cụ thể, bao gồm trích xuất thuộc tính, xây dựng mô hình, và kiểm tra tính thỏa mãn. Các mẫu thuộc tính điển hình như 'start_new_frame' và 'reset' được sử dụng để xác thực hành vi của node chủ LIN.

III. Kiểm tra Thuộc tính của Node Chủ LIN

Các thuộc tính node chủ LIN được xác định để đảm bảo hành vi chính xác của hệ thống. Luận văn tập trung vào kiểm tra các thuộc tính quan trọng như khởi động khung mới, reset hệ thống, và quản lý trạng thái. Sử dụng phương pháp kiểm tra mô hình, các thuộc tính này được ánh xạ vào các đồ thị thuộc tính và chuyển đổi thành FSM thuộc tính. Mỗi thuộc tính được kiểm tra độc lập để đảm bảo không có xung đột và tất cả các điều kiện được đáp ứng. Cách tiếp cận này giúp kiểm tra hệ thống LIN một cách toàn diện và có hệ thống.

3.1. Định nghĩa và Mô hình Hóa Thuộc tính

Thuộc tính của node chủ LIN được định nghĩa dựa trên yêu cầu kỹ thuật của giao thức LIN. Các mẫu thuộc tính điển hình bao gồm những đặc tính liên quan đến khung dữ liệu, đồng bộ hóa, và quản lý trạng thái. Mỗi thuộc tính được mô hình hóa thành FSM, với các trạng thái và chuyển dịch tương ứng với hành vi mong đợi. Tập hợp thuộc tính được trừu tượng hóa dựa trên ITL để hỗ trợ quá trình kiểm tra tự động.

3.2. Xây dựng Đồ thị Thuộc tính

Đồ thị thuộc tính của node chủ LIN được xây dựng từ tập hợp các thuộc tính đã định nghĩa. Mỗi đỉnh trong đồ thị thuộc tính biểu diễn một trạng thái cụ thể, và các cạnh thể hiện các chuyển dịch giữa các trạng thái. Đồ thị này cho phép các công cụ kiểm tra tự động xác minh liệu node chủ LIN có tuân theo tất cả các thuộc tính định nghĩa hay không. Quá trình này giúp phát hiện các lỗi logic và đảm bảo tính chính xác.

IV. Kết quả và Ứng dụng Thực tiễn của Kiểm tra Hệ thống LIN

Luận văn trình bày các kết quả kiểm tra của hệ thống LIN sử dụng khuôn khổ kiểm tra hình thức được phát triển. Các thử nghiệm được thực hiện trên node chủ LIN với các tình huống khác nhau, bao gồm truyền dữ liệu bình thường, xử lý lỗi, và reset hệ thống. Kết quả cho thấy phương pháp này kiểm tra hệ thống một cách hiệu quả và phát hiện được các lỗi tiềm ẩn. Ứng dụng thực tiễn của nghiên cứu này bao gồm kiểm tra phần mềm điều khiển thiết bị LIN trong các ứng dụng công nghiệp và ô tô, đảm bảo an toàn và độ tin cậy cao.

4.1. Kết quả Kiểm tra và Phân tích

Các công cụ kiểm thử được áp dụng trên node chủ LIN để xác minh tính chính xác của mô hình. Kết quả kiểm tra cho thấy hệ thống đáp ứng được hầu hết các thuộc tính định nghĩa. Trong quá trình kiểm tra, một số counterexample được phát hiện, chỉ ra các đường thực thi không mong muốn. Các lỗi này được phân tích và mô hình được cải tiến bằng cách sử dụng CEGAR framework. Quá trình lặp lại này giúp loại bỏ lỗi giả và xác thực các lỗi thực sự.

4.2. Ứng dụng và Hướng phát triển Tương lai

Phương pháp kiểm tra hệ thống LIN được phát triển có thể áp dụng cho các hệ thống nhúng khác sử dụng giao thức truyền thông tương tự. Khuôn khổ kiểm tra hình thức này có tiềm năng được mở rộng để hỗ trợ kiểm tra phần mềm/phần cứng kết hợp (HW/SW). Hướng phát triển tương lai bao gồm tối ưu hóa công cụ kiểm thử, hỗ trợ các giao thức mới, và tích hợp vào quy trình phát triển phần mềm thực tế.

Trích đoạn nội dung tài liệu

BỘ GIÁO DỤC VÀ ĐÀO TẠO 'TRƯỜNG ĐẠI HỌC BÁCH KHOA LIA NOL NGUYÊN KHÁC THÀNH NGHIÊN CỨU HÌNH THỨC ĐÓNG KIỂM TRA HỆ THÔNG sU DUNG GIAO THUC LIN (LOCAT. INTERCONNECT NETWORK) Chuyên ngành: Kỹ thuật truyền thông LUẬN VĂN THẠC SĨ KỸ THUẬT KỸ THUẬT TRUYỂN THÔNG NGƯỜI HƯỚNG DẪN KHOA HỌC TS. NGUYEN ĐỨC MINIL HÀ NỘI —2014 Luận văn thạc sĩ kỹ thuật Kỹ thuật truyền thông, LOT CAM BOAN Tôi tên: Nguyễn Khắc Thành Lớp: KT) [-2011B Đơn vị: Viện Điện tử - Viễn thông — Trường Đại học Bách khoa Trà Nội Để tài luận văn của tôi là: Nghiên cứu hình thức đẳng kiểm tra hệ thẳng ste dung giao thitc LIN (Local Interconnect Netwark). Tôi xi cam đoan nội dụng cua luận văn hoàn toản do tối tự từm hiểu và nghiên cứu, không có sự sao chép bắt cứ tải liệu nào, mọi tải liệu sử dụng, dựa trên cơ sở tham khảo để tìm hiểu thêm vấn đề Nếu phát hiện ra bất cứ sự sao chép nào.

Tôi xin hoàn toản chịu trách nhiệm trước hội dẳng kỹ luật của Nhà trường, Hà Nội, 30 tháng 03 năm 2014 Ky tén Nguyễn Khắc Thành. Nguyễn Khắc Thành CB110908 KTTT2 Luan văn thạc sĩ kỹ thuật LOT CAM ON Trước hết, em xin gửi lời oám ơn sầu sắc tới oáo thây cô giáo trong trường Pai hoc Bach Khoa Ha Ndi noi chung và các thày cô trong Viện Điện Tử - Viên Thông, Viện đào tạo sau đại học nói riêng dã tận tỉnh giảng, dạy, cho em những kién thức và kinh nghiệm quý báu trong thời gian học vừa qua Em xin gửi lời cảm ơu đến TS. Nguyễn Đức Minh, giảng viên bộ môn Xứ lý số tin hiệu, Viện Điện Tử - Viễn Thông, trưởng Đại học Bách Khoa Hà Nội đã tận tình giúp đỡ, hướng dẫn em trong suốt quá trình thục hiện hiận văn nảy, Cuối củng, em xin gửi lời cảm ơn chân thánh tới gia định, bạn bẻ đã động, viên, chăm sóc, đèng gớp ÿ kiến và giúp đỡ em trong quá trình học tập, nghiên clu và hoàn thành luân văn Hà Nội, ngày 30 thủng 3 năm 2014 Nguyễn Khắc Thành Sinh viên lớp KTTT2 — K2011B Viện Điện Tử - Viễn Thông Trường Dai hoc Bach Khoa Hà Nội Neuyén Khic ‘Thanh CB110908 KITT Luận văn thạc sĩ kỹ thuật Kỹ thuật truyền thông, Tình 1.20 May trạng thái hữu hạn của trình điều khiển thất bị LTN 33 linh 2.1: Sơ đồ khối của nođe chủ LIN. AO Tình 22: Sơ đồ RTL của Aquarius Tình 3.3: Sơ đỗ khối ci core CPU Aquarius Hinh 2.3 Sơ đỗ RTL, của bộ nhớ.

nen eeeeeeriee Hình 2.5: Ảnh xạ địa chỉ của RAM và ROM trên Aquarius Tình 26 Sơ dễ RTL, của UART Hinh 3.7 Sơ để RTL của IRQCTL.8: Quá trình từ chương trình C đến chương trình đisassembly.9: Chương trình Œ.10: Chương trình assembly của chương trinh Ơ.11: CEG của chương trình tách rời của chương trình C đơn giản Hinh 2.12: Tình chất giả.13: Tinh chat that.14: Một phân của hàm chính của trình điều khiển thiết bị LIN Tình 3.15: Chương trình lách rời của LTN trình điều khiến thiết bị Tĩinh 3.16 CTG của node chủ LIN được hình thành đựa trên CEG Tình2.17: Một mẫu tính chất của node chủ LTN.18: Chia một chuyển dỏi dài thành 4 chuyển dồi ngắn.19: Khuên khổ đồng kiểm tra hình thứe mô hình eụ thẻ của node chủ LIN. Thuộc tính star,_new_frame Hình 3.Bộ phản của CEG cho thude tính khung mới khởi dộng. MacroITL cpu at Label26 In main sh. Một đỉnh trong CBG anh xa hai node trên biểu đỗ thuộc tính Hinh 3.

Thuộc tỉnh reset của node chủ LAN.6 Xây dựng đề thị thuộc tính từ tập hợp thuộc tính Hình3. Đỏ thí thuộc tỉnh của noẻe chủ LIN. Từ đỏ thị thuộc tính đến rõ FSM thuộc tỉnh. PFSMir Nguyễn Khắc hành CBI10908 KTTT2 Luận văn thạc sĩ kỹ thuật Kỹ thuật truyền thông, DANH MỤC BẰNG Bang 1.1: Cáo kỹ thuật kiếm tra cho HW.

SW, HW/SW Tảng 4. Những công cụ trong kiểm thử mô hình cụ thể cửa nođde chủ LTN. Những thuộc tỉnh của Mồ hình Cụ thể của node chủ LIN. Tập thuộc tính của node chủ LIN được trừu tượng hóa đựa trên ITL 107 Bang 4.4 Số biến trạng thái của mỗi mô dụn.

Những thuộc tính dải, chung,. -Ö112 DANH MỤC HÌNH VẼ linh 1.1 Luéng thiết kẻ hệ thông phần cửng/phản mểm.2 So dé khéi hé thing Hardware/Software ws Hinh 1.3 Kiểm tra bình thức .4: Mô hình mạch lặp của bộ mã hóa TSM cho IMC .5: Counterexample Guided Abstraction Refinement Framework.6: CEGAR kết hợp với trữu tượng xác nhận trong kiểm tra phẩn mỗẫm THỉnh 1.?: Mô hình đồng mô phỏng không đồng nhất.TN voi] node master va 2 tarde slave.9: Kiến trúc layer của một node LIN Hinh.10: Giao tiếp điển hình trên bus LIN qua các khưng Tình 1.11: Cầu trắc khung Hinh.12 Câu trúc của một trường byte.13: Trường ngắt đồng bộ. co crireeer Hình. 114 Trường động bộ.15: ID được bảo vệ.16: Tám byte dữ liệu trong một khung, Hình.17 Lịch trình LIN và khe khung,.18: Một ví dụ về chuyên giao khuig.

cọc rereerrerrrrrre Tình 1.L9: Các lớp trong triển khai phần mềm của TTN Nguyễn Khắc Thành CB110908 KTTT2 Luận văn thạc sĩ kỹ thuật Kỹ thuật truyền thông, 2.2 Thành phần phần cứng của node chủ LTN.2 Kiểm thứ hình thức của mô hình thực tế.21 Thântáchchương trình.4 Các mẫu tinh chất đựa trên CFG dành cho mõ hình cụ thế cũa node. Khuôn khổ kiểm tra mô hình cụ thể của Node chủ LIN.69 CHƯƠNG 5: KIỀM TRA HỈNH THỨC CỦA THỰC HIỆN LIN DUA TREN PHUONG PHAP TRUU TUGNG IIL. Từ tập hợp thuộc tính tới đỏ thị thuộc tính 27S 311 Đổthi thuộc tinh.2 Đỏ thị thuộc tỉnh của node chủ LIN.2 _ Từ biểu dễ thuộc tỉnh dến mô hình máy hữu han trang thâi,. co 88 3⁄21 Máy hữu hạn trạng thái.2 PESM của node chủ LIN (Node chủ LIN) - 292 3.

TừPFSM đến mô hình trừu tượng 94 3.4 Kiểm tra hình thức của nodc chủ LTN với trừu tượng dựa trêu ITL. Sự triển khai của node chủ LIN với trừu tượng dựa trên LTL.2 Kiém tra chính thức của mô hình trùu tượng 97 3. Framework ciia déng kiém tra hinh thite cia triển khai LIN đựa vào những thuộc tính đài, chưng - 100 CHƯƠNG 4: KÉT QUÁ VÀ PHÂN TÍCH KÉT QUÁ THÍ NGHIỆM. Đểng kiểm tra hình thức cho mô hình cụ thể của nodc chả LTN.2 Déng kiểm tra hình thức node chủ LIN trữu tượng hóa đựa trên ITL.

Kiểm thủ chính thức của những thuộc tính đài và chung véi node cht LIN trừu tượng hóa dựa trên TT. ~ - 108 CHƯƠNG 5: KẾT LUẬN VÀ CÁC NGHIÊNNCỨU SAU NÀY.2 So sánh với cácnghiên cócứa trước Ổầy. Cée nghién ctu tiép theo - 116 TAI LIEU THAM KHAO Neuyén Khic ‘Thanh CB110908 KTTT2 Luận văn thạc sĩ kỹ thuật Kỹ thuật truyền thông, DANH MỤC BẰNG Bang 1.1: Cáo kỹ thuật kiếm tra cho HW. SW, HW/SW Tảng 4.

Những công cụ trong kiểm thử mô hình cụ thể cửa nođde chủ LTN. Những thuộc tỉnh của Mồ hình Cụ thể của node chủ LIN. Tập thuộc tính của node chủ LIN được trừu tượng hóa đựa trên ITL 107 Bang 4.4 Số biến trạng thái của mỗi mô dụn. Những thuộc tính dải, chung,.

-Ö112 DANH MỤC HÌNH VẼ linh 1.1 Luéng thiết kẻ hệ thông phần cửng/phản mểm.2 So dé khéi hé thing Hardware/Software ws Hinh 1.3 Kiểm tra bình thức .4: Mô hình mạch lặp của bộ mã hóa TSM cho IMC .5: Counterexample Guided Abstraction Refinement Framework.6: CEGAR kết hợp với trữu tượng xác nhận trong kiểm tra phẩn mỗẫm THỉnh 1.?: Mô hình đồng mô phỏng không đồng nhất.TN voi] node master va 2 tarde slave.9: Kiến trúc layer của một node LIN Hinh.10: Giao tiếp điển hình trên bus LIN qua các khưng Tình 1.11: Cầu trắc khung Hinh.12 Câu trúc của một trường byte.13: Trường ngắt đồng bộ. co crireeer Hình. 114 Trường động bộ.15: ID được bảo vệ.16: Tám byte dữ liệu trong một khung, Hình.17 Lịch trình LIN và khe khung,.18: Một ví dụ về chuyên giao khuig. cọc rereerrerrrrrre Tình 1.L9: Các lớp trong triển khai phần mềm của TTN Nguyễn Khắc Thành CB110908 KTTT2 Luận văn thạc sĩ kỹ thuật Kỹ thuật truyền thông, Hình 3.

Sơ để khỏi của mô hình trừu tượng. Sơ để RTL của mỏ hình trữu tượng. Node cht LIN qua mô hình trừu tượng. Mội thuộc tính cụ thể đến mội thude tinh tri trong.

Framework cho déng kiéin tra hình thúc của node chu LIN dựa trêu. những thuộc tính đài, chưng. Biểu điển sơ để mạch của mô hình mạch tương tác thỏa man chiền dain của thuộc tỉnh. Một nhóm LIN - - - 109 Hình 4.

Một vi dụ của thuộc tính dải, chung trong node chủ LIN. Mẫu thuộc tỉnh cho thuộc tính olumig, đải.à--:: Seo EET Nguyễn Khắc Ihành CBI10908 KTTT2 Luận văn thạc sĩ kỹ thuật Kỹ thuật truyền thông, Hình 3. Sơ để khỏi của mô hình trừu tượng. Sơ để RTL của mỏ hình trữu tượng.

Node cht LIN qua mô hình trừu tượng. Mội thuộc tính cụ thể đến mội thude tinh tri trong. Framework cho déng kiéin tra hình thúc của node chu LIN dựa trêu. những thuộc tính đài, chưng.

Biểu điển sơ để mạch của mô hình mạch tương tác thỏa man chiền dain của thuộc tỉnh. Một nhóm LIN - - - 109 Hình 4. Một vi dụ của thuộc tính dải, chung trong node chủ LIN. Mẫu thuộc tỉnh cho thuộc tính olumig, đải.à--:: Seo EET Nguyễn Khắc Ihành CBI10908 KTTT2 Luan văn thạc sĩ kỹ thuật LOTMG DAU Kiểm thử giao thức phù hợp là một miễn chính của quá trình đối mới Hiểm.

xăng trong ngành công nghiệp kiếm thir System-on-Chip. Bén cạnh đó, đồng kiểm. thử hình thức hệ thống phản cing/phan mém la mét nhiệm vụ dây thách thức. Do đó, đồng kiếm thứ hình thức hệ thẳng phản cứng/phân mềm thực hiện một giao thức bus là một công việc ý nghấa.

Trong hiện vẫn mày, chúng lôi hướng tới đẳng kiểm: tra hình thức một node chủ LIN , node đỏ được thạc hiện giỗng như một hệ thông, phần cứng phẩn mềm Để vượt qua khoảng cách giữa kiểm tra phản cứng và phần mẻmn, một framework déng kiém ta hinh thức được giới thiệu trong luận văn này, đặc biệt trang hệ thống phan cứng/phần mêm nơi mà các thành phản phân cứng và phân xiểm dược miễu tả ở các mức dộ trừu tượng khác nhau. Khoáng cách mô tả giữa phân mềm và phân cứng được loại bỏ bằng cách ánh xạ chúc năng phần mềm và các biển với các tín hiệu phân cứng. Các thuộc tính của node cha LIN liên quan đến các trạng thái chung vượt ngoài khả năng, của bộ kiểm tra đặc tỉnh bình thức tiên.