Luận Văn Thạc Sĩ Về Kiểm Chứng Tự Động Các Hệ Thời Gian Thực Xác Suất

Luận văn thạc sĩ nghiên cứu kiểm chứng tự động các hệ thời gian thực xác suất luận văn ths máy tính 60 48 01, khảo sát thực trạng, phân tích nguyên nhân, đề xuất giải pháp cải

• Tác giả: Nguyễn Đức Thọ
• Người hướng dẫn: Tiến Sỹ Đặng Văn Hưng
• 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: Kiểm Chứng Tự Động Hệ Thời Gian Thực Xác Suất Trong Luận Văn Thạc Sĩ Máy Tính
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2016
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CAM ĐOAN
• LỜI CẢM ƠN
• 1. CHƯƠNG 1: CƠ SỞ KHOA HỌC CỦA ĐỀ TÀI
• 1.1. Xích Markov thời gian rời rạc (DTMC)
• 1.2. Quá trình quyết định Markov (MDP)
• 1.3. Xích Markov thời gian liên tục (CTMC)
• 2. CHƯƠNG 2: KIỂM CHỨNG TỰ ĐỘNG CÁC PTA
• 2.1. Các định nghĩa cho PTA
• 2.2. Đặc tả tính chất cho các PTA (properties specification for PTAs)
• 2.3. Các phương pháp kiểm chứng tự động PTA
• 2.3.1. Xây dựng đồ thị miền (region graph contruction)
• 2.3.2. Đồ thị miền biên (boundary region graph)
• 2.3.3. Phương pháp đồng hồ số (digital clock method)
• 2.3.4. Phương pháp đạt được lùi (backward reachability)
• 2.3.5. Làm mịn trừu tượng với trò chơi ngẫu nhiên (abstraction refinement with stochastic games)
• 2.3.6. So sánh các phương pháp kiểm chứng
• 2.3.7. Các cài đặt thực tế và công cụ hỗ trợ
• 2.4. Công cụ kiểm chứng mô hình PRISM
• 2.4.1. Giới thiệu công cụ PRISM
• 2.4.2. Sử dụng PRISM kiểm chứng các tính chất của PTA
• 3. CHƯƠNG 3: KIỂM CHỨNG MỘT SỐ PTA BẰNG PRISM
• 3.1. Kiểm chứng giao thức ABP
• 3.1.1. Giới thiệu giao thức bít luân phiên
• 3.1.2. Mô hình hóa giao thức ABP bằng PTA
• 3.2. Cài đặt hệ truyền tin ABP bằng công cụ PRISM
• 3.2.1. Kết quả kiểm chứng và các đánh giá
• 3.3. Hệ điều khiển tự động đường ngang
• 3.3.1. Mô hình hóa bằng PTA
• 3.3.2. Cài đặt trong PRISM
• 3.3.3. Kết quả kiểm chứng
• 3.3.3.1. Kiểm chứng Pmax = ?[F “success”]
• 3.3.3.2. Kiểm chứng Pmax = ?[F “safe”]
• 3.3.3.3. Kiểm chứng Pmax = ?[F “jam”]
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Giới thiệu về kiểm chứng tự động

Kiểm chứng tự động là một lĩnh vực quan trọng trong công nghệ thông tin, đặc biệt trong việc đảm bảo tính chính xác và độ tin cậy của các hệ thống phần mềm. Kiểm chứng tự động giúp phát hiện lỗi và xác minh các thuộc tính của hệ thống mà không cần sự can thiệp của con người. Trong bối cảnh hệ thời gian thực, việc kiểm chứng trở nên phức tạp hơn do sự tương tác giữa thời gian và xác suất. Các hệ thống này thường được mô hình hóa bằng ô tô mát thời gian xác suất (PTA), cho phép biểu diễn các hành vi ngẫu nhiên và các ràng buộc thời gian. Việc áp dụng các phương pháp kiểm chứng tự động cho các PTA giúp đảm bảo rằng các hệ thống này hoạt động đúng theo các yêu cầu đã định. Theo nghiên cứu, việc sử dụng công cụ kiểm chứng mô hình PRISM đã cho thấy hiệu quả cao trong việc kiểm chứng các thuộc tính của PTA, từ đó nâng cao độ tin cậy của các hệ thống phần mềm.

1.1. Tầm quan trọng của kiểm chứng tự động

