Luận Văn Thạc Sĩ: Cải Tiến Thuật Toán Kiểm Chứng Tính Đúng Đắn Công Thức Khoảng

Luận văn thạc sĩ VNU UET trình bày cải tiến thuật toán chứng minh tính đúng đắn của công thức khoảng, mang lại giải pháp hiệu quả cho nghiên cứu.

• Tác giả: Nguyễn Thị Bình
• Người hướng dẫn: TS. Phạm Hồng Thái
• Trường học: Đại học Quốc gia Hà Nội
• Chuyên ngành: Công nghệ thông tin
• Đề tài: Cải Tiến Thuật Toán Kiểm Chứng Tính Đúng Đắn Công Thức Khoảng
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2014
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CẢM ƠN
• LỜI CAM ĐOAN
• DANH MỤC TỪ VIẾT TẮT
• DANH MỤC HÌNH VẼ
• DANH MỤC BẢNG
• MỤC LỤC
• 1. CHƯƠNG 1: CÁC KHÁI NIỆM CƠ BẢN
• 1.1. HỆ THỜI GIAN THỰC
• 1.2. KIỂM CHỨNG MÔ HÌM
• 1.2.1. Giới thiệu về kiểm chứng mô hình – Model Checking
• 1.2.2. Ý nghĩa, hạn chế của kiểm chứng mô hình
• 1.2.3. Kiểm chứng mô hình với hệ thời gian thực
• 1.2.4. Kiểm chứng mô hình với công thức khoảng
• 1.3. ÔTÔMAT THỜI GIAN
• 1.3.1. Thể hiện đồng hồ và phân vùng đồng hồ
• 1.3.2. Khái niệm ôtômat thời gian
• 2. CHƯƠNG 2: THUẬT TOÁN KIỂM CHỨNG MÔ HÌNH
• 2.1. ĐỒ THỊ VÙNG ĐẠT ĐƯỢC
• 2.1.1. Đồ thị vùng Ôtômat
• 2.1.2. Đồ thị đạt được nguyên
• 2.2. TÍNH RỜI RẠC HOÁ
• 2.2.1. Tập mô hình con của ôtômat thời gian
• 2.2.2. Khái niệm ε nguyên hoá và tính rời rạc hoá của công thức LDI
• 2.3. ĐỒ THỊ TRỌNG SỐ
• 2.4. THUẬT TOÁN KIỂM CHỨNG
• 3. CHƯƠNG 3: THUẬT TOÁN CẢI TIẾN
• 3.1. THUẬT TOÁN CẢI TIẾN
• 3.2. TÍNH HIỆU QUẢ
• 3.3. KẾT QUẢ THỬ NGHIỆM
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng quan về cải tiến thuật toán kiểm chứng tính đúng đắn công thức khoảng

Cải tiến thuật toán kiểm chứng tính đúng đắn công thức khoảng là một lĩnh vực nghiên cứu quan trọng trong công nghệ thông tin. Mục tiêu chính là nâng cao hiệu suất và độ chính xác của các thuật toán kiểm chứng. Việc cải tiến này không chỉ giúp giảm thiểu độ phức tạp mà còn tăng cường khả năng xử lý của hệ thống. Các nghiên cứu gần đây đã chỉ ra rằng việc áp dụng các phương pháp mới có thể mang lại những kết quả khả quan trong việc kiểm chứng tính đúng đắn của các công thức khoảng.

1.1. Khái niệm về thuật toán kiểm chứng

Thuật toán kiểm chứng là phương pháp tự động kiểm tra tính đúng đắn của một mô hình hoặc chương trình. Nó giúp xác định xem mô hình có thỏa mãn các thuộc tính đã định hay không. Kiểm chứng mô hình là một phần quan trọng trong quy trình phát triển phần mềm, giúp phát hiện lỗi sớm và đảm bảo chất lượng sản phẩm.

1.2. Tầm quan trọng của công thức khoảng

Công thức khoảng đóng vai trò quan trọng trong việc mô tả các tính chất thời gian của hệ thống. Chúng cho phép xác định các ràng buộc thời gian mà hệ thống cần tuân thủ. Việc kiểm chứng tính đúng đắn của công thức khoảng giúp đảm bảo rằng hệ thống hoạt động đúng theo yêu cầu thời gian đã đặt ra.

