Luận văn thạc sĩ về cải tiến thuật toán chứng minh tính đúng đắn công thức khoảng

Luận văn thạc sĩ toán học nghiên cứu cải tiến thuật toán chứng minh tính đúng đắn công thức khoảng, khảo sát thực trạng, phân tích nguyên nhân, đề xuất giải pháp cải thiện thực

• 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 Chứng Minh 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Ở ĐẦU
• 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ÌNH
• 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.2. TÍNH RỜI RẠC HOÁ
• 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. Giới thiệu về thuật toán

Thuật toán chứng minh tính đúng đắn của công thức khoảng là một lĩnh vực quan trọng trong công nghệ thông tin, đặc biệt là trong kiểm chứng mô hình. Thuật toán này giúp xác định xem một hệ thống có thỏa mãn các yêu cầu về thời gian hay không. Việc chứng minh tính đúng đắn của các công thức này không chỉ phụ thuộc vào logic mà còn vào các yếu tố thời gian. Công thức khoảng được sử dụng để mô tả các ràng buộc thời gian trong hệ thống, từ đó giúp đánh giá hiệu suất và độ tin cậy của hệ thống. Tuy nhiên, độ phức tạp của các thuật toán hiện tại vẫn còn cao, dẫn đến việc cần thiết phải cải tiến các phương pháp này để giảm thiểu chi phí tính toán và tăng hiệu quả. Việc kiểm tra tính đúng đắn của các công thức khoảng là một thách thức lớn, đặc biệt trong các hệ thống thời gian thực, nơi mà thời gian phản hồi là rất quan trọng.

1.1. Tầm quan trọng của việc kiểm chứng

Kiểm chứng mô hình là một kỹ thuật quan trọng trong phát triển phần mềm, giúp phát hiện lỗi ngay từ giai đoạn thiết kế. Kiểm chứng mô hình cho phép xác định tính hợp lệ của các thuộc tính trong một mô hình, từ đó đảm bảo rằng hệ thống hoạt động đúng như mong đợi. Sự ra đời của các thuật toán kiểm chứng đã giúp giảm thiểu rủi ro trong quá trình phát triển phần mềm. Tuy nhiên, các thuật toán này vẫn gặp phải vấn đề về không gian trạng thái, dẫn đến việc cần phải cải tiến để nâng cao hiệu suất. Việc kiểm tra tính đúng đắn của các công thức khoảng trong các hệ thống thời gian thực là một thách thức lớn, đòi hỏi các phương pháp mới và hiệu quả hơn.

II. Các khái niệm cơ bản

Để hiểu rõ hơn về thuật toán chứng minh tính đúng đắn của công thức khoảng, cần nắm vững các khái niệm cơ bản liên quan đến hệ thống thời gian thực và kiểm chứng mô hình. Hệ thời gian thực là hệ thống mà tính đúng đắn không chỉ phụ thuộc vào chức năng mà còn vào thời gian. Các hệ thống này thường được phân thành hai loại: hệ thời gian thực mềm và hệ thời gian thực cứng. Kiểm chứng mô hình là kỹ thuật giúp xác định xem một mô hình có thỏa mãn các thuộc tính đã định hay không. Việc sử dụng logic khoảng trong kiểm chứng mô hình giúp mô tả các ràng buộc thời gian, từ đó xác định tính đúng đắn của hệ thống. Tuy nhiên, độ phức tạp của các thuật toán kiểm chứng hiện tại vẫn còn cao, cần có các phương pháp cải tiến để giảm thiểu chi phí tính toán và tăng hiệu quả.

2.1. Hệ thống thời gian thực

Hệ thống thời gian thực là một lĩnh vực quan trọng trong công nghệ thông tin, nơi mà thời gian phản hồi là rất quan trọng. Các hệ thống này thường được ứng dụng trong các lĩnh vực như điều khiển tự động, hệ điều hành thời gian thực, và rô bốt. Thời gian thực không chỉ đơn thuần là tốc độ xử lý mà còn liên quan đến khả năng đáp ứng đúng thời điểm. Việc thiết kế các hệ thống này đòi hỏi phải đảm bảo rằng các ràng buộc về thời gian được thỏa mãn. Các hệ thống thời gian thực thường gặp phải vấn đề về độ phức tạp trong việc kiểm chứng tính đúng đắn, do đó cần có các phương pháp cải tiến để nâng cao hiệu suất kiểm chứng.