Kiểm chứng tự động không chỉ giúp phát hiện lỗi mà còn giảm thiểu thời gian và chi phí phát triển phần mềm. Việc áp dụng các phương pháp kiểm chứng cho phép các nhà phát triển xác minh tính chính xác của các giao thức và hệ thống phức tạp. Đặc biệt, trong các lĩnh vực như khoa học máy tính, nơi mà các hệ thống thường phải hoạt động trong môi trường không chắc chắn, việc kiểm chứng tự động trở thành một yêu cầu thiết yếu. Các nghiên cứu đã chỉ ra rằng việc áp dụng các công nghệ thông tin hiện đại trong kiểm chứng tự động có thể cải thiện đáng kể hiệu suất và độ tin cậy của các hệ thống phần mềm.

II. Cơ sở lý thuyết về hệ thống thời gian thực xác suất

Hệ thống thời gian thực xác suất là một lĩnh vực nghiên cứu quan trọng trong khoa học máy tính, đặc biệt là trong việc mô hình hóa và kiểm chứng các hệ thống phức tạp. Các hệ thống này thường được mô hình hóa bằng xích Markov thời gian rời rạc (DTMC) và quá trình quyết định Markov (MDP). Các mô hình này cho phép biểu diễn các hành vi ngẫu nhiên và các quyết định trong môi trường không chắc chắn. Việc sử dụng ô tô mát thời gian xác suất giúp mô hình hóa các hệ thống có yếu tố ngẫu nhiên, từ đó cho phép kiểm chứng các thuộc tính của hệ thống một cách hiệu quả. Các nghiên cứu đã chỉ ra rằng việc áp dụng các phương pháp kiểm chứng tự động cho các PTA có thể giúp phát hiện lỗi và đảm bảo tính chính xác của các hệ thống trong thời gian thực.

2.1. Các loại chuỗi Markov

Chuỗi Markov là một công cụ mạnh mẽ trong việc mô hình hóa các hệ thống ngẫu nhiên. Có nhiều loại chuỗi Markov, bao gồm xích Markov thời gian rời rạc (DTMC) và xích Markov thời gian liên tục (CTMC). Mỗi loại chuỗi có những đặc điểm riêng và được áp dụng trong các tình huống khác nhau. DTMC thường được sử dụng trong các hệ thống mà thời gian chuyển trạng thái là rời rạc, trong khi CTMC được áp dụng cho các hệ thống mà thời gian chuyển trạng thái là liên tục. Việc hiểu rõ các loại chuỗi Markov này là rất quan trọng trong việc phát triển các phương pháp kiểm chứng tự động cho các hệ thống thời gian thực xác suất.

III. Phương pháp kiểm chứng tự động

Phương pháp kiểm chứng tự động cho các hệ thống thời gian thực xác suất thường bao gồm việc xây dựng các mô hình và áp dụng các thuật toán kiểm chứng. Các phương pháp như xây dựng đồ thị miền và phương pháp đồng hồ số đã được nghiên cứu và áp dụng rộng rãi. Việc sử dụng công cụ PRISM cho phép thực hiện kiểm chứng tự động các thuộc tính của PTA một cách hiệu quả. Các nghiên cứu đã chỉ ra rằng việc áp dụng các phương pháp này không chỉ giúp phát hiện lỗi mà còn cải thiện đáng kể độ tin cậy của các hệ thống phần mềm. Đặc biệt, việc kiểm chứng các giao thức như giao thức bít luân phiên đã cho thấy hiệu quả cao trong việc đảm bảo tính chính xác và độ tin cậy của hệ thống.

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

Các phương pháp kiểm chứng tự động bao gồm nhiều kỹ thuật khác nhau, từ việc xây dựng mô hình đến việc áp dụng các thuật toán kiểm chứng. Việc sử dụng các công cụ kiểm chứng mô hình như PRISM cho phép thực hiện kiểm chứng tự động các thuộc tính của hệ thống một cách hiệu quả. Các phương pháp như làm mịn trừu tượng và so sánh các phương pháp kiểm chứng đã được nghiên cứu để cải thiện độ chính xác và hiệu quả của quá trình kiểm chứng. Các nghiên cứu đã chỉ ra rằng việc áp dụng các phương pháp này có thể giúp phát hiện lỗi và đảm bảo tính chính xác của các hệ thống trong thời gian thực.

Nội dung chính

Tổng quan nghiên cứu

