Kiểm Chứng Hệ Thống Thời Gian Thực Bằng RT-Spin - Trường Đại Học Công Nghệ

I. Tổng Quan Về Kiểm Chứng Hệ Thống Thời Gian Thực RT Spin

Kiểm chứng mô hình là một kỹ thuật kiểm chứng tự động các hệ thống hữu hạn trạng thái. Phương pháp này xác minh tính đúng đắn của một mô hình bằng việc xác định xem các thuộc tính người dùng mong muốn có được thỏa mãn hay không. Về nguyên tắc, hệ thống cần kiểm chứng sẽ được mô hình hóa. Công cụ kiểm chứng sẽ kiểm tra mô hình có thỏa mãn các thuộc tính được cho hay không. Nhờ khả năng duyệt qua tất cả các trạng thái trong mô hình mà tính đúng đắn của kết quả kiểm chứng mô hình luôn được đảm bảo. Tuy nhiên cho đến nay, kiểm chứng mô hình chủ yếu tập trung vào các hệ phi thời gian hoặc các tính chất thời điểm của hệ thời gian thực, tính chất khoản vẫn còn ít và hầu như các thuật toán này chỉ giải quyết bài toán theo ngữ nghĩa đã thu hẹp của tính chất cần kiểm chứng.

Promela là ngôn ngữ mô hình mức cao nhằm đặc tả hệ thống. Thứ tự thời gian của các hành động trong chương trình Promela dựa trên trình tự của các lệnh trong tiến trình. Tuy nhiên ngôn ngữ không cho phép đo lường chính xác khoảng thời gian giữa hai sự kiện. Thực tế rất nhiều hệ thống bao gồm các giao thức giao tiếp, các mạch không đồng bộ, các bộ điều khiển đèn hay giao thông và các hệ thống thực hiện thời gian thực cần được mô tả như các hệ thống thời gian thực. Do đó thúc đẩy cần mở rộng Promela cho thời gian thực trong đó thời gian liên tục và số các sự kiện có thể xảy ra giữa hai khoảng thời gian không bị chặn. Hiện tại có hai công cụ tích hợp thời gian với Spin DtSpin và RtSpin. Cả hai công cụ đều dựa trên lý thuyết Otomat thời gian (timed Otomat). RtSpin có thể mô hình Otomat thời gian với các đồng hồ thời gian thực nhưng khá cồng kềnh. Hạn chế của RtSpin không tương thích với thuật toán giảm số lượng không gian trạng thái của hệ thống. DtSpin dựa trên Otomat thời gian lý tưởng, thời gian được chia thành các khoảng thời gian bằng nhau và thời gian được biểu thị là các số tự nhiên. DtSpin tương thích với thuật toán giảm số lượng không gian trạng thái của hệ thống. Tuy nhiên DtSpin chỉ mở rộng với thời gian rời rạc. Nội dung nghiên cứu: Tìm hiểu Spin, hệ thống thời gian thực, lý thuyết Otomat thời gian và tích hợp thời gian với công cụ Spin. Phần đầu của luận văn ta nghiên cứu về Spin, hệ thống thời gian thực và lý thuyết mô hình kiểm chứng. Ta cũng đưa ra những khái niệm cơ bản về kiểm chứng mô hình và hệ thống thời gian thực là cơ sở nền tảng để thực hiện tích hợp và các công cụ tích hợp thời gian thực với Spin nhằm định lượng khoảng thời gian giữa các sự kiện và các ràng buộc về thời gian. Hai công cụ này dựa trên lý thuyết Otomat thời gian. Trong đó RtSpin dựa trên mô hình thời gian liên tục, DtSpin dựa trên mô hình thời gian rời rạc. Cuối cùng ta đưa ra một số thực nghiệm với công cụ RtSpin và DtSpin bao gồm: mô hình train-gate-controller được đặc tả trong phần lý thuyết Otomat thời gian, bài toán này là bài toán kinh điển và là tiền đề để kiểm chứng các hệ thống điều khiển giao thông. Tiếp đến ta cũng kiểm chứng giáo thức truyền nhận song song dựa trên các kênh truyền và gửi thông thông báo có thể mất mát thông tin. Cuối cùng mô hình Sapi là mô hình có giá trị thực tiễn của hệ thống tính cước của G-Mobile

1.1. Giới Thiệu Phương Pháp Kiểm Chứng Mô Hình Cho RTS