II. Vấn đề và thách thức trong kiểm chứng tính đúng đắn công thức khoảng

Mặc dù có nhiều tiến bộ trong lĩnh vực kiểm chứng mô hình, nhưng vẫn tồn tại nhiều thách thức lớn. Một trong những vấn đề chính là độ phức tạp của không gian trạng thái. Khi số lượng trạng thái tăng lên, việc kiểm chứng trở nên khó khăn hơn. Ngoài ra, các thuật toán hiện tại vẫn chưa hoàn toàn tối ưu, dẫn đến việc tiêu tốn nhiều thời gian và tài nguyên trong quá trình kiểm chứng.

2.1. Độ phức tạp của không gian trạng thái

Không gian trạng thái của hệ thống thường tăng theo hàm số mũ so với số dòng lệnh. Điều này gây khó khăn trong việc kiểm chứng, đặc biệt là với các hệ thống lớn và phức tạp. Việc giảm thiểu không gian trạng thái là một thách thức lớn trong nghiên cứu hiện nay.

2.2. Hạn chế của các thuật toán hiện tại

Các thuật toán kiểm chứng hiện tại vẫn còn nhiều hạn chế về hiệu suất và khả năng xử lý. Nhiều thuật toán không thể xử lý được các không gian trạng thái lớn, dẫn đến việc không thể áp dụng cho các hệ thống thực tế. Cần có những cải tiến đáng kể để nâng cao khả năng của các thuật toán này.

III. Phương pháp cải tiến thuật toán kiểm chứng tính đúng đắn công thức khoảng

Để giải quyết các vấn đề nêu trên, nhiều phương pháp cải tiến đã được đề xuất. Một trong những phương pháp hiệu quả là rời rạc hóa không gian trạng thái. Phương pháp này giúp giảm thiểu số lượng trạng thái cần kiểm chứng, từ đó nâng cao hiệu suất của thuật toán. Ngoài ra, việc áp dụng các kỹ thuật mới trong xây dựng đồ thị cũng góp phần cải thiện khả năng kiểm chứng.

3.1. Rời rạc hóa không gian trạng thái

Rời rạc hóa không gian trạng thái là một kỹ thuật giúp giảm thiểu số lượng trạng thái cần kiểm chứng. Bằng cách phân chia không gian thành các lớp tương đương, có thể giảm thiểu độ phức tạp và tăng cường hiệu suất kiểm chứng. Phương pháp này đã được chứng minh là hiệu quả trong nhiều nghiên cứu.

3.2. Xây dựng đồ thị phục vụ kiểm chứng

Việc xây dựng đồ thị là một phần quan trọng trong quá trình kiểm chứng. Đồ thị giúp mô tả các trạng thái và các phép chuyển giữa chúng. Cải tiến trong việc xây dựng đồ thị có thể giúp giảm thiểu kích thước của không gian trạng thái, từ đó nâng cao hiệu suất kiểm chứng.

IV. Ứng dụng thực tiễn của cải tiến thuật toán kiểm chứng

Cải tiến thuật toán kiểm chứng tính đúng đắn công thức khoảng đã được áp dụng trong nhiều lĩnh vực khác nhau. Các ứng dụng này không chỉ giúp nâng cao hiệu suất của hệ thống mà còn đảm bảo tính chính xác và độ tin cậy. Ví dụ, trong lĩnh vực y tế, việc kiểm chứng các hệ thống điều khiển thiết bị y tế là rất quan trọng để đảm bảo an toàn cho bệnh nhân.

4.1. Ứng dụng trong hệ thống y tế

Trong lĩnh vực y tế, các hệ thống điều khiển thiết bị y tế cần đảm bảo tính chính xác và độ tin cậy cao. Việc áp dụng các thuật toán kiểm chứng cải tiến giúp phát hiện lỗi sớm, từ đó đảm bảo an toàn cho bệnh nhân.

4.2. Ứng dụng trong hệ thống giao thông

Các hệ thống giao thông thông minh cũng cần được kiểm chứng để đảm bảo hoạt động hiệu quả. Việc áp dụng các phương pháp kiểm chứng cải tiến giúp nâng cao khả năng xử lý và giảm thiểu rủi ro trong các tình huống khẩn cấp.

V. Kết luận và tương lai của cải tiến thuật toán kiểm chứng

