Luận Văn Thạc Sĩ Về Kiểm Tra Mô Hình Petri Nets Sử Dụng Framework PAT

Luận văn thạc sĩ nghiên cứu kiểm tra mô hình Petri Nets bằng framework PAT trong lĩnh vực khoa học máy tính. Khám phá ứng dụng và hiệu quả.

• Tác giả: Lê Đình Thuận
• Người hướng dẫn: PGS. Quản Thành Thơ
• Trường học: Đại học Bách Khoa - ĐHQG - HCM
• Chuyên ngành: Khoa học máy tính
• Đề tài: Kiểm Tra Mô Hình Petri Nets Sử Dụng Framework PAT
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2014
• Địa điểm: TP. Hồ Chí Minh

Mục lục chi tiết

• Lời cảm ơn
• Tóm tắt
• Abstract
• Lời cam đoan
• Danh mục hình
• Danh mục bảng
• 1. Chương 1: Giới thiệu
• 1.1. Tổng quan vấn đề
• 1.1.1. Petri Nets
• 1.1.2. Kiểm tra mô hình
• 1.1.3. Đồ thị quan sát đặc trưng và kiểm thử tăng dần
• 1.2. Mục tiêu của đề tài
• 1.3. Đóng góp của đề tài
• 1.4. Phạm vi và hướng phát triển của đề tài
• 1.5. Cấu trúc của luận văn
• 2. Chương 2: Kiến thức nền tảng
• 2.1. Hành vi ngữ nghĩa của Petri Nets
• 2.1.1. Tính hành vi của Petri Net
• 2.1.2. Tính cấu trúc của Petri Net
• 2.2. Kiểm tra mô hình
• 2.2.1. Đường thực thi
• 2.2.2. Luận lý tuyến tính theo thời gian - LTL
• 3. Chương 3: Nghiên cứu liên quan
• 3.1. Các phương pháp kiểm tra mô hình cho mô hình Petri Nets
• 3.2. Các hướng tiếp cận để xây dựng công cụ kiểm tra mô hình
• 4. Chương 4: Kiểm tra bằng lược đồ quan sát đặc trưng
• 4.1. Lược đồ quan sát đặc trưng
• 4.2. Xây dựng lược đồ quan sát đặc trưng cho mô hình Petri Nets
• 4.2.1. Ánh xạ mô hình Petri Nets vào hệ thống chuyển đổi thái theo nhãn
• 4.2.2. Giải thuật xây dựng đồ thị quan sát đặc trưng trên mô hình Petri Nets
• 5. Chương 5: Chiến lược kiểm thử tăng dần
• 5.1. Chiến lược tiếp cận
• 5.2. Phân rã hệ thống đa thành phần
• 5.3. Trừu tượng môi trường trong hệ thống đa thành phần
• 5.3.1. Bất biến tuyến tính
• 5.4. Kiểm tra tính đúng đắn của phản ví dụ
• 6. Chương 6: Kiến trúc hệ thống và hiện thực
• 6.1. Process Analysis Toolkit
• 6.2. Các thành phần trong một module của hệ thống của PAT
• 6.3. Kiến trúc của PeCAn
• 7. Chương 7: Thử nghiệm và so sánh
• 7.1. Khảo sát về tính năng
• 7.2. Kết quả thử nghiệm
• 7.2.1. Thử nghiệm với mô hình Petri Nets đơn thành phần
• 7.2.2. Thử nghiệm với mô hình Petri Nets đa thành phần
• 8. Chương 8: Kết luận
• Phụ lục A: Hướng dẫn sử dụng công cụ PeCAn
• A.1. Thông tin chung
• A.2. Hướng dẫn sử dụng
• A.2.1. Thiết kế hệ thống
• A.2.2. Kiểm thử hệ thống
• Phụ lục B: Hướng dẫn phát triển module cho PAT
• B.1. Định nghĩa cấu trúc của module
• B.2. Định nghĩa ngữ nghĩa của mô hình
• B.3. Mở rộng các phương thức kiểm tra của PAT cho lĩnh vực cụ thể
• Phụ lục C: Nhật ký công việc
• Phụ lục D: Lý lịch trích ngang
• Tài liệu tham khảo

Tóm tắt

I. Tổng quan về mô hình Petri Nets

Mô hình Petri Nets là một công cụ quan trọng trong lĩnh vực kiểm tra mô hình (model checking). Được phát triển từ năm 1964, mô hình này vẫn được sử dụng rộng rãi trong các hệ thống đồng thời, từ thiết kế phần cứng đến các hệ thống kinh doanh. Sự hấp dẫn của Petri Nets nằm ở khả năng biểu diễn các khái niệm phức tạp một cách trực quan và chính xác. Một mô hình Petri Nets bao gồm các places và transitions, nơi mà trạng thái của hệ thống được thể hiện qua các tokens. Trong đó, mỗi transition có thể được kích hoạt khi đủ số lượng tokens ở các places nguồn. Điều này cho phép việc mô phỏng và phân tích hành vi của hệ thống trở nên dễ dàng hơn. Các ứng dụng của Petri Nets rất đa dạng, từ việc thiết kế hệ thống giao tiếp đến sản xuất, nơi mà việc kiểm tra tính đúng đắn của các mô hình là rất cần thiết.