Kiểm chứng mô hình là một kỹ thuật quan trọng để đảm bảo tính chính xác và độ tin cậy của các hệ thống thời gian thực (RTS). Nó giúp phát hiện lỗi thiết kế và xác minh rằng hệ thống đáp ứng các yêu cầu thời gian nghiêm ngặt. Kiểm chứng mô hình đặc biệt hữu ích trong việc xử lý tính đồng thời và tính không xác định trong các hệ thống phức tạp.

1.2. Vai Trò Của Ngôn Ngữ Promela Trong Mô Hình Hóa Hệ Thống

Promela là một ngôn ngữ mô hình hóa mức cao được sử dụng rộng rãi để đặc tả các hệ thống đồng thời. Nó cung cấp các cơ chế để mô tả các tiến trình, giao tiếp giữa các tiến trình và các thuộc tính của hệ thống. Tuy nhiên, Promela truyền thống không hỗ trợ đầy đủ các tính năng cần thiết để mô hình hóa các hệ thống thời gian thực.

1.3. DtSpin và RtSpin Các Công Cụ Tích Hợp Thời Gian Vào Spin

DtSpin và RtSpin là hai công cụ mở rộng Spin để hỗ trợ mô hình hóa và kiểm chứng các hệ thống thời gian thực. DtSpin dựa trên mô hình thời gian rời rạc, trong khi RtSpin dựa trên mô hình thời gian liên tục. Mỗi công cụ có ưu điểm và nhược điểm riêng, và sự lựa chọn công cụ phù hợp phụ thuộc vào đặc điểm của hệ thống được mô hình hóa.

II. Thách Thức và Vấn Đề Với Kiểm Định RTS Bằng RT Spin

Quá trình kiểm chứng dựa trên mô hình được bắt đầu bằng việc xác định yêu cầu của hệ thống từ đó xây dựng mô hình dựa vào các yêu cầu và chức năng của hệ thống. Việc xây dựng mô hình còn phải dựa trên các yếu tố dữ liệu đầu vào và đầu ra. Mô hình này được sử dụng để sinh ra các ca kiểm thử. Chúng ta có thể biết kết quả đầu ra mong đợi từ mô hình hoặc từ quy định chuẩn (oracle). Khi chạy kịch bản và kết quả thu được sẽ được so sánh với kết quả mong đợi. Từ đó quyết định hành động tiếp theo như sửa đổi mô hình hoặc dừng kiểm thử,… Các bước để thực hiện kiểm thử dựa trên mô hình. Xây dựng mô hình dựa trên các yêu cầu và chức năng của hệ thống. Tiếp đến tạo đầu ra dự kiến từ mô tả bài toán. Sau đó ta chạy kịch bản kiểm chứng và so sánh kết quả đầu ra thực tế với kết quả đầu ra dự kiến. Cuối cùng ta quyết định hành động tiếp theo (Sửa đổi mô hình, tạo thêm ca kiểm chứng, dừng kiểm chứng, đánh giá chất lượng của phần mềm).

2.1. Khó Khăn Trong Mô Hình Hóa Thời Gian Liên Tục Với RtSpin

RtSpin cho phép mô hình hóa thời gian liên tục, nhưng nó có thể trở nên cồng kềnh và phức tạp, đặc biệt đối với các hệ thống lớn. Việc quản lý và theo dõi các đồng hồ thời gian thực có thể gây khó khăn và làm tăng độ phức tạp của mô hình.

2.2. Hạn Chế Của RtSpin Trong Giảm Thiểu Không Gian Trạng Thái

Một trong những hạn chế chính của RtSpin là nó không tương thích với các thuật toán giảm thiểu không gian trạng thái. Điều này có thể dẫn đến 'bùng nổ trạng thái', làm cho quá trình kiểm chứng trở nên không khả thi đối với các hệ thống phức tạp.

2.3. Tính Chính Xác Của DtSpin Với Thời Gian Rời Rạc

DtSpin dựa trên mô hình thời gian rời rạc, điều này có thể làm giảm tính chính xác của mô hình, đặc biệt đối với các hệ thống yêu cầu độ chính xác cao về thời gian. Việc chia nhỏ thời gian thành các khoảng rời rạc có thể bỏ qua các chi tiết quan trọng và dẫn đến kết quả kiểm chứng không chính xác.

III. Phương Pháp Kiểm Chứng Tính Chất Thời Gian Thực Với RT Spin