Trong bối cảnh phát triển nhanh chóng của các hệ thống thời gian thực có yếu tố xác suất, việc kiểm chứng tự động các thuộc tính của hệ thống trở thành một yêu cầu cấp thiết nhằm đảm bảo tính chính xác và độ tin cậy. Theo ước tính, các hệ thống này ngày càng được ứng dụng rộng rãi trong các lĩnh vực như mạng truyền thông, điều khiển tự động, và các hệ thống nhúng. Luận văn tập trung nghiên cứu kiểm chứng tự động các hệ thời gian thực xác suất thông qua mô hình Ô tô mát thời gian xác suất (Probability Timed Automata - PTA), một mô hình mở rộng của ô tô mát thời gian truyền thống với bổ sung các phân bố xác suất rời rạc. Mục tiêu chính của nghiên cứu là phát triển và áp dụng các phương pháp kiểm chứng tự động nhằm đánh giá các thuộc tính định lượng của hệ thống thời gian thực xác suất, đồng thời triển khai thực nghiệm trên công cụ kiểm chứng mô hình PRISM. Phạm vi nghiên cứu bao gồm các hệ thống mô hình hóa bằng PTA, với các đặc tính được biểu diễn bằng logic cây tính toán xác suất thời gian (PTCTL), tập trung vào các giao thức truyền thông có yếu tố ngẫu nhiên như giao thức Alternating Bit Protocol (ABP). Nghiên cứu có ý nghĩa quan trọng trong việc nâng cao hiệu quả kiểm chứng mô hình, giảm thiểu rủi ro trong thiết kế và vận hành các hệ thống phức tạp, đồng thời cung cấp cơ sở khoa học cho việc phát triển các công cụ kiểm chứng tự động trong lĩnh vực kỹ thuật phần mềm và công nghệ thông tin.

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 nền tảng lý thuyết của các quá trình Markov và ô tô mát thời gian xác suất để mô hình hóa và phân tích các hệ thống thời gian thực có yếu tố xác suất. Cụ thể:

• Chuỗi Markov thời gian rời rạc (DTMC): Mô hình hóa các quá trình chuyển trạng thái với xác suất chuyển đổi không phụ thuộc vào quá khứ, chỉ dựa trên trạng thái hiện tại. DTMC được sử dụng để biểu diễn các hành vi xác suất trong không gian trạng thái rời rạc.

• Quá trình quyết định Markov (MDP): Mở rộng DTMC bằng cách bổ sung các lựa chọn không xác định (nondeterministic choices), cho phép mô hình hóa các hệ thống có sự kết hợp giữa quyết định và xác suất.

• Ô tô mát thời gian xác suất (PTA): Mô hình hóa các hệ thống thời gian thực với các đồng hồ thời gian thực và các chuyển trạng thái xác suất. PTA kết hợp các ràng buộc thời gian với các phân bố xác suất, cho phép mô hình hóa các hệ thống có hành vi ngẫu nhiên và các ràng buộc thời gian phức tạp.

Các khái niệm chính bao gồm: đồng hồ thời gian, ràng buộc thời gian, cấu trúc thưởng (reward structure), logic cây tính toán xác suất thời gian (PTCTL) để biểu diễn các thuộc tính cần kiểm chứng, và các phương pháp kiểm chứng mô hình như đồ thị miền, phương pháp đồng hồ số, phương pháp đạt được lùi, và trừu tượng hóa với trò chơi ngẫu nhiên.

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

Nghiên cứu sử dụng phương pháp mô hình hóa hệ thống bằng PTA, kết hợp với các kỹ thuật kiểm chứng tự động trên công cụ PRISM. Cụ thể:

• Nguồn dữ liệu: Thu thập và tổng hợp các tài liệu nghiên cứu về các mô hình Markov, ô tô mát thời gian xác suất, và các kỹ thuật kiểm chứng mô hình. Dữ liệu thực nghiệm được lấy từ việc mô hình hóa và kiểm chứng giao thức Alternating Bit Protocol (ABP) trên công cụ PRISM.

• Phương pháp phân tích: Áp dụng các kỹ thuật kiểm chứng mô hình như phương pháp đồng hồ số, phương pháp đạt được lùi, và trừu tượng hóa với trò chơi ngẫu nhiên để đánh giá các thuộc tính xác suất và phần thưởng của hệ thống. Sử dụng logic PTCTL để biểu diễn các thuộc tính định lượng cần kiểm chứng.