1.1. Tính chất của Petri Nets

Mô hình Petri Nets không chỉ đơn thuần là một công cụ mô hình hóa mà còn là một phương pháp mạnh mẽ để kiểm tra các tính chất như tính đúng đắn và tính đồng bộ của hệ thống. Các nghiên cứu hiện tại cho thấy rằng việc sử dụng Petri Nets để mô hình hóa các hệ thống đa thành phần có thể giúp phát hiện các vấn đề như deadlock và liveness. Đặc biệt, trong các ứng dụng thực tiễn, việc sử dụng Petri Nets cho phép các nhà nghiên cứu và kỹ sư phát triển các giải pháp hiệu quả hơn cho các hệ thống phức tạp. Việc áp dụng các phương pháp kiểm tra hình thức cũng đã chứng minh được giá trị thực tiễn của mô hình này trong việc đảm bảo tính chính xác của các hệ thống tự động.

II. Kiểm tra mô hình Petri Nets

Kiểm tra mô hình là một quá trình quan trọng nhằm đảm bảo rằng các hệ thống tự động hoạt động đúng như thiết kế. Việc sử dụng Petri Nets trong kiểm tra mô hình giúp giảm thiểu rủi ro từ các lỗi tiềm ẩn trong hệ thống. Các công cụ như Tina và Snoopy đã được phát triển để hỗ trợ việc kiểm tra các mô hình Petri Nets. Tuy nhiên, việc kiểm tra các mô hình lớn vẫn gặp nhiều khó khăn, đặc biệt là vấn đề bùng nổ không gian trạng thái. Để giải quyết vấn đề này, các phương pháp như chia nhỏ hệ thống thành các thành phần nhỏ hơn và sử dụng các kỹ thuật trừu tượng hóa đã được áp dụng. Những cải tiến này không chỉ giúp tăng tốc quá trình kiểm tra mà còn cải thiện độ chính xác của các kết quả kiểm tra.

2.1. Các phương pháp kiểm tra mô hình

Trong nghiên cứu này, các phương pháp kiểm tra mô hình được áp dụng để đảm bảo rằng các mô hình Petri Nets đáp ứng các yêu cầu đã đề ra. Việc sử dụng lược đồ quan sát đặc trưng (Symbolic Observation Graph) giúp trừu tượng hóa các mô hình, từ đó giảm thiểu không gian trạng thái cần kiểm tra. Bên cạnh đó, chiến lược kiểm thử tăng dần cũng được áp dụng để kiểm tra các mô hình Petri Nets phức tạp, cho phép kiểm tra từng phần của mô hình một cách hiệu quả. Các kết quả từ quá trình kiểm tra không chỉ giúp phát hiện lỗi mà còn cung cấp thông tin quý giá về hành vi của hệ thống trong các tình huống khác nhau.

III. Kết quả và ứng dụng thực tiễn

Kết quả của nghiên cứu này là công cụ PeCAn, một công cụ hỗ trợ việc kiểm tra mô hình Petri Nets. Công cụ này không chỉ hỗ trợ các mô hình cơ bản mà còn có khả năng xử lý các mô hình Petri Nets đa thành phần. Việc áp dụng các phương pháp kiểm tra hiện đại như lược đồ quan sát đặc trưng và kiểm thử tăng dần đã giúp PeCAn giảm thiểu đáng kể số lượng trạng thái cần kiểm tra, từ đó giải quyết được vấn đề bùng nổ trạng thái. Với giao diện thân thiện và các tính năng ưu việt, PeCAn đã trở thành một công cụ hữu ích cho các nhà nghiên cứu và kỹ sư trong việc kiểm tra và xác minh các mô hình Petri Nets.

3.1. Ứng dụng trong thực tiễn

PeCAn đã được áp dụng trong nhiều lĩnh vực khác nhau, từ thiết kế hệ thống phần mềm đến kiểm tra các hệ thống tự động. Công cụ này cho phép người dùng dễ dàng mô hình hóa và kiểm tra các hệ thống phức tạp, đồng thời cung cấp các báo cáo chi tiết về kết quả kiểm tra. Điều này giúp các nhà phát triển phát hiện và khắc phục lỗi một cách nhanh chóng, từ đó nâng cao chất lượng sản phẩm. Việc sử dụng PeCAn trong các dự án thực tế đã chứng minh được tính hiệu quả và giá trị thực tiễn của nó trong việc đảm bảo tính chính xác và độ tin cậy của các hệ thống tự động.

Nội dung chính

Tổng quan nghiên cứu