Cải tiến thuật toán kiểm chứng tính đúng đắn công thức khoảng là một lĩnh vực nghiên cứu đầy tiềm năng. Với sự phát triển không ngừng của công nghệ, các phương pháp mới sẽ tiếp tục được đề xuất và cải tiến. Tương lai của lĩnh vực này hứa hẹn sẽ mang lại nhiều giải pháp hiệu quả hơn, giúp nâng cao chất lượng và độ tin cậy của các hệ thống.

5.1. Triển vọng nghiên cứu trong tương lai

Nghiên cứu trong lĩnh vực cải tiến thuật toán kiểm chứng sẽ tiếp tục phát triển. Các phương pháp mới sẽ được đề xuất để giải quyết các vấn đề hiện tại, từ đó nâng cao hiệu suất và độ chính xác của các thuật toán kiểm chứng.

5.2. Tác động đến ngành công nghệ thông tin

Cải tiến thuật toán kiểm chứng sẽ có tác động lớn đến ngành công nghệ thông tin. Việc nâng cao khả năng kiểm chứng sẽ giúp đảm bảo chất lượng sản phẩm, từ đó nâng cao độ tin cậy của các hệ thống phần mềm trong thực tế.

Nội dung chính

Tổng quan nghiên cứu

Hệ thống thời gian thực ngày càng trở nên phổ biến và đóng vai trò quan trọng trong nhiều lĩnh vực như điều khiển tự động, hệ điều hành, và các thiết bị y tế. Theo ước tính, các hệ thống này đòi hỏi tính đúng đắn không chỉ về chức năng mà còn về mặt thời gian, với các ràng buộc nghiêm ngặt về khả năng đáp ứng trong khoảng thời gian xác định. Vấn đề kiểm chứng tính đúng đắn của các hệ thống này trở nên cấp thiết nhằm đảm bảo an toàn và hiệu quả vận hành. Mục tiêu nghiên cứu của luận văn là cải tiến thuật toán kiểm chứng tính đúng đắn của công thức khoảng trong hệ thời gian thực, cụ thể là công thức bất biến khoảng tuyến tính (LDI), nhằm giảm độ phức tạp tính toán và tăng hiệu suất kiểm chứng. Phạm vi nghiên cứu tập trung vào các hệ thống được mô hình hóa bằng ôtômat thời gian, với dữ liệu và thử nghiệm thực hiện tại Đại học Công nghệ - Đại học Quốc gia Hà Nội trong giai đoạn 2014. Ý nghĩa của nghiên cứu được thể hiện qua việc giảm thiểu thời gian kiểm chứng và tài nguyên tính toán, góp phần nâng cao độ tin cậy của các hệ thống thời gian thực trong thực tế.

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 các lý thuyết và mô hình sau:

• Ôtômat thời gian (Timed Automata): Mô hình hóa hệ thống thời gian thực bằng các trạng thái và đồng hồ, cho phép biểu diễn các ràng buộc thời gian và chuyển trạng thái dựa trên các điều kiện đồng hồ.
• Lôgic khoảng (Duration Calculus - DC): Hệ lôgic dùng để đặc tả các tính chất thời gian của hệ thống, trong đó các trạng thái được biểu diễn như hàm bool theo thời gian, và các công thức khoảng mô tả tổng thời gian xuất hiện của trạng thái.
• Công thức bất biến khoảng tuyến tính (Linear Duration Invariant - LDI): Lớp công thức trong DC biểu diễn các ràng buộc tuyến tính về tổng thời gian xuất hiện của các trạng thái trong khoảng thời gian quan sát.
• Kiểm chứng mô hình (Model Checking): Kỹ thuật tự động kiểm tra tính đúng đắn của mô hình hệ thống so với các thuộc tính được đặc tả, sử dụng thuật toán duyệt không gian trạng thái.
• Đồ thị vùng đạt được nguyên (Integral Reachability Graph): Cấu trúc dữ liệu rút gọn không gian trạng thái của ôtômat thời gian bằng cách phân vùng đồng hồ và rời rạc hóa thời gian, giúp giảm độ phức tạp tính toán.
• Đồ thị trọng số phục vụ kiểm chứng LDI: Đồ thị được xây dựng từ đồ thị vùng nguyên, trong đó các cạnh được chia nhỏ thành các cung có trọng số 0 hoặc 1, tương ứng với các bước thời gian rời rạc.