• Timeline nghiên cứu: Quá trình nghiên cứu được thực hiện trong khoảng thời gian từ năm 2015 đến 2016, bao gồm các giai đoạn: tổng quan lý thuyết, phát triển mô hình PTA, cài đặt và kiểm chứng trên PRISM, phân tích kết quả và đề xuất giải pháp.

• Cỡ mẫu và chọn mẫu: Mô hình hóa hệ thống ABP với các tham số như số lượng bản tin DATA = 10, số lần retry từ 0 đến 30, các tỷ lệ mất gói tin và mất ACK được thiết lập theo các kịch bản thực tế để đánh giá hiệu quả kiểm chứng.

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

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

1. Xác suất thành công của giao thức ABP tăng theo số lần retry: Kết quả kiểm chứng trên PRISM cho thấy khi tăng số lần retry từ 0 đến 3, xác suất thành công (Pmax = ? [F "finished"]) tăng đáng kể, đạt mức ổn định khi retry ≥ 3. Ví dụ, với LOST_DATA_RATE = 0.1 và LOST_ACK_RATE = 0.24, xác suất thành công tăng từ khoảng 0.6 lên gần 0.95 khi retry tăng từ 0 lên 3.

2. Giảm thiểu xác suất mất gói tin khi tăng retry: Xác suất mất gói tin (Pmax = ? [F "lost"]) giảm nhanh khi số lần retry tăng, đặc biệt rõ rệt trong khoảng retry từ 0 đến 10. Với TIMEOUT = 150 và ACK_TIMEOUT = 5, xác suất mất gói tin giảm từ khoảng 0.4 xuống dưới 0.05 khi retry tăng lên 10.

3. Kích thước mô hình MDP tăng tuyến tính theo các tham số: Số lượng trạng thái, chuyển dịch và lựa chọn trong mô hình MDP tăng tuyến tính theo số lượng bản tin DATA và số lần retry. Ví dụ, với DATA = 10 và retry tăng từ 0 đến 4, số trạng thái tăng từ khoảng 393 lên 1745, số chuyển dịch tăng từ 1499 lên 48799.

4. Hiệu quả của các phương pháp kiểm chứng: Phương pháp đồng hồ số hoạt động hiệu quả với các mô hình PTA không chứa ràng buộc đường chéo và các ràng buộc đóng, trong khi phương pháp đạt được lùi và trừu tượng hóa với trò chơi ngẫu nhiên cho hiệu năng tốt hơn trong các trường hợp phức tạp hơn.

Thảo luận kết quả

Nguyên nhân của việc tăng xác suất thành công khi tăng retry là do khả năng gửi lại bản tin bị mất hoặc hỏng được cải thiện, giảm thiểu rủi ro mất dữ liệu. Tuy nhiên, khi số lần retry vượt quá một ngưỡng nhất định (khoảng 3 lần), xác suất thành công không tăng đáng kể do giới hạn thời gian TIMEOUT của hệ thống. Điều này phù hợp với các nghiên cứu trước đây về hiệu quả của các giao thức truyền thông có cơ chế retry.

Việc giảm xác suất mất gói tin khi tăng retry cũng phản ánh tính hiệu quả của cơ chế gửi lại trong giao thức ABP, giúp đảm bảo độ tin cậy truyền thông. Kích thước mô hình MDP tăng tuyến tính theo các tham số cho thấy sự phức tạp tính toán tăng theo quy mô hệ thống, đòi hỏi các kỹ thuật kiểm chứng tối ưu để đảm bảo khả năng mở rộng.

So sánh với các nghiên cứu khác, kết quả phù hợp với các báo cáo ngành về kiểm chứng mô hình xác suất, đồng thời khẳng định tính khả thi của việc áp dụng PTA và công cụ PRISM trong kiểm chứng các hệ thống thời gian thực xác suất. Việc trình bày dữ liệu qua biểu đồ xác suất thành công và mất gói tin theo số lần retry, cũng như bảng kích thước mô hình MDP, giúp minh họa rõ ràng các xu hướng và hiệu quả của các phương pháp kiểm chứng.

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

1. Tăng cường sử dụng phương pháp đồng hồ số cho các mô hình PTA không có ràng buộc đường chéo: Động từ hành động là áp dụng, mục tiêu là nâng cao hiệu quả kiểm chứng với các mô hình đơn giản, thời gian thực hiện trong vòng 6 tháng, chủ thể thực hiện là các nhóm nghiên cứu và phát triển phần mềm kiểm chứng.