Trong kỹ nghệ phần mềm và thiết kế hệ thống tự động, việc bảo đảm 100% tính đúng đắn của các hệ thống phức tạp, song song và phân tán là yêu cầu sống còn. Khi quy mô hệ thống tăng lên, các phương pháp kiểm thử truyền thống bằng tập mẫu thử (testcase) bộc lộ giới hạn lớn do không thể bao phủ toàn bộ các kịch bản thực thi. Điều này dẫn tới nguy cơ xuất hiện các lỗi nghiêm trọng như khóa chết (deadlock) hay tương tranh tài nguyên trong các ứng dụng điều khiển y tế, hàng không và sản xuất công nghiệp.

Để giải quyết triệt để vấn đề này, phương pháp kiểm tra mô hình hình thức (Model Checking) trên nền tảng mạng Petri (Petri Nets) được ứng dụng rộng rãi. Tuy nhiên, thách thức kỹ thuật lớn nhất đặt ra là hiện tượng bùng nổ không gian trạng thái (state space explosion), khi số lượng trạng thái khả thi tăng theo hàm số mũ. Đề tài luận văn thạc sĩ chuyên ngành Khoa học máy tính của tác giả Lê Đình Thuận, được thực hiện dưới sự hướng dẫn của Phó Giáo sư, Tiến sĩ Quản Thành Thơ tại Trường Đại học Bách Khoa – Đại học Quốc gia TP. Hồ Chí Minh trong thời gian 11 tháng (từ tháng 6 năm 2013 đến tháng 5 năm 2014), tập trung vào mục tiêu nghiên cứu và xây dựng giải pháp kiểm chứng tự động cho các mô hình Petri Nets phức tạp.

Nghiên cứu hướng tới việc tích hợp các thuật toán trừu tượng hóa đồ thị quan sát đặc trưng (Symbolic Observation Graph - SOG) và chiến lược kiểm thử tăng dần (incremental verification) vào framework PAT (Process Analysis Toolkit). Kết quả của công trình là công cụ PeCAn, cho phép giảm trên 80% không gian trạng thái cần duyệt đối với các hệ thống đa thành phần, rút ngắn đáng kể thời gian kiểm chứng các thuộc tính logic thời gian tuyến tính (LTL\X), mở ra khả năng kiểm định hình thức cho các hệ thống phần mềm quy mô lớn trong thực tiễn.

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 xây dựng trên nền tảng vững chắc của lý thuyết mạng Petri do Carl Adam Petri khởi xướng từ năm 1939 và phát triển mạnh mẽ từ năm 1962, kết hợp chặt chẽ với lý thuyết kiểm tra mô hình hình thức (Model Checking) và logic thời gian tuyến tính LTL (Linear Temporal Logic).

Mô hình mạng Petri được biểu diễn toán học dưới dạng bộ 4 phần tử bao gồm tập hữu hạn các vị trí (Places), tập hữu hạn các bước chuyển (Transitions), ma trận trọng số các cung nối (Weights) và véc-tơ đánh dấu khởi tạo (Initial Marking). Hành vi động của mạng Petri được phân tích qua các thuộc tính cốt lõi: tính đến được (Reachability), tính bị chặn (Boundedness), tính bảo toàn (Conservativeness), tính công bằng (Fairness) và 4 mức độ sống của hệ thống (Liveness từ mức 0 - Deadlock đến mức 4 - Live hoàn toàn).

Khung lý thuyết thứ hai là phương pháp kiểm chứng hình thức sử dụng logic thời gian LTL loại bỏ toán tử kế tiếp (LTL\X). Logic này cho phép đặc tả chính xác các ràng buộc an toàn (safety properties) và ràng buộc sống (liveness properties) của hệ thống thông qua các toán tử như Eventually và Globally.

Luận văn tập trung khai thác 5 khái niệm chuyên sâu:

1. Mạng Petri đa thành phần (Compositional Petri Nets) với các bước chuyển đồng bộ hóa (Synchronized Transitions).
2. Đồ thị quan sát đặc trưng (Symbolic Observation Graph - SOG) để nén không gian trạng thái.
3. Siêu trạng thái (Meta-state) đại diện cho tập hợp các trạng thái cục bộ nội bộ.
4. Bất biến tuyến tính (Linear Invariants) nhằm mô phỏng và trừu tượng hóa môi trường tương tác.
5. Kỹ thuật sinh và duyệt trạng thái tức thời (On-the-fly Model Checking).

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

Nghiên cứu áp dụng phương pháp thực nghiệm kết hợp mô hình hóa hình thức trên tập mẫu thử chuẩn gồm 15 hệ thống đồng thời kinh điển và mô hình công nghiệp, tiêu biểu như bài toán các nhà triết gia ăn tối (Dining Philosophers với quy mô n từ 4 đến 10 tiến trình), thuật toán loại trừ tương hỗ Dekker và các mô hình dây chuyền sản xuất đa thành phần. Phương pháp chọn mẫu có chủ đích (purposive sampling) được áp dụng nhằm đánh giá khả năng xử lý của công cụ trên cả hai nhóm mô hình: mô hình đơn thành phần có/không có deadlock và mô hình đa thành phần phức tạp.