Các khái niệm chính bao gồm: vùng đồng hồ (clock regions), dáng điệu (runs) của ôtômat, tính rời rạc hóa (discretization) của công thức LDI, và thuật toán duyệt đồ thị trọng số để kiểm chứng tính thoả mãn công thức.

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

Nguồn dữ liệu nghiên cứu bao gồm các mô hình ôtômat thời gian được xây dựng dựa trên các hệ thống thực tế như hệ thống chắn tàu, với các tham số thời gian a, b, c được lấy ngẫu nhiên hoặc theo ước tính. Phương pháp phân tích chính là xây dựng và rút gọn đồ thị vùng đạt được nguyên, chuyển đổi sang đồ thị trọng số phục vụ kiểm chứng LDI, sau đó áp dụng thuật toán duyệt đồ thị để kiểm tra tính thoả mãn công thức.

Cỡ mẫu thử nghiệm gồm 21 bộ ôtômat với số trạng thái và phép chuyển khác nhau, được cài đặt và chạy trên môi trường PHP với web server Apache. Phương pháp chọn mẫu dựa trên các trường hợp thực tế và các tham số thời gian khác nhau nhằm đánh giá hiệu quả thuật toán. Timeline nghiên cứu kéo dài trong năm 2014, bao gồm các bước: tìm hiểu lý thuyết, xây dựng thuật toán, cài đặt chương trình, thử nghiệm và đánh giá kết quả.

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

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

1. Hiệu quả rút gọn không gian trạng thái: Việc sử dụng đồ thị vùng đạt được nguyên giúp giảm đáng kể số lượng trạng thái so với đồ thị vùng tổng quát. Ví dụ, đồ thị vùng nguyên của ôtômat mẫu có 8 trạng thái và 11 phép chuyển, trong khi đồ thị vùng tổng quát có thể lớn hơn nhiều lần.

2. Tính rời rạc hóa công thức LDI: Luận văn chứng minh rằng công thức LDI là rời rạc hóa được đối với ôtômat thời gian, tức là kiểm chứng trên mô hình nguyên tương đương với kiểm chứng trên mô hình thực. Điều này giúp giảm độ phức tạp tính toán mà vẫn đảm bảo tính chính xác.

3. Cải tiến thuật toán kiểm chứng LDI: Thuật toán cải tiến bằng cách gộp các cung liên tiếp có trọng số 1 thành cung lớn hơn với trọng số tổng, giảm số đỉnh đồ thị trọng số phục vụ kiểm chứng. Kết quả thử nghiệm cho thấy thời gian kiểm chứng giảm từ khoảng 24-64 giây xuống còn 28-272 giây tùy trường hợp, với số đỉnh và cung giảm đáng kể (ví dụ: từ 259 đỉnh xuống 63 đỉnh trong một trường hợp).

4. Độ phức tạp thuật toán: Thuật toán chưa cải tiến có độ phức tạp duyệt đồ thị là O(2^n * n), trong khi thuật toán cải tiến có thể giảm xuống O(2^n) trong trường hợp tốt, giúp tăng hiệu quả xử lý đáng kể.

Thảo luận kết quả

Nguyên nhân chính của sự cải tiến là do việc gộp các cung có trọng số liên tiếp giúp giảm số lượng đỉnh cần duyệt, từ đó giảm thời gian và bộ nhớ sử dụng. So sánh với các nghiên cứu trước đây, luận văn đã phát triển thêm bước rời rạc hóa và tối ưu cấu trúc đồ thị, phù hợp với các hệ thống thời gian thực phức tạp.

Kết quả thử nghiệm trên hệ thống chắn tàu thực tế cho thấy thuật toán cải tiến không chỉ giảm thời gian kiểm chứng mà còn giữ nguyên tính chính xác, đảm bảo các công thức LDI được kiểm chứng đầy đủ. Biểu đồ so sánh thời gian chạy thuật toán cải tiến và chưa cải tiến minh họa rõ sự khác biệt lớn về hiệu suất.

Ý nghĩa của kết quả là mở ra hướng tiếp cận mới cho việc kiểm chứng mô hình hệ thống thời gian thực, giúp giảm thiểu rủi ro do lỗi phần mềm trong các ứng dụng quan trọng như điều khiển giao thông, y tế, và hàng không.

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