2. Phát triển và tối ưu hóa phương pháp đạt được lùi và trừu tượng hóa với trò chơi ngẫu nhiên: Động từ hành động là cải tiến, nhằm mở rộng khả năng kiểm chứng các mô hình phức tạp hơn, thời gian 1 năm, chủ thể là các nhà phát triển công cụ kiểm chứng mô hình.

3. Áp dụng mô hình PTA và công cụ PRISM trong kiểm chứng các giao thức truyền thông thực tế: Động từ hành động là triển khai, mục tiêu là đánh giá và đảm bảo độ tin cậy của các hệ thống truyền thông, thời gian 6-12 tháng, chủ thể là các tổ chức nghiên cứu và doanh nghiệp trong lĩnh vực viễn thông.

4. Nâng cao khả năng mở rộng của công cụ kiểm chứng thông qua kỹ thuật biểu tượng và tổng hợp thông số: Động từ hành động là nghiên cứu và phát triển, nhằm giảm thiểu kích thước mô hình và tăng tốc độ kiểm chứng, thời gian 1 năm, chủ thể là các nhóm nghiên cứu công nghệ phần mềm.

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

1. Nhà nghiên cứu và sinh viên ngành Công nghệ Thông tin, Kỹ thuật Phần mềm: Học hỏi các phương pháp mô hình hóa và kiểm chứng hệ thống thời gian thực xác suất, áp dụng trong nghiên cứu và luận văn.

2. Kỹ sư phát triển phần mềm kiểm chứng mô hình: Áp dụng các kỹ thuật kiểm chứng tự động và công cụ PRISM để nâng cao chất lượng sản phẩm phần mềm.

3. Chuyên gia trong lĩnh vực mạng truyền thông và hệ thống nhúng: Hiểu rõ cơ chế hoạt động và kiểm chứng các giao thức truyền thông có yếu tố xác suất như ABP.

4. Doanh nghiệp và tổ chức nghiên cứu phát triển công nghệ: Sử dụng kết quả nghiên cứu để đảm bảo độ tin cậy và hiệu quả của các hệ thống thời gian thực trong sản phẩm và dịch vụ.

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

1. Ô tô mát thời gian xác suất (PTA) là gì?
   PTA là mô hình ô tô mát thời gian mở rộng với các phân bố xác suất rời rạc, dùng để mô hình hóa các hệ thống thời gian thực có yếu tố ngẫu nhiên và ràng buộc thời gian. Ví dụ, PTA có thể mô hình hóa giao thức truyền thông với các sự kiện mất gói tin ngẫu nhiên.

2. Tại sao cần kiểm chứng tự động các hệ thống thời gian thực xác suất?
   Kiểm chứng tự động giúp đảm bảo các thuộc tính quan trọng như độ tin cậy, an toàn và hiệu suất của hệ thống được thỏa mãn, giảm thiểu rủi ro lỗi trong thiết kế và vận hành. Ví dụ, xác suất thành công truyền tin trong giao thức ABP cần được đánh giá chính xác.

3. Công cụ PRISM hỗ trợ những phương pháp kiểm chứng nào cho PTA?
   PRISM hỗ trợ phương pháp đồng hồ số, phương pháp đạt được lùi và trừu tượng hóa với trò chơi ngẫu nhiên, cho phép kiểm chứng các thuộc tính xác suất và phần thưởng của PTA. Đây là các kỹ thuật đã được chứng minh hiệu quả trong thực tế.

4. Phương pháp đồng hồ số có giới hạn gì?
   Phương pháp đồng hồ số chỉ áp dụng cho các PTA không chứa ràng buộc đường chéo và các ràng buộc thời gian đóng, với giá trị đồng hồ là số nguyên. Điều này giới hạn phạm vi áp dụng nhưng giúp giảm kích thước mô hình và tăng tốc độ kiểm chứng.

5. Làm thế nào để lựa chọn số lần retry tối ưu trong giao thức ABP?
   Dựa trên kết quả kiểm chứng, số lần retry từ 3 đến 10 là hợp lý để đạt xác suất thành công cao mà không làm tăng quá mức độ phức tạp và thời gian truyền tin. Việc này cần cân nhắc cùng các tham số khác như TIMEOUT và tỷ lệ mất gói tin.

Kết luận