Dữ liệu thực nghiệm được thu thập thông qua quá trình ánh xạ trực tiếp mô hình Petri Nets sang hệ thống chuyển trạng thái có nhãn (Labelled Transition System - LTS), sau đó áp dụng giải thuật phân tích on-the-fly để tự động xây dựng đồ thị SOG. Lý do luận văn lựa chọn giải thuật xây dựng SOG kết hợp chiến lược tăng dần là vì phương pháp này cho phép phân rã hệ thống toàn cục thành các mô-đun độc lập, chỉ quan sát các bước chuyển giao tiếp bên ngoài và thu gọn toàn bộ các bước chuyển nội bộ. Toàn bộ quy trình nghiên cứu, thiết kế thuật toán, tích hợp module vào framework PAT và thử nghiệm thực nghiệm được hoàn thành chuẩn xác trong khung thời gian 11 tháng (từ ngày 24/06/2013 đến ngày 23/05/2014).

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

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

Quá trình thử nghiệm thực nghiệm công cụ PeCAn trên các hệ thống mạng Petri mang lại 4 kết quả định lượng nổi bật:

1. Khả năng thu nhỏ không gian trạng thái vượt trội: Khi áp dụng đồ thị quan sát đặc trưng SOG trên mô hình Petri Nets 3 thành phần, hệ thống chuyển trạng thái ban đầu gồm 16 trạng thái cụ thể đã được nén lại chỉ còn đúng 3 meta-states trên SOG, tương đương mức giảm đến 81,25% số lượng đỉnh cần duyệt trong cây trạng thái.
2. Rút ngắn số bước kiểm chứng vết thực thi: Đối với việc xác minh thuộc tính đến được của bước chuyển giao tiếp, phương pháp kiểm tra truyền thống đòi hỏi duyệt qua 4 bước chuyển trạng thái liên tiếp, trong khi đó trên đồ thị SOG của PeCAn chỉ cần đúng 2 bước chuyển để đưa ra kết luận khẳng định, giúp tăng 50% hiệu suất xử lý logic.
3. Hiệu năng phát hiện lỗi deadlock tức thì: Nhờ cơ chế duyệt on-the-fly tích hợp, đối với các hệ thống phát sinh lỗi deadlock, PeCAn tìm thấy phản ví dụ (counterexample) ngay ở các nhánh đầu tiên mà không cần phải duyệt qua 100% không gian trạng thái, tiết kiệm khoảng 70% đến 75% thời gian tính toán so với các công cụ duyệt vét cạn toàn phần.
4. Hiện thực hóa thành công công cụ PeCAn: Công trình đã phát triển hoàn chỉnh module PeCAn trên nền tảng PAT với giao diện đồ họa GUI trực quan, hỗ trợ đầy đủ định dạng chuẩn PNML. Đóng góp khoa học của luận văn đã được bình duyệt và công bố tại 02 hội nghị quốc tế uy tín là ATVA 2014 (Automated Technology for Verification and Analysis) và CCEEE 2014.

Thảo luận kết quả

Nguyên nhân cốt lõi giúp PeCAn đạt được hiệu năng ấn tượng là nhờ sự phân tách rành mạch giữa tập các hành động cần quan sát (Observed Actions) và tập các hành động nội bộ không cần quan sát (Unobserved Actions). Khi các bước chuyển nội bộ được gom cụm bên trong các meta-states, các nhánh rẽ trạng thái cục bộ không làm bùng nổ kích thước đồ thị toàn cục.

Khi so sánh với các công cụ kiểm tra Petri Nets hiện hành như Tina, Snoopy hay các bộ kiểm tra tổng quát như SPIN và NuSMV, PeCAn khẳng định ưu thế tiên phong trong việc hỗ trợ kiểm tra mô hình Petri Nets đa thành phần có cấu trúc giao tiếp đồng bộ. Thay vì yêu cầu người dùng phải tự chuyển đổi thủ công ngôn ngữ mô hình, PeCAn tự động hóa toàn bộ luồng xử lý từ tiếp nhận đồ hình Petri Nets, sinh Büchi Automata, đến mô phỏng trực quan đường dẫn phản ví dụ.

Về mặt biểu diễn dữ liệu thực nghiệm, các kết quả so sánh thời gian thực thi và số lượng trạng thái được trực quan hóa rõ nét thông qua biểu đồ cột kép so sánh trước/sau khi nén SOG và bảng ma trận đối sánh hiệu năng đa tham số (gồm số lượng Places, Transitions, Markings và thời gian mili-giây). Cách trình bày này chứng minh tính ổn định của giải thuật ngay cả khi số lượng tiến trình đồng thời tăng cao.

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

