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

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.

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.