• Luận văn đã nghiên cứu và áp dụng thành công các phương pháp kiểm chứng tự động cho hệ thống thời gian thực xác suất dựa trên mô hình PTA.
• Công cụ PRISM được sử dụng hiệu quả để mô hình hóa và kiểm chứng giao thức truyền thông Alternating Bit Protocol với các tham số thực tế.
• Kết quả cho thấy số lần retry ảnh hưởng rõ rệt đến xác suất thành công và mất gói tin, đồng thời kích thước mô hình MDP tăng tuyến tính theo các tham số hệ thống.
• Các phương pháp kiểm chứng như đồng hồ số, đạt được lùi và trừu tượng hóa với trò chơi ngẫu nhiên có ưu nhược điểm riêng, cần lựa chọn phù hợp với đặc điểm mô hình.
• Đề xuất các hướng nghiên cứu tiếp theo bao gồm tối ưu hóa phương pháp kiểm chứng, mở rộng phạm vi áp dụng và nâng cao hiệu năng công cụ kiểm chứng.

Áp dụng các giải pháp đề xuất để phát triển công cụ kiểm chứng mô hình hiệu quả hơn, đồng thời mở rộng nghiên cứu sang các hệ thống phức tạp hơn trong thực tế.

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

MỞ ĐẦU Trong những năm gần đây, đã có nhiều nghiên cứu về các phương pháp kiểm chứng mô hình nhằm kiểm tra thuộc tính của các hệ thống, các giao thức tự động hoặc áp dụng để sinh các bộ kịch bản kiểm thử nhằm kiểm tra thuộc tính của các hệ thống. Việc kiểm chứng mô hình đòi hỏi các hệ thống cần được mô hình hóa và biểu diễn trên các không gian trạng thái, với nhiều kỹ thuật mô hình hóa khác nhau đã được nghiên cứu và triển khai, áp dụng trong thực tế. Việc biểu diễn các hệ thống được thực hiện bởi các ô tô mát, và các hành động trên các hệ thống được biểu diễn bởi các chuyển dịch trạng thái tương ứng trên ô tô mát, trong khi các thuộc tính cần kiểm chứng được biểu diễn bởi các mệnh đề logic. Kiểm chứng mô hình xác suất là dạng mở rộng của kiểm chứng mô hình, nhằm biểu diễn và kiểm chứng các tính chất của hệ thống trong đó việc chuyển trạng thái của hệ thống xảy ra có yếu tố xác suất, theo đó việc chuyển từ một trạng thái sang một hoặc nhiều trạng thái khác theo phân bổ xác suất.

Ô tô mát thời gian xác suất (PTA) là khái niệm mở rộng của Ô tô mát thời gian, bổ sung thêm phân bổ xác suất rời rạc, và có thể áp dụng để mô hình hóa các giao thức có yếu tố ngẫu nhiên, các hệ thống có khả năng chịu lỗi cũng như có thể áp dụng để mô hình hóa hệ thống trong nhiều lĩnh vực khác như kinh tế, kỹ thuật, sinh học,. Đề tài này tập trung vào việc nghiên cứu các đặc tính, mô hình hóa các hệ thời gian thực xác suất và khả năng áp dụng trong việc kiểm chứng mô hình nhằm kiểm chứng tự động các thuộc tính của hệ thời gian thực xác suất bằng công cụ. Phạm vi nghiên cứu của đề tài bao gồm: (1) nghiên cứu các tính chất Markov của các hệ thống, các loại chuỗi Markov và các tính chất của nó; (2) các hệ tự động thời gian thực xác suất và các phương pháp kiểm chứng tự động tính chất của hệ thời gian thực xác suất; (3) nghiên cứ công cụ kiểm chứng mô hình PRISM và khả năng áp dụng trong việc kiểm chứng các tính chất của hệ thời gian thực xác suất, (4) Áp dụng nghiên cứu trong việc mô hình hóa giao thức Alternative Bit Protocol bằng hệ thời gian thực xác suất và thực hiện cài đặt trên công cụ PRISM, thực hiện kiểm chứng tự động các tính chất của hệ thống bằng khả năng kiểm chứng của PRISM. TỔNG QUAN Hoạt động của một hệ thống máy tính, cũng như của bất kỳ một hệ thống nào trong các lĩnh vực khác như sinh học, hóa học, vật lý, … đều là chuyển đổi giữa các trạng thái khác nhau của hệ thống.