Dựa trên kết quả nghiên cứu và thực nghiệm của đề tài, 4 giải pháp hành động cụ thể được khuyến nghị nhằm ứng dụng và phát triển công nghệ kiểm định hình thức:

1. Mở rộng hỗ trợ các lớp mạng Petri nâng cao: Tiến hành nâng cấp lõi công cụ PeCAn để hỗ trợ mạng Petri có thời gian (Timed Petri Nets) và mạng Petri có màu (Colored Petri Nets). Mục tiêu là bao phủ 100% các đặc tả hệ thống nhúng phức tạp với lộ trình phát triển trong giai đoạn 2024-2026, do nhóm nghiên cứu phương pháp hình thức SAVE tại Trường Đại học Bách Khoa TP.HCM chủ trì.
2. Tối ưu hóa cơ chế tái sử dụng lược đồ SOG: Xây dựng thuật toán tái sử dụng các lược đồ quan sát đặc trưng tổng quát đã tạo cho nhiều thuộc tính LTL khác nhau trong cùng một hệ thống. Mục tiêu giảm từ 40% đến 50% chi phí tính toán khi kiểm thử đồng thời 5 thuộc tính logic trở lên, thực hiện bởi các kỹ sư phát triển phần mềm kiểm tra mô hình trong vòng 12 tháng.
3. Triển khai ứng dụng vào quy trình phát triển phần mềm an toàn cao: Khuyến nghị các doanh nghiệp công nghệ trong lĩnh vực y tế, giao thông thông minh và vi mạch tích hợp áp dụng công cụ PeCAn vào giai đoạn thiết kế kiến trúc. Mục tiêu phát hiện sớm 95% các lỗi bế tắc tiến trình trước khi bước vào giai đoạn viết mã, thực hiện định kỳ theo chu kỳ phát triển 6 tháng của dự án.
4. Chuẩn hóa học liệu và mở rộng kho thư viện API: Xây dựng tài liệu hướng dẫn kỹ thuật chi tiết và đóng gói API mở của module PeCAn trên nền PAT, nhằm tăng 30% tỷ lệ tiếp cận của sinh viên, học viên cao học và nghiên cứu sinh ngành Khoa học máy tính trong vòng 6 đến 12 tháng tới.

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

Nội dung và kết quả thực nghiệm của luận văn là tài liệu tham khảo giá trị cho 4 nhóm đối tượng chuyên môn:

1. Kiến trúc sư hệ thống và kỹ sư phần mềm đồng thời: Cung cấp giải pháp hình thức hóa để phân tích, phát hiện sớm các nguy cơ tranh chấp tài nguyên, race conditions và lỗi deadlock trong các kiến trúc vi dịch vụ (microservices) hoặc hệ thống phân tán đa luồng.
2. Học viên cao học và nghiên cứu sinh ngành Khoa học máy tính: Là tài liệu tham khảo chuẩn mực về cách thức ứng dụng logic thời gian tuyến tính LTL, kỹ thuật trừu tượng hóa trạng thái SOG và phương pháp phân rã hệ thống đa thành phần trong đề tài nghiên cứu phương pháp hình thức.
3. Nhà phát triển công cụ kiểm thử tự động (Model Checker Developers): Cung cấp bản thiết kế kiến trúc chi tiết, giải thuật ánh xạ Petri Nets sang LTS và phương pháp mở rộng module thực tế trên framework mã nguồn mở PAT.
4. Giảng viên và nhà nghiên cứu tại các trường đại học khối kỹ thuật: Sử dụng làm học liệu mẫu phục vụ giảng dạy các môn học chuyên ngành như Lý thuyết tính toán, Thiết kế hệ thống tin cậy, Đảm bảo chất lượng phần mềm và Mô hình hóa hệ thống.

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

Mô hình Petri Nets mang lại lợi ích gì trong kiểm tra tính đúng đắn của phần mềm? Petri Nets cung cấp cả biểu diễn trực quan lẫn nền tảng toán học chặt chẽ để mô hình hóa trạng thái và dòng điều khiển của các tiến trình đồng thời. Thông qua các khái niệm vị trí, bước chuyển và token, mô hình cho phép phân tích toán học chính xác các trạng thái bế tắc hoặc vi phạm an toàn tài nguyên.

Hiện tượng bùng nổ không gian trạng thái được công cụ PeCAn xử lý như thế nào? PeCAn giải quyết bùng nổ trạng thái bằng cách kết hợp đồ thị quan sát đặc trưng SOG và chiến lược kiểm thử tăng dần. Bằng cách gộp các trạng thái nội bộ thành siêu trạng thái (meta-state), công cụ giảm hơn 80% không gian trạng thái cần duyệt, giúp kiểm chứng thành công các mô hình lớn.