1. Áp dụng thuật toán cải tiến trong các công cụ kiểm chứng mô hình: Động từ hành động là "tích hợp", target metric là "giảm thời gian kiểm chứng ít nhất 30%", timeline trong 6-12 tháng, chủ thể thực hiện là các nhóm phát triển phần mềm kiểm chứng mô hình.

2. Mở rộng nghiên cứu sang các lớp công thức rời rạc hóa khác: Động từ "nghiên cứu", target metric là "mở rộng phạm vi công thức kiểm chứng", timeline 1-2 năm, chủ thể là các nhà nghiên cứu trong lĩnh vực khoa học máy tính.

3. Phát triển module tích hợp giảm thiểu độ trễ thời gian trong phần mềm kiểm chứng: Động từ "phát triển", target metric là "giảm độ trễ xử lý xuống dưới 10%", timeline 12 tháng, chủ thể là nhóm kỹ sư phần mềm.

4. Tăng cường đào tạo và phổ biến kiến thức về kiểm chứng mô hình và thuật toán cải tiến: Động từ "tổ chức", target metric là "đào tạo ít nhất 100 chuyên gia trong 1 năm", chủ thể là các trường đại học và viện nghiên cứu.

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

1. Nhà nghiên cứu và giảng viên trong lĩnh vực khoa học máy tính và kỹ thuật phần mềm: Giúp hiểu sâu về kiểm chứng mô hình hệ thời gian thực và các thuật toán cải tiến, phục vụ nghiên cứu và giảng dạy.

2. Kỹ sư phát triển phần mềm hệ thống thời gian thực: Áp dụng các phương pháp kiểm chứng để nâng cao độ tin cậy và an toàn của sản phẩm.

3. Sinh viên cao học chuyên ngành kỹ nghệ phần mềm và công nghệ thông tin: Là tài liệu tham khảo quan trọng cho luận văn, đề tài nghiên cứu liên quan đến kiểm chứng mô hình và hệ thời gian thực.

4. Các tổ chức và doanh nghiệp phát triển hệ thống điều khiển tự động, y tế, giao thông: Hỗ trợ đánh giá và đảm bảo chất lượng phần mềm trong các hệ thống quan trọng.

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

1. Kiểm chứng mô hình là gì và tại sao quan trọng trong hệ thời gian thực?
   Kiểm chứng mô hình là kỹ thuật tự động kiểm tra tính đúng đắn của mô hình hệ thống so với các thuộc tính đặt ra. Trong hệ thời gian thực, nó giúp đảm bảo hệ thống đáp ứng các ràng buộc thời gian nghiêm ngặt, tránh lỗi gây hậu quả nghiêm trọng.

2. Công thức bất biến khoảng tuyến tính (LDI) là gì?
   LDI là công thức trong lôgic khoảng biểu diễn các ràng buộc tuyến tính về tổng thời gian xuất hiện của các trạng thái trong khoảng thời gian quan sát, dùng để đặc tả tính chất thời gian của hệ thống.

3. Tại sao cần rời rạc hóa công thức LDI?
   Rời rạc hóa giúp chuyển bài toán kiểm chứng từ không gian thời gian thực vô hạn sang không gian nguyên rời rạc, giảm độ phức tạp tính toán mà vẫn giữ nguyên tính chính xác.

4. Thuật toán cải tiến kiểm chứng LDI hoạt động như thế nào?
   Thuật toán gộp các cung liên tiếp có trọng số 1 thành cung lớn hơn với trọng số tổng, giảm số đỉnh đồ thị cần duyệt, từ đó giảm thời gian và bộ nhớ sử dụng trong quá trình kiểm chứng.

5. Kết quả thử nghiệm cho thấy cải tiến thuật toán có hiệu quả ra sao?
   Thời gian kiểm chứng giảm đáng kể, ví dụ từ 259 đỉnh xuống còn 63 đỉnh trong một trường hợp, thời gian chạy giảm từ hàng trăm giây xuống còn vài chục giây, giúp tăng hiệu quả và khả năng áp dụng thực tế.

Kết luận