III. Thuật toán kiểm chứng

Thuật toán kiểm chứng mô hình là một phần quan trọng trong việc xác định tính đúng đắn của các hệ thống thời gian thực. Thuật toán này giúp kiểm tra xem một mô hình có thỏa mãn các thuộc tính đã định hay không. Việc sử dụng logic khoảng trong kiểm chứng mô hình giúp mô tả các ràng buộc thời gian, từ đó xác định tính đúng đắn của hệ thống. Tuy nhiên, độ phức tạp của các thuật toán kiểm chứng hiện tại vẫn còn cao, dẫn đến việc cần thiết phải cải tiến các phương pháp này để giảm thiểu chi phí tính toán và tăng hiệu quả. Các thuật toán kiểm chứng hiện tại thường gặp phải vấn đề về không gian trạng thái, do đó cần có các phương pháp mới để nâng cao hiệu suất kiểm chứng.

3.1. Các phương pháp kiểm chứng

Các phương pháp kiểm chứng hiện tại bao gồm nhiều kỹ thuật khác nhau, từ kiểm chứng mô hình đến các thuật toán kiểm chứng cụ thể. Kiểm chứng mô hình là một kỹ thuật quan trọng giúp phát hiện lỗi trong các giai đoạn thiết kế. Việc sử dụng logic khoảng trong kiểm chứng mô hình giúp mô tả các ràng buộc thời gian, từ đó xác định tính đúng đắn của hệ thống. Tuy nhiên, độ phức tạp của các thuật toán kiểm chứng hiện tại vẫn còn cao, dẫn đến việc cần thiết phải cải tiến các phương pháp này để giảm thiểu chi phí tính toán và tăng hiệu quả. 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ể giúp nâng cao hiệu suất kiểm chứng và giảm thiểu rủi ro trong quá trình phát triển phần mềm.

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, robot, 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. Việc kiểm chứng tính đúng đắn của các hệ thống này là một thách thức lớn do sự phức tạp của yếu tố thời gian và không gian trạng thái rất rộng. 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 thuật toán và nâng cao hiệu quả 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 thực nghiệm lấy từ hệ thống điều khiển tự động tại chỗ giao nhau đường sắt, trong khoảng thời gian nghiên cứu từ năm 2014 tại Đại học Công nghệ - Đại học Quốc gia Hà Nội. Ý nghĩa của nghiên cứu được thể hiện qua việc giảm đáng kể số lượng trạng thái cần duyệt trong quá trình kiểm chứng, từ đó rút ngắn thời gian xử lý và giảm chi phí tính toán, góp phần nâng cao độ tin cậy và an toàn cho các hệ thống thời gian thực.

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ông thức bất biến khoảng tuyến tính (LDI) được sử dụng để mô tả các ràng buộc về tổng thời gian hệ thống ở các trạng thái nhất định.
• 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ả bằng lôgic, trong đó việc duyệt không gian trạng thái là bước then chốt.
• Đồ thị vùng đạt được nguyên (Integral Reachability Graph): Kỹ thuật rời rạc hóa không gian trạng thái liên tục thành các vùng nguyên giúp giảm số lượng trạng thái cần xét.
• Đồ 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 gán trọng số biểu diễn khoảng thời gian, phục vụ cho việc kiểm chứng công thức LDI.

Các khái niệm chính bao gồm: vùng đồng hồ (clock regions), tính rời rạc hóa (discretization), đồ thị miền (zone graph), và thuật toán duyệt đồ thị trọng số.

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 từ hệ thống điều khiển tự động tại chỗ giao nhau đường sắt, với các tham số đồng hồ và trạng thái được xác định cụ thể. Phương pháp phân tích chính là xây dựng đồ thị vùng đạt được nguyên từ ôtômat, chuyển đổi sang đồ thị trọng số phục vụ kiểm chứng LDI, và áp dụng thuật toán duyệt đồ thị để kiểm tra tính thoả mãn công thức LDI.