Nhà toán học người Nga Andrei Andreevich Markov (1856-1922) đã nghiên cứu một loại phân bổ xác suất quan trọng trong không gian trạng thái, đặt nền tảng cho một lớp các bài toán, mô hình chuyển trạng thái được gọi chung là không gian trạng thái Markov, hoặc các quá trình có tính chất Markov (Markov properties).Các quá trình có tính chất Markov được áp dụng rộng rãi trong các nghiên cứu cơ bản về hệ thống máy tính, cơ chế làm việc của các ô tô mát, hoặc việc mô hình hóa các hệ thống trong các lĩnh vực khác như sinh học, kinh tế, giao thông. Để bổ sung thêm giá trị thời gian, cũng như các ràng buộc thời gian đối với việc chuyển giữa các trạng thái trong thời gian thực, các nghiên cứu bổ sung sau này đã hoàn thiện các mô hình biểu diễn các ô tô mát thời gian, thực hiện bởi[1]với các giả thiết đồng hồ thời gian chính xác tuyệt đối và các hoạt động xảy ra ngay tức thì (độ trễ bằng 0 tuyệt đối). Các yếu tố xác suất được nghiên cứu và bổ sung trong biểu diễn ô tô mát thời gian, mở rộng thành mô hình biểu diễn ô tô mát thời gian xác suất, được định nghĩa bằng các phân bố thời gian rời rạc và các lựa chọn ngẫu nhiên cho các nhánh trong ô tô mát thời gian. Mô hình biểu diễn ô tô mát thời gian xác suất giúp có thể mô hình hóa các hệ thống ngoài đời thực, sử dụng các công cụ kiểm chứng để kiểm chứng các đặc tính của các hệ được biểu diễn.

Phạm vi đề tài nhằm nghiên cứu các tính chất của ô tô mát thời gian thực xác suất và thực hiện kiểm chứng tự động các tính chất đó bằng công cụ. Có thể phát biểu bài toán kiểm chứng mà đề tài cần giải quyết như sau: Cho hệ thống thời gian thực xác suất M. Thực hiện kiểm chứng tự động bằng công cụ xem M có thỏa mãn tính chất P hay không. Để có thể giải quyết bài toán kiểm chứng tự động bằng công cụ, phạm vi nghiên cứu của đề tài sẽ tập trung vào các nội dung chính bao gồm: 1.

Mô hình hóa hệ xác suất thời gian thực bằng ô tô mát thời gian thực xác suất PTA. Hình thức hóa các tính chất xác suất cần kiểm chứng bằng cây lô gic tính toán xác suất PCTL. Nghiên cứu công cụ hỗ trợ cài đặt PTA và biểu diễn tính chất để thực hiện kiểm chứng tự động. Áp dụng với nghiên cứu với giao thức Alternating Bit Protocol: Mô hình hóa hệ giao thức bằng PTA, hình thức hóa các tính chất bằng PCTL và thực hiện cài đặt hệ giao thức trên công cụ PRISM.

Cấu trúc trình bày của đề tài gồm sáu phần chính. Phần đầu là giới thiệu tổng quan về đề tài, phần hai là cơ sở khoa học của đề tài, nêu các biểu diễn và tính chất các quá trình Markov. Phần ba trình bày việc kiểm chứng tự động các ô tô mát thời gian thực xác suất, gồm các cú pháp và ngữ nghĩa các PTA, đặc tả tính chất cho PTA và các phương pháp kiểm chứng tự động đối với PTA. Phần bốn giới thiệu công cụ kiểm chứng mô hình PRISM, là công cụ có khả năng kiểm chứng tự động các tính chất của các hệ mô hình hóa khác nhau trong đó có PTA.

Phần năm trình bày một trường hợp áp dụng PTA để mô hình hóa hệ giao thức Alternating Bit Protocol và hình thức hóa các tính chất của ABP, cài đặt bằng công cụ PRISM và kiểm chứng tự động các tính chất của ABP. Phần cuối cùng là phần kết luận, đề xuất các hướng nghiên cứu mở rộng của đề tài. CƠ SỞ KHOA HỌC CỦA ĐỀ TÀI Giới thiệu chung về chuỗi Markov Chuỗi Markov (Markov chain hay Markov process) là một quá trình ngẫu nhiên với các đặc tính Markov. Thuật ngữ “chuỗi Markov” (hay “xích Markov”, “quá trình Markov”) dành để chỉ trình tự các biến ngẫu nhiên mà một tiến trình trải qua, với đặc tính Markov được định nghĩa là khả năng xuất hiện của các biến ngẫu nhiên tiếp theo chỉ phụ thuộc vào biến hiện tại (tạo thành 1 chuỗi).