• Luận văn đã nghiên cứu và áp dụng thành công các lý thuyết ôtômat thời gian, lôgic khoảng và kiểm chứng mô hình để giải quyết bài toán kiểm chứng công thức LDI trong hệ thời gian thực.
• Thuật toán kiểm chứng LDI được cải tiến bằng cách rút gọn đồ thị trọng số, giảm đáng kể số đỉnh và cung, từ đó giảm độ phức tạp và thời gian xử lý.
• Kết quả thử nghiệm trên hệ thống chắn tàu thực tế cho thấy thuật toán cải tiến vượt trội so với thuật toán trước đó về hiệu suất mà vẫn đảm bảo tính chính xác.
• Nghiên cứu mở ra hướng phát triển các phương pháp kiểm chứng mô hình hiệu quả hơn cho các hệ thống thời gian thực phức tạp.
• Các bước tiếp theo bao gồm mở rộng thuật toán cho các lớp công thức khác, hoàn thiện phần mềm kiểm chứng và ứng dụng rộng rãi trong công nghiệp.

Hành động khuyến nghị: Các nhà nghiên cứu và kỹ sư nên áp dụng thuật toán cải tiến này trong phát triển và kiểm thử hệ thống thời gian thực để nâng cao độ tin cậy và hiệu quả vận hành.

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

CHƯƠNG 1: CÁC KHÁI NIỆM CƠ BẢN 1. HỆ THỜI GIAN THỰC 1. Khái niệm hệ thời gian thực Trong những năm gần đây hệ thống điều khiển thời gian thực đang trở thành một lĩnh vực thu hút sự quan tâm của các nhà nghiên cứu khoa học về khoa học máy tính. Đây là hệ thống được ứng dụng rộng rãi hiện nay như: hệ điều hành thời gian thực, lập lịch, rô bôt, các hệ thống điều khiển tự động… Hiện có một số hiểu nhầm về hệ thời gian thực là hệ mà phải xử lí tốc độ cao, xử lý nhanh.

Thực chất thời gian thực có nghĩa là thời gian phải “đủ nhanh” và được đặt trong một ngữ cảnh nào đó như: Có thể là khả năng đáp ứng chính xác tại thời điểm, hay xảy ra trong khoảng thời gian xác định, hay chậm nhât là lúc nào và sớm nhất là lúc nào [2]. Sự kiện Phản ứng Sự kiện Phản ứng T T ts tp-1 tp-2 Thời gian ts tp Thời gian a) Chính xác tại t = tp b) Trong khoảng. tp-1 ≤ t ≤ tp-2 Sự kiện Phản ứng Sự kiện Phản ứng T T ts tp Thời gian ts tp Thời gian c) Chậm nhất là. t ≤ tp d) Sớm nhất là.

t ≥ tp Hình 1-1: Khả năng đáp ứng của hệ thống Ví dụ xử lý tiến trình của hệ điều hành: khi có rất nhiều các tiến trình cần xử lý, và tại mỗi thời điểm chí có một tiến trình được thực hiện.Vì vậy cần có sự phân chia thời gian, lựa chọn tiến trình sao cho việc thực thi hiệu quả nhất. Định nghĩa [4]: Hệ thống thời gian thực là hệ thống mà tính đúng đắn của nó không chỉ phụ thuộc chức năng mà còn phụ thuộc thời gian, hệ thống có lỗi khi yêu cầu về thời gian không được thoả mãn. Như vậy việc thiết kế hệ thống thời gian thực phải đảm bảo hệ thống có thể tiếp nhận các ràng buộc và mặt thời gian trong suốt quá trình thực thi. Phân loại hệ thời gian thực Các hệ thời gian thực thường được phân thành hai loại sau: hệ thời gian thực mềm (Soft real time system) và hệ thời gian thực cứng (Hard real time system) [4]: LUAN VAN CHAT LUONG download : add [e-mail] 3 Đối với hệ thời gian thực mềm, yếu tố thời gian đóng vai trò quan trọng nhưng nếu thời gian hệ thống đáp ứng không thoả mãn ràng buộc đưa ra – vi phạm ràng buộc thời gian, thời gian trả lời của hệ thống vượt quá giới hạn trễ cho phép tuy nhiên hệ thống vẫn tiếp tục hoat động bình thường, tác hại trễ này thường không đáng kể.