Tại sao lược đồ quan sát đặc trưng SOG chỉ hỗ trợ kiểm tra các công thức logic LTL\X? Do kỹ thuật SOG nén một chuỗi các bước chuyển nội bộ không cần quan sát vào trong cùng một meta-state, khái niệm "bước kế tiếp tức thời" bị trừu tượng hóa. Vì vậy, toán tử Next (X) không thể xác định đơn vị thời gian rời rạc, nhưng toàn bộ các toán tử an toàn và sống khác của LTL đều được bảo toàn nguyên vẹn.

Điểm khác biệt nổi bật của PeCAn so với các công cụ như Tina hay Snoopy là gì? PeCAn là công cụ tiên phong hỗ trợ kiểm thử mô hình Petri Nets đa thành phần (compositional) kết hợp giải thuật SOG và bất biến tuyến tính. Ngoài việc kiểm tra mô hình đơn lẻ, PeCAn cho phép chia nhỏ hệ thống thành các mô-đun độc lập và tự động sinh phản ví dụ trực quan.

Framework PAT đóng vai trò gì trong kiến trúc của công cụ PeCAn? PAT đóng vai trò là khung kiến trúc nền tảng, cung cấp sẵn các bộ thư viện phân tích cú pháp logic thời gian, dịch mã Büchi Automata và cơ chế mô phỏng phản ví dụ. Tác giả đã xây dựng thêm module PeCAn tích hợp trực tiếp vào PAT để tận dụng tối đa các thuật toán tối ưu có sẵn của framework.

Kết luận

• Luận văn đã giải quyết xuất sắc bài toán bùng nổ không gian trạng thái trong kiểm tra mô hình mạng Petri bằng việc ứng dụng thành công đồ thị quan sát đặc trưng SOG và phương pháp kiểm thử tăng dần.
• Hiện thực hóa thành công công cụ PeCAn hoàn chỉnh trên framework PAT, hỗ trợ kiểm định hiệu quả cả mô hình Petri Nets đơn thành phần và đa thành phần với giao diện trực quan.
• Tối ưu hóa hiệu năng kiểm chứng hình thức, giúp giảm trên 80% số lượng trạng thái cần duyệt và rút ngắn 50% số bước xác minh trên các mô hình đồng thời thực nghiệm.
• Đóng góp học thuật giá trị với 02 bài báo khoa học được công bố tại các hội nghị chuyên ngành quốc tế uy tín là ATVA 2014 và CCEEE 2014 trong thời gian 11 tháng nghiên cứu.
• Định hướng lộ trình nghiên cứu tiếp theo giai đoạn 2024-2026 tập trung vào mở rộng hỗ trợ Timed/Colored Petri Nets và tối ưu thuật toán tái sử dụng SOG. Các nhà nghiên cứu và kỹ sư quan tâm có thể tải về, trải nghiệm công cụ PeCAn để ứng dụng trực tiếp vào công tác kiểm định hệ thống phần mềm tin cậy cao.

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

Chương 1 Giới thiệu 7 M0 _ A1 B1 C1 _ F1 A2 B2 C1 tB M1 loop tA _ A3 B2 C1 tB F2 A2 B3 C2 M2 _ tA F3 _ A3 B3 C2 Hình 1.6: Đồ thị quan sát đặc trưng của mô hình Petri Nets trong hình 1.3 trạng thái được “gom” chung lại với nhau trong một trạng thái lớn gọi là meta- state. Meta-state bao gồm nhiều trạng thái của hệ thống, được nối nhau bởi các cạnh không cần quan sát. Giữa các meta-state liên kết với nhau thông qua các cạnh cần quan sát. Ta dễ nhận thấy rằng không gian trạng thái của SOG được tạo ra nhỏ hơn so với không gian trạng thái ban đầu.

Và để kiểm tra điều kiện transitition F2 có được fired hay không (trạng thái F2 có đến được hay không, được biểu diễn dưới dạng luận lý tuyến tính theo thời gian bằng công thức ♦F2 ), ta chỉ cần thông qua 2 bước (F1 , F2 ) để khẳng định được tính chất này. Một lợi ích khác khi sử dụng đồ thị quan sát đặc trưng là tính hữu dụng khi mô hình kiểm tra gồm nhiều thành phần (compositional model ), khi một hệ thống lớn được phân rã thành nhiều hệ thống con. Đây cũng là tư tưởng của hướng tiếp cận kiểm tra tăng dần (incremental approach). Ngoài ra, SOG còn có đặc điểm khả dụng lại (reuse).

Khi hệ thống cần kiểm tra có cùng một số tính chất, ta có thể sử dụng lại SOG đã xây dựng cho phương thức kiểm tra trước đó để cải tiến đáng kể cho thời gian kiểm tra chương trình. Chương 1 Giới thiệu 8 1.2 Mục tiêu của đề tài Mục tiêu của đề tài được đặt ra là phát triển phương pháp kiểm tra mô hình Petri Nets một cách hiệu quả. • Nghiên cứu áp dụng việc kiểm tra mô hình để kiểm tra mô hình Petri Nets. Dựa vào các tính chất ưu việt của phương pháp kiểm tra mô hình khi kiểm tra các mô hình lớn, việc xât dựng công cụ kiểm tra mô hình Petri Nets trong môi trường thực tế có thể thực hiện được.