Với Spin, ngôn ngữ Promela đựợc sử dụng để xây dựng mô hình của hệ thống và các tính chất của nó. Promela là ngôn ngữ không tất định, là một trong các ngôn ngữ có cú pháp và ngữ nghĩa tương tự ngôn ngữ C. Một chương trình Promela bao gồm khai báo định nghĩa kiểu, biến, kênh, một hay nhiều tiến trình, mỗi tiến trình chứa một chuỗi các câu lệnh. Các tiến trình có thể có tham số hoặc không.Các tiến trình đƣợc khai báo với từ khóa kích hoạt sẽ được khởi tạo và gán một giá trị pid (process id) duy nhất. Một tiến trình thực hiện đồng thời với các tiến trình khác và giao tiếp với các tiến trình khác bằng cách sử dụng biến chung phần hay giao tiếp qua các kênh. Trạng thái của tiến trình được đặc trưng bởi vị trị lệnh tiến trình đang thực hiện và nội dung của các biến. Tiến trình được khởi tạo bởi hàm run() hoặc khai báo kích hoạt khi định nghĩa tiến trình. Tiến trình không xác định thời gian thực hiện các lệnh, các tiến trình được giao nhau tuy nhiên các lệnh khác nhau của các tiến trình không xảy ra cùng lúc ngoại trừ kênh giao tiếp đồng thời. Mỗi tiến trình ở mỗi điểm có thể thực hiện lựa các hành đồng khác nhau. Một tiến trình bao gồm trình tự các câu lệnh. Mỗi câu lệnh có thể thực hiện được ngay lập tức hoặc không thực hiện được. Tất cả các câu lệnh là nguyên tử và khi thực hiện không giao với các tiến trình khác. Để kiểm chứng các tính chất chắc chắn đúng trong chương trình thường dùng lệnh assert (expr) trong mô hình Promela. Lệnh này luôn thực hiện được và nếu biểu thức trả vê 0 thì Spin thông báo một lỗi “has been violated”.

3.1. Sử Dụng Ngôn Ngữ Promela Để Đặc Tả Hệ Thống Thời Gian Thực

Để sử dụng RT-Spin, cần mô hình hóa hệ thống thời gian thực bằng ngôn ngữ Promela, bổ sung các tính năng hỗ trợ thời gian thực. Điều này bao gồm khai báo các đồng hồ, ràng buộc thời gian và các hành động phụ thuộc vào thời gian.

3.2. Mô Hình Hóa Các Ràng Buộc Thời Gian Sử Dụng RT Spin

RT-Spin cung cấp các cơ chế để mô hình hóa các ràng buộc thời gian trong hệ thống. Điều này có thể được thực hiện bằng cách sử dụng các biểu thức thời gian, các phép so sánh thời gian và các toán tử logic để mô tả các mối quan hệ thời gian giữa các sự kiện.

3.3. Kiểm Chứng Các Thuộc Tính Thời Gian Thực Sử Dụng LTL và CTL

RT-Spin cho phép kiểm chứng các thuộc tính thời gian thực của hệ thống bằng cách sử dụng các ngôn ngữ logic thời gian như LTL (Linear Temporal Logic) và CTL (Computation Tree Logic). Các thuộc tính này mô tả các hành vi mong muốn của hệ thống theo thời gian.

IV. Ứng Dụng RT Spin Để Kiểm Chứng Giao Thức Truyền Nhận Song Song

Trong chế độ giả lập, Spin biên dịch và chạy một chương trình promela, sau đó in ra các trạng thái của chương trình. Một trạng thái của chương trình là một bộ các giá trị gồm của các biến, các giá trị của biến đếm vị trí của các tiến trình. Một tính toán của chương trình là chuỗi các trạng thái bắt đầu bởi trạng thái khởi tạo và tiếp tục với những trạng thái xuất hiện khi mỗi câu lệnh được thực hiện. 1 biến n được khởi tạo với giá trị 0, chương trình bao gồm 2 tiến trình: P và Q tương ứng gán biến n giá trị 1 hoặc 2 và in ra giá trị của n cùng tên tiến trình. Chương trình với 2 tiến trình byte n=0; active proctype P(){ n=1; printf("Process P, n=%d\n",n); } active proctype Q() { n=2; printf("Process Q, n=%d\n",n); }

4.1. Mô Hình Hóa Giao Thức Truyền Nhận Song Song Với Promela

Sử dụng Promela để mô hình hóa các thành phần của giao thức truyền nhận song song, bao gồm các tiến trình gửi và nhận, các kênh truyền thông và các yếu tố thời gian liên quan đến việc truyền và xử lý dữ liệu.

4.2. Đặc Tả Các Thuộc Tính An Toàn Và Sống Động Của Giao Thức