Ví dụ mạng rút tiền tự động ATM là hệ thống thời gian thực. Khi đưa thẻ ATM vào máy, máy sẽ phản ứng lại trong vòng 1 hay 2 giây hoặc nó lâu hơn thế, và nếu không thực hiện được giao dịch thì vẫn phải chấp nhận. Ngược lại với hệ thời gian thực mềm là hệ thời gian thực cứng, trường hợp này hệ thống quan tâm khắt khe đến các hậu quả do vi phạm về giới hạn thời gian trễ cho phép. Thường thì hậu quả của sự vi phạm về mặt thời gian này là ảnh hưởng rất lớn gây tổn hại về vật chất về kinh tế lớn.

Ví dụ như máy hỗ trợ nhịp tim cho bệnh nhân khi phẫu thuật. Thuật toán điều khiển phụ thuộc vào thời gian nhịp tim của người bệnh, nếu thời gian này bị trễ, tính mạng của người bệnh sẽ bị ảnh hưởng. Hay ví dụ điển hình là hệ thống điều khiển không lưu, phân phối đường bay, thời gian cất cánh, hạ cánh không hợp lý, không đúng lúc có thể gây ra tai nạn máy bay mà thảm họa của nó khó mà lường trước được. KIỂM CHỨNG MÔ HÌNH 1.

Giới thiệu về kiểm chứng mô hình – Model Checking Kiểm chứng mô hình [1] là một kĩ thuật giúp kiểm tra một chương trình hoặc một bản thiết kế có thỏa mãn các tính chất đặt ra hay không một cách tự động. Đầu vào là một mô hình cần kiểm chứng và các thuộc tính cần thỏa mãn. Đầu ra là kết luận mô hình thỏa mãn các tính chất hoặc đưa ra một phản ví dụ nếu mô hình không thỏa mãn Các nghiên cứu đầu tiên về Model Checking (MC) được thực hiện bởi Edmund Melson Clarke và Ernest Allen Emerson cũng như Jean-Pierre Queille và Joseph Sifakis Jean-Pierre. Clarke, Emerson và Sifakis đã được nhận giải thưởng Turing năm 2007 cho các đóng góp của họ về MC.

Có thể nói kiểm chứng mô hình là kỹ thuật phân tích hệ thống để xác định tính hợp lệ của một hay nhiều tính chất mà người dùng quan tâm trong một mô hình cho trước. Cụ thể hơn, với mô hình M và thuộc tính p cho trước, nó kiểm tra liệu thuộc tính p có thỏa mãn trong mô hình M hay không: M |= p. Về mặt thực thi, kiểm chứng mô hình là kỹ thuật tĩnh, nó duyệt qua tất cả các trạng thái, các đường thực thi có thể có trong mô hình M để xác định tính thỏa p. Trên thực tế, mô hình kiểm chứng đã chứng minh rằng nó là một phương thức hiệu quả để phát hiện nhiều lỗi trong các pha thiết kế ban đầu.

Kiểm chứng mô hình bao gồm 3 bước: Mô hình hóa, đặc tả và kiểm chứng. LUAN VAN CHAT LUONG download : add [e-mail] 4 Ở bước mô hình hóa: kết quả tạo ra là một mô hình mà các công cụ kiểm chứng có thể sử dụng được. Đầu vào của bước này có thể là bản thiết kế phần mềm hoặc là các dòng mã lập trình. Bước đặc tả: các thuộc tính mà bản thiết kế cần thỏa mãn được đặc tả.

Các thuộc tính này thường được diễn đạt bằng các biểu thức logic. Kết quả của hai bước mô hình hóa và đặc tả chính là đầu vào của kiểm chứng mô hình. Ở bước cuối cùng: kiểm chứng, công cụ kiểm chứng sẽ tự động thực hiện và trả về kết quả là thỏa mãn nếu mô hình thỏa mãn các thuộc tính, hoặc đưa ra một phản ví dụ nếu mô hình không thỏa mãn. Dựa vào phản ví dụ, người ta có thể tìm ra được lý do vì sao mô hình không thỏa mãn các thuộc tính đặt ra.

Ý nghĩa, hạn chế của kiểm chứng mô hình Mục đích chính của kiểm chứng mô hình giúp tạo ra khả năng cho phép xây dựng và phát triển hệ thống một cách đúng đắn. Các hệ thống phần mềm đang ngày càng trở nên cần thiết và đóng vai trò quan trọng trong đời sống hàng ngày. Nhiều công việc có mức độ ảnh hưởng lớn được thực hiện bởi phần mềm như điều khiển đèn giao thông, giao dịch ngân hàng, điều khiển các thiết bị y tế. Những phần mềm thực hiện các công việc đó phải đảm bảo có độ tin cậy rất cao và không được phép xuất hiện lỗi.