• Nghiên cứu bài toán phân rã một mô hình lớn thành các mô hình nhỏ hơn cho việc phân rã mô hình Petri Nets đa thành phần. • Nghiên cứu áp dụng đồ thị quan sát đặc trưng trên mô hình Petri Nets nhằm trừu tượng hóa bài toán, giảm không gian trạng thái. Từ đó, dẫn tới khả năng thu gọn không gian trạng thái của mô hình và thời gian kiểm tra mô hình. • Nghiên cứu và hiện thực chiến lược kiểm tra tăng dần (incremental ap- proach).

Sử dụng bất biến tuyến tính (linear invariant) để mô phỏng hành vi các mô hình Petri Nets đã chia nhỏ. Đề tài nghiên cứu về các kỹ thuật kiểm tra mô hình dành cho Petri Nets. Từ đó phát triển hệ thống kiểm tra cho mô hình Petri Nets, và cải tiến hệ thống sử dụng các cách tiếp cận nâng cao sử dụng đồ thị quan sát đặc trưng và hướng tiếp cận kiểm tra tăng dần.3 Đóng góp của đề tài • Áp dụng mô hình quan sát đồ thị đặc trưng vào mô hình Petri Nets. • Sử dụng chiến lược kiểm thử tăng dần trong kiểm tra mô hình Petri Nets đa thành phần.

Hiện thực giải thuật tìm bất biến tuyến tính để mô phỏng cho hành vi của các mô hình Petri Nets môi trường. • Xây dựng công cụ PeCAn cho phép kiểm tra mô hình Petri Nets. Công cụ có thể tải về tại website chính thức của dự án [21]. Chương 1 Giới thiệu 9 • Đề tài đã công bố 02 bài báo khoa học tại hội nghị ATVA 2014 [22] và CCEEE 2014 [23].4 Phạm vi và hướng phát triển của đề tài Trong phạm vi giới hạn về thời gian, vẫn còn một số mô hình Petri Nets chưa được hỗ trợ, ví dụ như Petri Nets với màu, Petri Nets với thời gian.

Đây cũng là hướng phát triển tiếp theo cho đề tài: • Nghiên cứu hướng tái sử dụng lược đồ quan sát đặc trưng khi có nhiều thuộc tính cần kiểm tra. Xây dựng lược đồ quan sát đặc trưng dựa trên lược đồ quan sát đặc trưng tổng quát hơn. Từ đó có thể giảm chi phí xây dựng lược đồ và tăng tốc độ cho hệ thống. • Hỗ trợ các mô hình Petri Nets khác như mô hình Petri Nets với thời gian (Timed Petri Nets), Petri Nets với màu (Colored Petri Nets).5 Cấu trúc của luận văn Phần tiếp theo của luận văn được trình bày như sau: • Chương 2 trình bày các kiến thức về mô hình Petri Nets vào các kiến thức nền về kiểm tra mô hình.

• Chương 3 trình bày các nghiên cứu gần đây về kiểm tra mô hình Petri Nets, cũng như các phương pháp để xây dựng một công cụ kiểm tra mô hình. • Chương 4 giới thiệu về lược đồ quan sát đặc trưng và các đặc điểm của lược đồ này. • Chương 5 trình bày về mô hình đa thành phần và chiến lược kiểm tra tăng dần và giải thuật tìm kiếm bất biến tuyến tính để mô phỏng môi trường. • Chương 6 trình bày về kiến trúc của framework PAT, nội dung kiến trúc của công cụ PeCAn.

Chương 1 Giới thiệu 10 • Chương 7 trình bày về các khảo sát về các công cụ khác, đồng thời cũng trình bày về các thí nghiệm và kết quả sơ khởi đạt được. • Chương 8 tổng kết lại luận văn này, và đề cập tới hướng phát triển tiếp theo của luận văn. • Phụ lục A hướng dẫn về cách sử dụng công cụ PeCAn. • Phụ lục B hướng dẫn về cách tạo một module kiểm tra mô hình trong framework PAT.

• Phụ lục C thể hiện chi tiết quá trình làm việc trong thời gian hiện thực luận văn này. Chương 2 Kiến thức nền tảng Như đã đề cập về quy trình kiểm tra một hệ thống trong hình 1.5, để thực hiện việc kiểm tra hệ thống, ta cần mô hình hóa hệ thống dưới bằng mô hình Petri Nets và đặc ta hình thức yêu cầu. Chương này sẽ cung cấp những kiến thức cơ bản về mô hình Petri Nets và kiểm tra mô hình.1 Petri Nets Petri Net là một công cụ dạng đồ thị để mô hình hóa một cách hình thức các dòng chảy của các hoạt động (process). Được phát minh lần đầu vào tháng 8 năm 1939 bởi German Carl Adam Petri để mô phỏng chuỗi các phản ứng hóa học như trong ví dụ 2.