Sử dụng LTL hoặc CTL để đặc tả các thuộc tính an toàn và sống động của giao thức truyền nhận song song. Ví dụ, thuộc tính an toàn có thể yêu cầu rằng không có thông báo nào bị mất, và thuộc tính sống động có thể yêu cầu rằng mọi thông báo được gửi cuối cùng sẽ được nhận.

4.3. Sử Dụng RT Spin Để Kiểm Chứng Tính Đúng Đắn Của Giao Thức

Sử dụng RT-Spin để kiểm chứng rằng mô hình Promela của giao thức truyền nhận song song đáp ứng các thuộc tính an toàn và sống động đã đặc tả. RT-Spin sẽ tự động khám phá không gian trạng thái của mô hình và tìm kiếm các vi phạm các thuộc tính.

V. Áp Dụng RT Spin Để Xác Minh Hệ Thống Tính Cước G Mobile Sapi

Với Spin có thể kiểm tra những loại tính chất: khóa chết (Deadlocks) là trạng thái có một tiến trình chiếm hữu tài nguyên lâu dài làm cho các tiến trình có nhu cầu sử dụng tài nguyên này luôn ở trạng thái đợi mãi mãi hay còn gọi trạng thái kết thúc không hợp lệ, tính khẳng định (assertions) là cách đơn giản để kiểm tra chương trình. Một assertion là một mệnh đề được đặt trong 1 chương trình mà ta cho rằng mệnh đề sẽ luôn đúng tại vị trí đó. Spin sẽ tính toán các assertion trong quá trình tìm kiếm phản ví dụ trong không gian trạng thái của chương trình, code không đạt được (unreachable code) là cách kiểm tra có những đoạn mã lệnh trong tiến trình nhưng không bao giờ được thực hiện, công thức LTL, tính chất sống động (liveness properties). Tính chất sống động bao gồm: không có vòng lặp tiến trình (non-progress cycles) và vòng lặp chấp nhận được (acceptance cycles). Khi kiểm tra tính chất không có vòng lặp tiến trình, bộ kiểm chứng sẽ cảnh báo nếu có một thực hiện không đi qua vô hạn lần trạng thái tiến trình. Trong đó trạng thái tiến trình là trạng thái hệ thống mà một số tiến trình đang thực hiện lệnh được gán nhãn với tiền tố "progress". Khi kiểm tra tính chất có vòng lặp chấp nhận được, bộ kiểm chứng sẽ cảnh báo nếu có một thực hiện đi qua vô hạn lần trạng thái chấp nhận được. Trong đó trạng thái chấp nhận được là trạng thái hệ thống mà một số tiến trình đang thực hiện lệnh được gán nhãn với tiền tố "acceptance".

5.1. Mô Hình Hóa Hệ Thống Tính Cước Sapi Bằng Ngôn Ngữ Promela

Sử dụng Promela để mô hình hóa các thành phần của hệ thống tính cước Sapi, bao gồm các tiến trình xử lý cuộc gọi, tính cước, cập nhật tài khoản và các yếu tố thời gian liên quan đến các hoạt động này.

5.2. Định Nghĩa Các Yêu Cầu Về Thời Gian Và Độ Chính Xác Của Sapi

Xác định các yêu cầu về thời gian và độ chính xác của hệ thống tính cước Sapi. Ví dụ, yêu cầu có thể là thời gian tính cước cho một cuộc gọi phải nhỏ hơn một ngưỡng nhất định, hoặc độ chính xác của việc tính cước phải đạt một mức độ nhất định.

5.3. Kiểm Chứng Hệ Thống Sapi Với RT Spin Đảm Bảo Độ Tin Cậy

Sử dụng RT-Spin để kiểm chứng rằng mô hình Promela của hệ thống tính cước Sapi đáp ứng các yêu cầu về thời gian và độ chính xác đã định nghĩa. RT-Spin sẽ giúp phát hiện các lỗi thiết kế có thể dẫn đến tính cước không chính xác hoặc chậm trễ trong quá trình tính cước.

VI. Kết Luận và Hướng Nghiên Cứu Tương Lai Về RT Spin