Cỡ mẫu nghiên cứu là hệ thống ôtômat gồm 8 trạng thái và 11 phép chuyển, với hai đồng hồ thời gian x, y. Phương pháp chọn mẫu dựa trên mô hình thực tế của hệ thống chắn tàu, đảm bảo tính đại diện cho các hệ thống thời gian thực phức tạp. Timeline nghiên cứu bao gồm các bước: xây dựng mô hình ôtômat, tạo đồ thị vùng nguyên, chuyển đổi sang đồ thị trọng số, và thực hiện kiểm chứng bằng thuật toán cải tiến.

Phương pháp phân tích sử dụng kỹ thuật duyệt đồ thị theo chiều sâu kết hợp với các điều kiện ràng buộc về trọng số và độ dài đường đi, nhằm phát hiện nhanh các trường hợp không thoả mãn công thức LDI.

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

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

1. Giảm số lượng đỉnh và cung trong đồ thị trọng số: Thuật toán cải tiến đã giảm đáng kể số đỉnh và cung so với thuật toán chưa cải tiến. Ví dụ, trong hệ thống ôtômat 8 trạng thái, số đỉnh giảm từ khoảng 259 xuống còn khoảng 63, tương ứng giảm hơn 75% số lượng trạng thái cần duyệt.

2. Rút ngắn thời gian kiểm chứng: Thời gian kiểm chứng trung bình giảm từ khoảng 2.5 giây xuống còn dưới 1 giây trong nhiều trường hợp thử nghiệm, tương đương giảm hơn 60% thời gian xử lý.

3. Độ chính xác và tính đúng đắn được bảo toàn: Thuật toán cải tiến vẫn đảm bảo kết quả kiểm chứng chính xác, không bỏ sót các trường hợp không thoả mãn công thức LDI, nhờ việc phân tích chi tiết các cung có độ dài lớn và xử lý các trường hợp đặc biệt khi l(p) > B.

4. Khả năng xử lý các hệ thống phức hợp: Thuật toán cải tiến cho thấy hiệu quả rõ rệt khi áp dụng cho các hệ thống ghép song song nhiều ôtômat, giúp giảm bùng nổ tổ hợp không gian trạng thái.

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 liên tiếp có trọng số bằng 1 thành các cung lớn hơn với trọng số tổng hợp, giúp giảm số lượng đỉnh cần duyệt trong đồ thị trọng số. Điều này làm giảm đáng kể độ phức tạp tính toán, đặc biệt trong các trường hợp có nhiều cung liên tiếp với trọng số nhỏ.

So sánh với các nghiên cứu trước đây, thuật toán cải tiến không chỉ giữ được tính đúng đắn mà còn nâng cao hiệu quả xử lý, phù hợp với các hệ thống thời gian thực có không gian trạng thái lớn. Kết quả này có thể được minh họa qua biểu đồ so sánh thời gian chạy giữa hai thuật toán, cho thấy đường chạy thời gian của thuật toán cải tiến luôn thấp hơn đáng kể.

Ý nghĩa của kết quả là mở ra hướng phát triển các công cụ kiểm chứng mô hình hiệu quả hơn, giảm thiểu chi phí tính toán và thời gian phản hồi, từ đó nâng cao độ tin cậy và an toàn cho các hệ thống thời gian thực trong thực tế.

Đề 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à "triển khai", mục tiêu là giảm thời gian kiểm chứng trung bình ít nhất 50%, trong vòng 6 tháng, do các nhóm phát triển phần mềm và nghiên cứu khoa học thực hiện.

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: Đề xuất "nghiên cứu" và "phát triển" các thuật toán kiểm chứng cho các công thức phức tạp hơn trong lôgic khoảng, nhằm tăng phạm vi ứng dụng, trong vòng 1-2 năm, do các nhà nghiên cứu và sinh viên cao học thực hiện.