Thực tế cho thấy nếu có một lỗi nhỏ cũng dấn tới việc phá huỷ toàn bộ hệ thống. Như sự kiện ngày 28/6/1962: Tàu thăm dò vũ trụ Mariner I - con tàu có sứ mệnh bay đến sao Kim nhưng đã bị phá hủy 293 giây sau khi phóng do bay chệch hướng so với dự kiến ban đầu. Những cuộc điều tra sau đó đã khám phá ra rằng một công thức được viết trên giấy bằng bút chì đã không được chuyển đổi sang mã điện toán, khiến hệ thống máy tính tính toán sai đường đi của tên lửa. Vì vậy, sự ra đời của kiểm chứng mô hình là cực kì quan trọng, kiểm chứng mô hình cho phép khẳng định được phần mềm hoàn toàn không còn lỗi và thực hiện được đúng các chức năng đã đặt ra.

Ngoài ra, kiểm chứng còn có ý nghĩa quan trọng trong quy trình phát triển phần mềm. Kiểm chứng mô hình cho phép tìm ra được các lỗi ngay từ giai đoạn thiết kế của quy trình phát triển. Điều này có vai trò rất quan trọng vì các lỗi từ giai đoạn thiết kế nếu tìm ra muộn có thể gây thiệt hại rất lớn so với các lỗi của giai đoạn sau. Hiệu suất của việc kiểm định thường phụ thuộc vào không gian trạng thái của hệ thống.

Các hệ thống MC gần đây có thể xử lý các không gian trạng thái lên đến từ 108 đến 1010 phần tử. Do vậy MC không được dùng cho các hệ thống có số trạng thái vô hạn, cũng vì lý do giới hạn của bộ nhớ và số nhân xử lý của hệ thống máy tính. Chính vì thế vấn đề lớn nhất của Model Checking vẫn là bùng nổ tổ hợp không gian trạng thái của hệ thống. Không gian trạng thái phát sinh trong chương trình thường LUAN VAN CHAT LUONG download : add [e-mail] 5 tăng theo hàm số mũ so với số dòng lệnh và phụ thuộc vào: biến, kích thước của biến tính theo số bit, và cấu trúc của chương trình.

Kiểm chứng mô hình với hệ thời gian thực Với đặc trưng hệ thống thời gian thực là tính đúng đắn của hệ thống phụ thuộc vào thời gian. Thời gian t chúng ta xét trên tập số thực R+. Mỗi trạng thái của hệ thống không chỉ là trạng thái bình thường mà còn gắn kèm với đại lượng thời gian. Như vậy không gian trạng thái của hệ thời gian thực là rất rộng.

Vấn đề của bài toán đặt ra khi kiểm chứng mô hình trên thời gian thực là sự phức tạp về thời gian và không gian trạng thái phát sinh. Kiểm chứng mô hình cần rút gọn không gian trạng thái đưa về các lớp tương đương dựa trên kĩ thuật phân vùng, miền. Trên cơ sở đó đưa ra thuật toán để kiểm tra tính đúng đắn của hệ thống. Kiểm chứng mô hình với công thức khoảng Ở mục này ta làm rõ yếu tố thời gian trong quá trình hoạt động của hệ thống.

Khi hệ thống xuất hiện ở các trạng thái thì thời điểm xuất hiện là lúc nào, xuất hiện bao lâu, phải thoả mãn ràng buộc là gì? Hệ thống xuất hiện ở trạng thái s tại một thời điểm thì ta gọi đây là tính chất thời điểm. Còn tổng thời gian mà hệ thống ở các trạng thái được xem xét thì được gọi là tính chất thời khoảng. Yếu tố rằng buộc thể hiện khi hệ thống xuất hiện ở các trạng thái này phải thoả mãn điều kiện hạn chế thời gian: bị chặn trong khoảng nào đó. Và bài toán đặt ra là liệu với điều kiện cho trước đó hệ thống có đảm bảo tính đúng đắn hay không.

Để chứng minh được sự thoả mãn hay không của hệ thống với các yêu cầu thời gian được đặt ra đã có rất nhiều thuật toán của nhiều nhà nghiên cứu khoa học nhưng độ phức tạp còn rất cao.