Khi áp dụng trong không gian trạng thái, nó có thể được dùng để mô tả các hệ thống có các chuỗi trạng thái liên kết với nhau, và những biến đổi sang trạng thái tiếp theo chỉ phụ thuộc trạng thái hiện tại của hệ thống. Quá trình có tính chất Markov Một quá trình là một ô tô mát (hay quá trình, hoặc một chuỗi trạng thái) bắt đầu với một trong các trạng thái này và dịch chuyển từ trạng thái này sang trạng thái khác. Nếu ô tô mát đang ở trạng thái si, sau đó chuyển sang trạng thái sj ở bước tiếp theo với xác suất được biểu diễn bằng pij, và giá trị này không phụ thuộc vào các trạng thái ô tô mát trước khi chuyển sang trạng thái hiện tại. Các giá trị xác suất pij được gọi là các xác suất chuyển (transition probability).

Ô tô mát có thể ở trạng thái hiện tại, với xác suất được ghi nhận là pii. Việc phân bố xác suất các trạng thái ban đầu được định nghĩa bởi S. Thông thường các trạng thái ban đầu được xác định bởi một hoặc một số trạng thái, trong đó nếu các phân bố xác suất chuyển từ trạng thái hiện tại sang các trạng thái tiếp theo chỉ phụ thuộc vào trạng thái hiện tại thì quá trình như vậy được gọi là có tính chất Markov, gọi ngắn gọn là Quá trình Markov. pn+1 = Pr(sn+1 = x | s1 = x1, s2 = x2, ., sn = xn) = Pr(sn+1 = x | sn = xn) 2.1 Xích Markov thời gian rời rạc (DTMC) Định nghĩa Hình 2.1 là minh họa cho một xích Markov (hay một chuỗi Markov) đơn giản, với 3 trạng thái s0, s1, s2 và xác suất chuyển giữa các trạng thái thể hiện trên các đường nối giữa các trạng thái.

DTMClà quá trình biến đổi trạng thái rời rạc, thuần nhất theo thời gian. Khái niệm thuần nhất theo thời gian được hiểu là xác suất pij chuyển trạng thái từ si sang sj của chuỗi Markov là giá trị không phụ thuộc thời z 12 gian. Nói cách khác tại mọi thời điểm được xét, giá trị xác suất pij không thay đổi.1: Markov chain Khái niệm tập không gian trạng thái trong chuỗi Markov không được thống nhất về phạm vi giới hạn trong các tài liệu khác nhau, không gian trạng thái có thể dùng để biểu diễn quá trình xảy ra với bất kỳ dạng biến đổi nào, do vậy có thể là không gian hữu hạn hoặc vô hạn, đếm được hoặc không đếm được. Tuy nhiên, phần lớn các ứng dụng chuỗi Markov chỉ sử dụng tập không gian trạng thái hữu hạn, hoặc tập không gian trạng thái vô hạn đếm được, có các đặc điểm phân tích thống kê đơn giản hơn.

Vector xác suất Vector xác suất với r thành phần là một vector dòng với các giá trị không âm, và tổng các giá trị là 1. Gọi u là vector xác suất biểu diễn trạng thái ban đầu của chuỗi Markov, khi đó thành phần thứ i của u biểu thị xác suất chuỗi Markov sẽ bắt đầu ở trạng thái si. Ma trận xác suất (còn gọi là ma trận chuyển – transition matrix) Giá trị pij cho biết xác suất chuyển từ trạng thái i sang trạng thái j. Do xác suất là giá trị không âm, và hệ sẽ phải chuyển đến một trạng thái nào đó, ta có: pij≥ 0, i, j ≥ 0; = 1, i = 0, 1, ….

r Ma trận P kích thước r x r gồm các phần tử pij là ma trận chuyển của chuỗi Markov có r+1 trạng thái. z 13 … … … … … … … Chuỗi Markov hấp thụ (absorbing Markov chain) Một trạng thái si của chuỗi Markov được gọi là trạng thái hấp thụ (absorbing) nếu chuỗi không thể thoát ra khỏi trạng thái đó (pii = 1).