3. Tích hợp thuật toán cải tiến vào quy trình phát triển phần mềm thời gian thực: Khuyến nghị "tích hợp" thuật toán vào các giai đoạn thiết kế và kiểm thử phần mềm để phát hiện lỗi sớm, giảm thiểu rủi ro, trong vòng 1 năm, do các công ty phát triển phần mềm và tổ chức kiểm thử đảm nhiệm.

4. Phát triển giao diện trực quan và module hỗ trợ: Động từ hành động là "xây dựng" các module trực quan giúp người dùng dễ dàng theo dõi quá trình kiểm chứng và phân tích kết quả, nâng cao trải nghiệm người dùng, trong vòng 9 tháng, do các nhóm phát triển phần mềm thực hiện.

Đố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: Giúp hiểu sâu về kiểm chứng mô hình hệ thời gian thực, áp dụng các thuật toán cải tiến trong 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: Hỗ trợ trong việc thiết kế, kiểm thử và đảm bảo tính đúng đắn của các hệ thống phức tạp, giảm thiểu lỗi và rủi ro.

3. Sinh viên cao học chuyên ngành kỹ thuật phần mềm và công nghệ thông tin: Là tài liệu tham khảo quý giá cho các đề tài luận văn, nghiên cứu về kiểm chứng mô hình và lôgic khoảng.

4. Các tổ chức và doanh nghiệp phát triển hệ thống điều khiển tự động: Giúp nâng cao hiệu quả kiểm chứng, đảm bảo an toàn và độ tin cậy cho các sản phẩm và dịch vụ của mình.

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 đặc tả. Trong hệ thời gian thực, nó giúp đảm bảo hệ thống hoạt động đúng chức năng và đáp ứng các ràng buộc thời gian, giảm thiểu rủi ro và lỗi 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 dùng để mô tả các ràng buộc về tổng thời gian hệ thống ở các trạng thái nhất định, ví dụ như tổng thời gian ở trạng thái an toàn không vượt quá một ngưỡng cho phép.

3. Thuật toán cải tiến có ưu điểm gì so với thuật toán kiểm chứng truyền thống?
   Thuật toán cải tiến giảm đáng kể số lượng trạng thái và cạnh cần duyệt trong đồ thị trọng số, từ đó rút ngắn thời gian kiểm chứng và giảm chi phí tính toán mà vẫn đảm bảo tính chính xác.

4. Phương pháp rời rạc hóa có vai trò như thế nào trong kiểm chứng mô hình?
   Rời rạc hóa chuyển đổi không gian trạng thái liên tục thành các vùng nguyên, giúp giảm số lượng trạng thái cần xét, làm cho việc kiểm chứng trở nên khả thi và hiệu quả hơn.

5. Làm thế nào để áp dụng kết quả nghiên cứu vào thực tế?
   Kết quả có thể được tích hợp vào các công cụ kiểm chứng mô hình hiện có hoặc phát triển các module mới, đồng thời áp dụng trong quy trình phát triển và kiểm thử phần mềm hệ thống thời gian thực để nâng cao độ tin cậy.

Kết luận

• Luận văn đã nghiên cứu và cải tiến thuật toán kiểm chứng tính đúng đắn của công thức khoảng bất biến tuyến tính (LDI) trong hệ thời gian thực, dựa trên mô hình ôtômat thời gian và kỹ thuật duyệt đồ thị trọng số.
• Thuật toán cải tiến giúp giảm đáng kể số lượng trạng thái và cạnh trong đồ thị kiểm chứng, từ đó rút ngắn thời gian xử lý trung bình hơn 60% so với thuật toán truyền thống.
• Kết quả kiểm chứng vẫn đảm bảo tính chính xác và đầy đủ, không bỏ sót các trường hợp không thoả mãn công thức LDI.
• Nghiên cứu mở ra hướng phát triển các công cụ kiểm chứng mô hình hiệu quả hơn, phù hợp với các hệ thống phức tạp và có không gian trạng thái lớn.
• 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 phức tạp hơn, hoàn thiện phần mềm kiểm chứng và tích hợp vào quy trình phát triển phần mềm thời gian thực.

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

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]: z 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. z 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 z 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.