Trong chương này chúng tôi trình bày về mô hình kiểm thử với ngôn ngữ Promela và công cụ Spin. Kiểm chứng mô hình khảo sát tất cả các trạng thái có thể của hệ thống là kiểm tra rằng chúng chứa sự đúng đắn đã được đặc tả. Việc sinh ra các trạng thái và kiểm tra có thể được thực hiện một cách tự động bằng phần mềm và Spin là một trong những bộ kiểm chứng (model checker) được sử dụng rộng rãi. Các bộ kiểm chứng không kiểm tra trực tiếp chương trình mà kiểm tra một mô hình là thể hiện mức cao của hệ thống. Mô hình này mô tả hành vi của hệ thống. Để áp dụng được các công cụ kiểm chứng mô hình, việc đầu tiên là phải xây dựng mô hình của hệ thống. Các mô hình này cùng với đặc tả của thuộc tính cần kiểm tra là đầu vào của các bộ kiểm chứng. Chương này ta cũng giới thiệu về hệ thống thời gian thực. Ở phần sau chúng ta sẽ tìm hiểu sâu về otomat thời gian để mô hình hóa và kiểm chứng hệ thống thời gian thực.

6.1. Tổng Kết Các Kết Quả Đạt Được Khi Sử Dụng RT Spin

Tổng kết các kết quả đạt được khi sử dụng RT-Spin để kiểm chứng các hệ thống thời gian thực, bao gồm các ưu điểm, nhược điểm và các hạn chế của công cụ.

6.2. Đề Xuất Các Hướng Nghiên Cứu Phát Triển RT Spin

Đề xuất các hướng nghiên cứu phát triển RT-Spin để cải thiện khả năng mô hình hóa và kiểm chứng các hệ thống thời gian thực, bao gồm các kỹ thuật giảm thiểu không gian trạng thái, cải thiện hiệu suất kiểm chứng và hỗ trợ các tính năng thời gian thực phức tạp hơn.

6.3. So Sánh RT Spin Với Các Công Cụ Kiểm Chứng Mô Hình Khác

So sánh RT-Spin với các công cụ kiểm chứng mô hình khác như UPPAAL, NuSMV, PRISM để đánh giá vị trí của RT-Spin trong lĩnh vực kiểm chứng mô hình và xác định các điểm mạnh và điểm yếu của nó.

Luận văn: Kiểm Chứng Tính Chất Thời Gian Thực Hệ Thống Đồng Thời Bằng RT-Spin

Lời cảm ơn

Lời cam đoan

MỤC LỤC

Danh mục hình vẽ

Danh mục ký hiệu, từ viết tắt

1. Chƣơng 1: Mở đầu

2. Chƣơng 2 Cơ sở kiểm chứng mô hình

2.1. Kiểm chứng dựa trên mô hình

2. Các bƣớc thực hiện

2. Ngôn ngữ Promela và Spin

2.1. Ngôn Ngữ Promela

2. Giới thiệu về hệ thống thời gian thực

2. Đặc điểm của hệ thống thời gian thực

2. Cấu tạo hệ thời gian thực

2. Vì sao chọn hệ thời gian thực

3. Chƣơng 3 - Otomat thời gian

3.1. Otomat thời gian

3.2. Ngôn ngữ thời gian

3.3. Bảng chuyển trạng thái với các ràng buộc thời gian

3.4. Các ràng buộc đồng hồ và đồng hồ biên dịch

3.5. Các bảng chuyển trạng thái thời gian

3.6. Ngôn ngữ hình thức thời gian

3.7. Các tính chất của ngôn ngữ hình thức thời gian

3.8. Otomat Muller thời gian

3.9. Kiểm tra tính rỗng

3.9.1. Giới hạn đến các hằng nguyên

3.10. Các miền Đồng hồ

3.11. Cấu trúc không thời gian

3.12. Otomat thời gian xác định

3.13. Các tính chất đóng

3.14. Sự biểu cảm

3.15. Ví dụ về kiểm chứng

4. Chƣơng 4 Tích hợp thời gian với Spin

4.1. Mở rộng Spin và Promela với thời gian thực

4.2. Ngôn ngữ thời gian và Otomat Buchi thời gian

4.3. Ngữ nghĩa trong Promela không có thời gian và có thời gian

4.4. Mở rộng Spin với thời gian thực

4.5. Định nghĩa TBA dựa trên chƣơng trình Promela thời gian thực

4.6. Mở rộng Spin và Promela với thời gian rời rạc

4.7. Mô hình thời gian rời rạc

4.8. Cú pháp Spin với mô hình thời gian rời rạc

5. Chƣơng 5 Thực nghiệm Spin với hệ thống thời gian thực

5.1. Thực nghiệm kiểm chứng giao thức truyền và nhận thông báo song song

5.2. Thực nghiệm kiểm chứng giao thức hệ thống Sapi

5.3. Thực nghiệm kiểm chứng Train-Gate-Controller

TÀI LIỆU THAM KHẢO