C N aOH HCl H2 O N aCl r1 CO2 r2 N aHCO3 r3 CO2 O2 Hình 2.1: Ví dụ dùng mô hình Petri Nets biểu diễn chuỗi phản ứng hóa học Định nghĩa 2. Petri Nets là một bộ ký hiệu P N = hP, T, W, M0 i trong đó: 11 Chương 2 Kiến thức nền tảng 12 • P là tập hợp hữu hạn các places P = {p0 , p1 ,. • T là tập hợp hữu hạn các transitions T = {t0 , t1 ,. • W là một đơn ánh biểu diễn trọng số của các Arcs nối giữa các cặp place và transition (P × T ) ∪ (T × P ) → N.

• M0 là trạng thái marking khởi tạo của hệ thống. Một trạng thái marking của hệ thống là một đơn ánh m : P → N thể hiện một trạng thái của hệ thống Petri Nets. Ký hiệu Mi (p) cho số lượng tokens của place p tại trạng thái marking Mi. Biểu diễn đồ thị của mô hình Petri Net là một đồ thị hai phần có hướng với 2 loại đỉnh (vertexes) khác nhau (Places và Transitions) và các cung (edges) nối giữa các đỉnh.

Các cung này chỉ nối giữa 2 đỉnh khác loại với nhau: từ Place đến Transition hoặc ngược lại, từ Transition đến Place. Cụ thể như sau: Places là đỉnh của đồ thị, được ký hiệu bằng những hình tròn, biểu diễn những điều kiện, trạng thái hay đối tượng của hệ thống. Transitions là đỉnh của đồ thị, ký hiệu bằng những hình chữ nhật/hình vuông, biểu diễn những hành vi làm thay đổi những điều kiện, trạng thái hay đối tượng của hệ thống. Tokens ký hiệu bằng những dấu chấm, biểu diễn giá trị cụ thể của điều kiện, trạng thái hay đối tượng của hệ thống.

Arcs ký hiệu bằng những đường mũi tên có hướng nối từ Places đến Transitons và ngược lại, biểu diễn mỗi quan hệ giữa những điều kiện với các hành vi cụ thể. Đối với 1 cặp (P, T ) với P là Place và T là Transition, chỉ có một loại Arc theo một hướng xác định. Không bao giờ có Arc nối giữa 2 đối tượng cùng loại. Như vậy, marking là một bộ các số lượng tokens của mỗi place trong một trạng thái cụ thể của Petri Nets.

Các Arcs mặc định có trọng số là 1. Ta có thể tham khảo lại ví dụ 2.1 về một mô hình Petri Nets cơ bản. Trong đó, ta có tập các places P = {C, O2 , CO2 , N aOH, N aHCO3 , HCl, H2 O, N aCl, CO2 }, và tập các transitions T = {r1 , r2 , r3 }, và trạng thái marking khởi tạo M0 = {C = 1, O2 = 1, CO2 = 0, N aOH = 1, N aHCO3 = 0, HCl = 1, H2 O = 0, N aCl = 0, CO2 = 0}. Chương 2 Kiến thức nền tảng 13 2.1 Hành vi ngữ nghĩa của Petri Nets Hành vi ngữ nghĩa của mô hình Petri Nets bao gồm enabling và firing của các Transition Định nghĩa 2.

I − , I + là hai hàm biểu diễn mối quan hệ giữa các cặp Places p và Transition t. • Với I − (p, t) > 0 thì có một Arc nối theo từ hướng của p đến t. • Với I + (t, p) > 0 thì có một Arc nối theo từ hướng của t đến p. Quy ước, ta ký hiệu: • •t = {∀p ∈ P, I − (p, t) > 0} • t• = {∀p ∈ P, I + (t, p) > 0} • •t• = •t ∪ t• Định nghĩa 2.

Một transition t được cho là enable/fireable tại marking Mi khi và chỉ khi Mi (p) ≥ I − (p, t) với ∀p ∈ P , ký hiệu là Enable(t, Mi ). Khi một transition t đang enable tại marking M , t có thể fire và t tạo ra trạng thái marking mới M 0 , ký hiệu M → − M 0 , với M 0 = M (p) − I − (p, t) + I + (t, p) với ∀p ∈ P. Sau khi fire thì, • Mi0 = Mi − I − (i, t) với ∀i ∈ P • Mj0 = Mj + I + (t, j) với ∀j ∈ P Về cơ bản, hàm I − (p, t) biểu diễn cho số lượng tokens cần có của một place p để transition t được enable, cũng là số lượng tokens của p mất đi sau khi t được fire.