Nghiên cứu về Dépliage du modèle en langage AltaRica của NGUYEN Duy Tung tại Université Bordeaux I

Luận văn thạc sĩ nghiên cứu dépliage du modèle en langage altarica, đánh giá hiện trạng, phân tích vấn đề, đề xuất biện pháp hoàn thiện trong lĩnh vực .

• Tác giả: Nguyen Duy Tung
• Người hướng dẫn: M. Couvreur Jean-Michel
• Trường học: Université Bordeaux I
• Chuyên ngành: Informatique
• Đề tài: Dépliage du modèle en langage AltaRica
• Loại tài liệu: Mémoire de fin d'études
• Năm xuất bản: 2005
• Địa điểm: Bordeaux

Mục lục chi tiết

• MOT DE REMERCIEMENT
• 1. Introduction générale
• 2. Langage AltaRica
• 2.1. Introduction
• 2.2. Définition
• 2.3. Transformation de l'AltaRica au réseau de Petri
• 3. Dépliage de réseau de Petri
• 3.1. Notions élémentaires
• 3.2. Dépliage de produits d'automates
• 3.3. Dépliage basé sur le préfixe local
• 3.4. Dépliage basé sur les techniques LCA et RMQ
• 3.5. Dépliage basé sur le RMQ dynamique
• 4. Implémentations expérimentales
• 5. Discussion sur les inconvénients et améliorations
• Annexe

Tóm tắt

I. Giới thiệu về Dépliage du modèle AltaRica Giải pháp hiệu quả

Dépliage du modèle AltaRica là một phương pháp quan trọng trong việc quản lý rủi ro và phân tích mô hình. Phương pháp này giúp giảm thiểu sự phức tạp trong việc kiểm tra các hệ thống phức tạp bằng cách sử dụng ngôn ngữ mô hình hóa cao cấp. Bài viết này sẽ khám phá các khía cạnh khác nhau của phương pháp này, từ lý thuyết đến ứng dụng thực tiễn.

1.1. Định nghĩa và tầm quan trọng của mô hình AltaRica

Mô hình AltaRica là một ngôn ngữ mô hình hóa cao cấp, cho phép mô tả các hệ thống phức tạp một cách dễ dàng hơn so với các ngôn ngữ mô hình hóa thấp hơn như mạng Petri. Việc sử dụng mô hình này giúp các kỹ sư có thể phát triển và kiểm tra các hệ thống một cách hiệu quả hơn.

1.2. Lịch sử phát triển của mô hình AltaRica

Mô hình AltaRica đã được phát triển từ những năm 1990 với sự hợp tác giữa các nhà nghiên cứu và công nghiệp. Qua các giai đoạn phát triển, mô hình này đã được cải tiến để đáp ứng nhu cầu ngày càng cao trong việc mô hình hóa và kiểm tra các hệ thống phức tạp.

II. Vấn đề và thách thức trong việc áp dụng mô hình AltaRica

Mặc dù mô hình AltaRica mang lại nhiều lợi ích, nhưng việc áp dụng nó cũng gặp phải một số thách thức. Một trong những vấn đề lớn nhất là sự phức tạp trong việc chuyển đổi từ mô hình AltaRica sang mạng Petri, điều này có thể dẫn đến sự gia tăng số lượng trạng thái cần kiểm tra.

2.1. Khó khăn trong việc chuyển đổi mô hình

Quá trình chuyển đổi từ mô hình AltaRica sang mạng Petri không chỉ đòi hỏi kiến thức sâu rộng về cả hai ngôn ngữ mà còn cần các công cụ hỗ trợ phù hợp. Việc thiếu các công cụ này có thể làm giảm hiệu quả của quá trình kiểm tra.

2.2. Vấn đề về hiệu suất trong kiểm tra mô hình

Kiểm tra mô hình dựa trên mạng Petri có thể dẫn đến sự bùng nổ tổ hợp, làm cho việc kiểm tra trở nên không khả thi trong một số trường hợp. Điều này đòi hỏi các giải pháp mới để cải thiện hiệu suất kiểm tra.

III. Phương pháp dépliage hiệu quả cho mô hình AltaRica

Để giải quyết các vấn đề nêu trên, nhiều phương pháp dépliage đã được phát triển. Những phương pháp này không chỉ giúp giảm thiểu số lượng trạng thái mà còn cải thiện hiệu suất kiểm tra mô hình.

3.1. Dépliage dựa trên sản phẩm của tự động hóa

Phương pháp này cho phép sử dụng các đặc điểm của mô hình AltaRica để thực hiện dépliage hiệu quả hơn. Bằng cách này, có thể giảm thiểu độ phức tạp của quá trình kiểm tra.

3.2. Kỹ thuật LCA và RMQ trong dépliage

Kỹ thuật LCA (Least Common Ancestor) và RMQ (Range Minimum Query) có thể được tích hợp vào quá trình dépliage để giảm thiểu độ phức tạp và cải thiện hiệu suất kiểm tra mô hình.

IV. Ứng dụng thực tiễn của mô hình AltaRica trong ngành công nghiệp

Mô hình AltaRica đã được áp dụng rộng rãi trong nhiều lĩnh vực khác nhau, từ công nghiệp chế tạo đến công nghệ thông tin. Việc sử dụng mô hình này giúp các tổ chức cải thiện quy trình làm việc và giảm thiểu rủi ro.

4.1. Ví dụ ứng dụng trong ngành chế tạo

Trong ngành chế tạo, mô hình AltaRica đã được sử dụng để mô hình hóa và kiểm tra các quy trình sản xuất phức tạp, giúp tối ưu hóa hiệu suất và giảm thiểu lỗi.

4.2. Ứng dụng trong công nghệ thông tin

Trong lĩnh vực công nghệ thông tin, mô hình AltaRica giúp các nhà phát triển phần mềm kiểm tra và xác minh các hệ thống phức tạp, từ đó nâng cao chất lượng sản phẩm.

V. Kết luận và tương lai của mô hình AltaRica

Mô hình AltaRica đã chứng minh được giá trị của nó trong việc quản lý rủi ro và phân tích mô hình. Tương lai của mô hình này hứa hẹn sẽ còn phát triển hơn nữa với sự hỗ trợ của các công nghệ mới.

5.1. Triển vọng phát triển của mô hình AltaRica

Với sự phát triển không ngừng của công nghệ, mô hình AltaRica có thể được cải tiến để đáp ứng tốt hơn nhu cầu của ngành công nghiệp và nghiên cứu.

5.2. Tầm quan trọng của nghiên cứu tiếp theo

Nghiên cứu tiếp theo về mô hình AltaRica sẽ giúp phát triển các công cụ và phương pháp mới, từ đó nâng cao hiệu quả và khả năng áp dụng của mô hình trong thực tiễn.

Nội dung chính

Tổng quan nghiên cứu

Trong lĩnh vực mô hình hóa và xác minh hệ thống phức tạp, việc xử lý sự bùng nổ tổ hợp trong số lượng trạng thái là một thách thức lớn. Đến năm 2005, các phương pháp xác minh dựa trên tiền tố hữu hạn đã được xem là giải pháp hiệu quả nhằm hạn chế vấn đề này, đặc biệt trên nền tảng mạng Petri – một ngôn ngữ mô hình cấp thấp phổ biến. Theo ước tính, bài toán bùng nổ trạng thái có thể đạt tới mức số trạng thái lên đến hàng nghìn hoặc hàng triệu tùy độ phức tạp hệ thống, đòi hỏi các thuật toán xử lý hiệu quả và tiết kiệm bộ nhớ.

Tuy nhiên, các kỹ thuật này chưa áp dụng đầy đủ cho các ngôn ngữ mô hình cấp cao như AltaRica – vốn được thiết kế để mô tả hệ thống phức tạp với cấu trúc rõ ràng và linh hoạt hơn. Mục tiêu nghiên cứu của luận văn nhằm xây dựng công cụ chuyển đổi mô hình AltaRica sang mạng Petri, đồng thời đề xuất các thuật toán khai triển (dépliage) hiệu quả dựa trên sản phẩm của các tự động hữu hạn, tích hợp các kỹ thuật như LCA (Least Common Ancestor) và RMQ (Range Minimum Query) nhằm giảm thiểu độ phức tạp tính toán.

Phạm vi nghiên cứu giới hạn trong việc áp dụng thuật toán khai triển cho các mô hình chuẩn như Solitaire Game, Dining Philosophers và Buffer với kích thước biến đổi, triển khai và đánh giá trên môi trường máy tính Apple G5 2 lõi, 8GB RAM. Ý nghĩa chính của nghiên cứu nằm ở việc cải thiện hiệu suất xử lý, giảm thiểu thời gian và bộ nhớ sử dụng trong việc kiểm tra mô hình, góp phần vào việc phát triển các công cụ hỗ trợ thiết kế và đánh giá hệ thống phức tạp một cách chính xác và nhanh chóng.

---

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Nghiên cứu dựa trên hai lý thuyết và mô hình chủ đạo:

• Mạng Petri (Petri Net): Là cấu trúc đồ thị có hướng gồm hai loại nút – điểm (place) và chuyển tiếp (transition), mô tả trạng thái và sự kiện hệ thống. Mạng Petri cho phép diễn đạt mối quan hệ đồng thời, xung đột và phụ thuộc nguyên nhân – kết quả trong hệ thống. Đặc trưng của mạng Petri là dùng marquage (đánh dấu) để biểu diễn trạng thái hiện tại.

• Khai triển (Unfolding) mạng Petri: Là phép biến đổi từ mạng Petri sang một cấu trúc dạng cây gọi là mạng xuất hiện (occurrence net) hoặc cây sự kiện, giúp tránh việc xử lý từng trạng thái trong không gian trạng thái lớn bằng cách khai triển tuần tự các sự kiện xảy ra. Thuật toán cơ bản của McMillan (1995) dùng tiền tố hữu hạn để kiểm soát kích thước khai triển.

Ngoài ra, nghiên cứu ứng dụng các khái niệm sau:

• Khai triển sản phẩm các tự động hữu hạn (Unfolding of products of automata): Thay vì khai triển toàn bộ mạng Petri chuyển đổi từ AltaRica, việc khai triển từng thành phần riêng biệt giúp xử lý cục bộ và giảm thiểu tính toán không cần thiết.

• Kỹ thuật LCA (Least Common Ancestor) và RMQ (Range Minimum Query): Đây là các phương pháp trong cấu trúc dữ liệu dùng để truy vấn nhanh chóng quan hệ tổ tiên chung gần nhất hoặc giá trị nhỏ nhất trong một đoạn mảng, từ đó tối ưu xét xung đột, quan hệ thứ tự trong mạng Petri khai triển.

• Định nghĩa và sử dụng các loại tiền tố hữu hạn (finite prefixes) để đảm bảo tính đủ đầy khi khai triển mà không cần xây dựng toàn bộ không gian trạng thái.

Các thuật toán này sử dụng mở rộng cho mô hình AltaRica, cho phép khai triển ngôn ngữ mô hình cấp cao này thông qua chuyển đổi sang mạng Petri.

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

Phương pháp luận chính của nghiên cứu bao gồm các bước sau:

1. Chuyển đổi mô hình: Xây dựng công cụ alta2net dùng thư viện altatool để tự động chuyển đổi mô hình AltaRica sang định dạng mạng Petri. Việc này chỉ xét đến các biến trạng thái, bỏ qua biến luồng nhằm tập trung vào xác minh trạng thái.

2. Thiết kế và triển khai thuật toán khai triển: Bao gồm thuật toán khai triển thông thường dựa theo thuật toán McMillan, và thuật toán khai triển nâng cao dựa trên sản phẩm các tự động. Sử dụng cỡ mẫu với các mô hình tiêu chuẩn như Solitaire Game (SG), Dining Philosophers (DP) và Buffer (BUF) với kích thước biến đổi (ví dụ: SG(3) đến SG(13)).

3. Ứng dụng kỹ thuật LCA và RMQ: Nghiên cứu tích hợp kỹ thuật Least Common Ancestor (LCA) và Range Minimum Query (RMQ), bao gồm RMQ động nhằm tối ưu thao tác kiểm tra xung đột và thứ tự trong khai triển. Tối ưu hóa cấu trúc dữ liệu qua việc xây dựng đồ thị các tiền tố con, cây Cartesian, và cấu trúc dữ liệu cây AVL để hỗ trợ truy vấn nhanh chóng.

4. Phân tích và so sánh kết quả thực nghiệm: Thực hiện thử nghiệm trên các bộ test tiêu chuẩn, ghi nhận các chỉ số về số lượng places |P|, transitions |T|, số sự kiện |E|, số cut-off events, và thời gian khai triển. So sánh hiệu năng giữa khai triển bình thường và khai triển nâng cao, đồng thời đánh giá mức tối ưu trong xử lý cấu trúc dữ liệu.

5. Timeline nghiên cứu: Giai đoạn hoàn thành công cụ chuyển đổi và thuật toán khai triển là tháng 10/2005; công việc mở rộng áp dụng kỹ thuật RMQ và LCA được tiến hành song song trong quá trình thực nghiệm và hoàn thiện đề tài.

---

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

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

1. Hiệu suất thuật toán khai triển sản phẩm các tự động: Thuật toán khai triển nâng cao cho các bài test SG(3) đến SG(13) đã chứng minh tiết kiệm đáng kể thời gian so với khai triển bình thường. Ví dụ, với SG(07), khai triển bình thường mất 83 giây trong khi thuật toán nâng cao gần như đạt 0 giây, tương tự SG(09) mất 1 giây trong khi khai triển bình thường không thể chạy do quá tải tài nguyên.

2. Kết quả chi tiết các mô hình chuẩn:

   • SG(13): Mạng Petri có 39 places, 46 transitions, khai triển nâng cao mất khoảng 61 giây, trong khi phương pháp thường không thực thi được.
   • DP(12): Mạng Petri 72 places, 48 transitions, khai triển nâng cao mất 9 giây, khai triển thường không chạy nổi.
   • BUF(020): 40 places, 21 transitions, khai triển nâng cao trong 1 giây, khai triển bình thường mất đến 984 giây.

3. Giảm độ phức tạp kiểm tra xung đột và cấu hình: Nhờ vào khai triển dựa trên tiền tố cục bộ và sử dụng LCA, RMQ, độ phức tạp xét xung đột giảm từ O(h) xuống gần bằng h^(1/2) hoặc thậm chí hằng số (đối với RMQ động). So sánh cụ thể trong bảng:

   Thuật toán	Độ phức tạp kiểm tra xung đột	Độ phức tạp kiểm tra thứ tự
   Khai triển sản phẩm	O(h)	O(h)
   Dựa trên tiền tố cục bộ	O(h^(1/2))	O(h)
   Dựa trên LCA và RMQ	Hằng số	Hằng số
   Dựa trên RMQ động	O(log(bmax.n))	O(log(bmax.n))

4. Sử dụng các cấu trúc dữ liệu tiên tiến: Mạng Cartesian, cây AVL và cấu trúc ma trận RMQ giúp tăng tốc độ truy vấn và truy cập, đồng thời sử dụng lập trình động để giảm chi phí cập nhật khi thêm sự kiện mới.

Thảo luận kết quả

Việc ứng dụng khai triển dựa trên sản phẩm tự động và các kỹ thuật truy vấn tổ tiên chung giúp giảm tải tính toán khi làm việc với mô hình cấp cao AltaRica, vốn có cấu trúc phân tách rõ ràng thành các thành phần nhỏ (các tự động riêng biệt). Điều này làm giảm đáng kể hiện tượng bùng nổ số trạng thái.

So với các nghiên cứu trước đây tập trung khai triển trực tiếp trên mạng Petri, sự kết hợp với LCA và RMQ cải thiện đáng kể thời gian truy vấn xung đột và quan hệ bậc thang, từ đó đẩy nhanh quá trình xây dựng tiền tố hữu hạn để xác minh mô hình.

Kết quả thực nghiệm cho thấy việc tối ưu thuật toán đòi hỏi phối hợp nhiều công nghệ: chuyển đổi mô hình, xử lý cấu trúc dữ liệu, và phương pháp khai triển phân tán thủ công (local + global). Tuy nhiên, nghiên cứu cũng lưu ý nhược điểm khi kích thước mô hình quá lớn, ngay cả phương pháp nâng cao cũng gặp khó khăn do độ lớn cây arborescent và yêu cầu tính toán cao.

Các đồ thị và bảng so sánh trong luận văn minh họa rõ ràng sự khác biệt về tốc độ và quy mô xử lý, thể hiện tính khả thi của giải pháp trong thực tế ứng dụng công nghiệp.

---

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

1. Phát triển thêm thuật toán khai triển dựa trên RMQ động để giảm thiểu chi phí cập nhật dữ liệu khi thêm sự kiện mới. Thời gian đề xuất: 6-12 tháng. Chủ thể: nhóm phát triển phần mềm LaBRI.

2. Tối ưu hóa công cụ alta2net hỗ trợ chuyển đổi mô hình AltaRica lớn hơn nhằm khai thác triệt để tính chất phân mảnh của mô hình và giảm thiểu biến thể không cần thiết. Thời gian: 3-6 tháng. Chủ thể: nhóm nghiên cứu logic và công cụ.

3. Áp dụng song song hóa (parallelization) thuật toán khai triển trên các kiến trúc đa nhân hoặc cụm máy để mở rộng quy mô mô hình khả thi. Timeline: 1 năm. Chủ thể: bộ phận phát triển và nhà khoa học tính toán hiệu năng cao.

4. Nghiên cứu thuật toán heuristics giảm kích thước cây arborescent trong khai triển local nhằm giảm bớt chi phí tính toán cho trường hợp xấu hoặc cấu trúc cây phức tạp. Thực hiện: 6 tháng. Chủ thể: nghiên cứu viên chuyên sâu về mô hình mạng Petri.

Các đề xuất này nhằm hướng tới tiêu chí giảm thời gian chạy, tiết kiệm bộ nhớ và mở rộng độ lớn hệ thống mô hình được kiểm tra.

---

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

1. Nhà nghiên cứu khoa học máy tính và kỹ thuật phần mềm: Tận dụng phương pháp khai triển sản phẩm tự động và kỹ thuật dữ liệu nâng cao để phát triển các công cụ xác minh mô hình quy mô lớn, tối ưu hiệu suất.

2. Kỹ sư phát triển hệ thống phức tạp, đặc biệt trong công nghiệp chế tạo và hàng không: Ứng dụng ngôn ngữ AltaRica kết hợp công cụ khai triển đã đề xuất để mô hình hóa và xác minh hệ thống nhằm đảm bảo tính chính xác, độ an toàn.

3. Sinh viên và học viên cao học nghiên cứu về mô hình hóa vận hành và xác minh: Tài liệu cung cấp nền tảng lý thuyết, kỹ thuật triển khai và thí nghiệm thực tế, giúp nắm vững kiến thức về mạng Petri, ngôn ngữ mô hình cao cấp và hình thức khai triển.

4. Nhóm phát triển phần mềm công cụ mô hình và xác minh: Tận dụng các thuật toán, cấu trúc dữ liệu được trình bày để tích hợp vào công cụ có khả năng xử lý mô hình phức tạp với hiệu năng cao.

Các đối tượng này có thể áp dụng bài học từ nghiên cứu để mở rộng hoặc phát triển hệ thống mô hình hóa và kiểm thử tối ưu hơn trong tương lai.

---

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

1. Khai triển (unfolding) là gì và tại sao lại quan trọng trong xác minh mô hình?
Khai triển là quá trình chuyển đổi mạng Petri sang cấu trúc dạng cây (mạng xuất hiện) nhằm thể hiện rõ ràng các sự kiện đồng thời và phụ thuộc. Điều này giúp giảm kích thước không gian trạng thái cần xét đến, tránh bùng nổ tổ hợp và tăng hiệu quả xác minh.

2. Tại sao cần chuyển đổi mô hình từ AltaRica sang mạng Petri?
Mạng Petri là ngôn ngữ mô hình có nền tảng lý thuyết phong phú và nhiều thuật toán khai triển, xác minh sẵn có. AltaRica là ngôn ngữ cao cấp có nhiều tính năng linh hoạt nhưng chưa có nhiều công cụ hỗ trợ khai triển trực tiếp, nên chuyển đổi giúp dùng được các thuật toán khai triển đã phát triển.

3. Kỹ thuật LCA và RMQ giúp tối ưu gì trong thuật toán khai triển?
LCA (Least Common Ancestor) và RMQ (Range Minimum Query) cho phép truy vấn nhanh quan hệ tổ tiên chung và giá trị nhỏ nhất trên các cây khai triển. Nhờ đó, tốc độ kiểm tra xung đột và quan hệ thứ tự trở nên gần như hằng số, giảm đáng kể thời gian tính toán.

4. Thuật toán khai triển sản phẩm các tự động có điểm mạnh nào?
Thuật toán này khai triển riêng từng thành phần tự động trong mô hình rồi phối hợp kết quả, tránh việc khai triển toàn cầu toàn bộ mạng Petri, giúp tiết kiệm bộ nhớ và thời gian xử lý nhờ khai thác đặc điểm cấu trúc phân mảnh.

5. Những giới hạn nào của phương pháp đề xuất?
Mặc dù có cải tiến về độ phức tạp, khi kích thước mô hình rất lớn vẫn gặp khó khăn do số lượng trạng thái cực lớn và độ sâu cây arborescent tăng cao. Việc cập nhật dữ liệu động cũng tạo ra chi phí, đòi hỏi nghiên cứu bổ sung để tối ưu thêm.

---

Kết luận

• Đã xây dựng thành công công cụ chuyển đổi AltaRica sang mạng Petri, làm cơ sở cho khai triển và xác minh mô hình cấp cao.
• Triển khai hiệu quả thuật toán khai triển sản phẩm tự động, giảm thời gian chạy từ hàng chục phút xuống gần bằng không trong các mô hình chuẩn.
• Ứng dụng thành công kỹ thuật dữ liệu LCA và RMQ giúp cải tiến đáng kể độ phức tạp kiểm tra xung đột, đảm bảo truy vấn nhanh và chính xác.
• Thực nghiệm trên các bộ test chứng minh tính khả thi của phương pháp, đồng thời nhận diện các điểm cần cải tiến khi xử lý mô hình quy mô lớn.
• Hướng phát triển tiếp theo tập trung vào thuật toán khai triển dựa trên RMQ động, tối ưu cập nhật và mở rộng khả năng song song hóa.

Luận văn khuyến khích các nhà nghiên cứu, kỹ sư và nhà phát triển công cụ tiếp tục khai thác, cải tiến thuật toán nhằm xử lý được các hệ thống phức tạp hơn với hiệu suất cao hơn, đáp ứng nhu cầu ngày càng tăng trong lĩnh vực tự động hóa và mô phỏng hệ thống.
Hành động tiếp theo: Áp dụng đề xuất phát triển thuật toán RMQ động, triển khai song song thuật toán khai triển trong các dự án nghiên cứu và công nghiệp.

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

Université Bordeaux I – Institut de la Francophonie ENSEIRB - CNRS pour lʹInformatique Laboratoire Bordelais de Recherche en Informatique Mémoire de fin d'études "Dépliage du modèle en langage AltaRica" Préparé par NGUYEN Duy Tung Sous la direction de M. COUVREUR Jean-Michel et M. WALUKIEWICZ Igor LaBRI, Octobre 2005 TIEU LUAN MOI download : [e-mail] Dépliage du modèle en langage AltaRica Page 1 Table des matières 1.3 Transformation de l'AltaRica au réseau de Petri. Dépliage de réseau de Petri.2 Etat de l'art .3 Dépliage de produits d'automates .1 Dépliage basé sur le préfixe local.2 Dépliage basé sur les techniques LCA et RMQ.3 Dépliage basé sur le RMQ dynamique.

La syntaxe de langage AltaRica au format BNF. Tests standards en langage AltaRica. Algorithme de dépliage de produits d'automates. Autres exemples de réseaux de Petri et leurs préfixes .58 Mémoire de fin d'études de NGUYEN Duy Tung, Promotion IX TIEU LUAN MOI download : [e-mail] Dépliage du modèle en langage AltaRica Page 2 Liste des figures Figure 2.1 : Réseau de Petri Figure 2.2 : Réseau de Petri de SG(3) Figure 2.3 : Macro-transition et des transitions correspondantes Figure 2.4 : SG(3) en langage AltaRica Figure 3.1 : Réseau d'ocurrence Figure 3.2a : Algorithme de dépliage Figure 3.2b : Génération des transitions Figure 3.3 : Préfixe fini Figure 3.4 : Préfixe du dépliage de SG(3) Figure 3.5a : Composant s0 de SG(3) Figure 3.5b : Composant s1 de SG(3) Figure 3.5c : Composant s2 de SG(3) Figure 3.6a : Processus arborescent dans le composant s0 de SG(3) Figure 3.6b : Processus arborescent dans le composant s1 de SG(3) Figure 3.6c : Processus arborescent dans le composant s2 de SG(3) Figure 3.7 : Processus arborescent global Figure 5.1 : Graphe des sous-préfixes Figure 5.2 : Les sous-préfixes Q, R et P de SG(3) Figure 5.3 : Graphe des sous-préfixes de SG(3) Figure 5.4 : L'arbre Cartsian du composant s1 de SG(3) Figure 5.5 : RMQ rapide Figure 5.6 : La construction du graphe des sous-préfixes Figure 5.7 : Construction de matrice A Figure 5.8 : Arbre AVL dans le RMQ dynamique Mémoire de fin d'études de NGUYEN Duy Tung, Promotion IX TIEU LUAN MOI download : [e-mail] Dépliage du modèle en langage AltaRica Page 3 Liste des tableaux Tableau 4.1 : Résultats de dépliage du SG (avec une blanche) Tableau 4.2 : Résultats de dépliage du SG (avec deux blanches) Tableau 4.3 : Résultats de dépliage du DP Tableau 4.4 : Résultats de dépliage du BUF Tableau 5.1 : Comparaison de la complexité des algorithmes de dépliage Mémoire de fin d'études de NGUYEN Duy Tung, Promotion IX TIEU LUAN MOI download : [e-mail] Dépliage du modèle en langage AltaRica Page 4 Résumé De nos jours, pour éviter l'explosion combinatoire du nombre d'états d'un système compliqué, la vérification basée sur des préfixes finis est une bonne solution, mais le dépliage n'est développé que sur le réseau de Petri, un langage de modélisation en bas niveau.

Autrement dit, il ne supporte pas un langage de modélisation en haut niveau comme l'AltaRica. Il faut construire un outil de transformation pour résoudre ce problème. D'autre part, grâce aux caractéristiques du modèle en AltaRica, on peut utiliser un dépliage plus efficace, le dépliage de produits d'automates. De plus, dans leur dépliage local, nous pouvons intégrer la technique basée sur le préfixe local ou les techniques Dernière Ancêtre Commun (LCA) et Requête Minimale du Rang (RMQ) pour diminuer la complexité du problème.

Nous avons des implémentations expérimentales sur des tests standards pour tester la correctivité et la performance des algorithmes de dépliage ainsi que des améliorations. Mots clés: Dépliage, Altarica, réseau de Petri, modélisation, vérification, préfixe, Dernière Ancêtre Commun (LCA), Requête Minimale du Rang (RMQ), RMQ dynamique Mémoire de fin d'études de NGUYEN Duy Tung, Promotion IX TIEU LUAN MOI download : [e-mail] Dépliage du modèle en langage AltaRica Page 5 Abstract Nowadays, for avoiding the combinational explosion of the states number of complex systems, the model-checking based on finite prefix is a good solution but the unfolding is only developed on the Petri net, a language of modelling in low-level. In other words, it does not support a modelling language in high-level like AltaRica. We must build a tool of transformation in order to resolve this problem.

On the other hand, because of features of model in AltaRica, we can use a more efficient unfolding, this is a unfolding of products of automats. Furthermore, in their local unfolding, we can integrate the technic based on the local prefixe or the technics Least Common Ancestor (LCA), Range Minimum Query (RMQ) for reduce the complexity of the problem. We have the experimental implementations on the standard tests in order to test the correctitude and the performance of unfolding algorithms and their improvements. Key-words: Unfolding, Altarica, Petri net, modelling, model-checking, prefix, Least Common Ancestor (LCA), Range Minimum Query (RMQ), dynamic RMQ Mémoire de fin d'études de NGUYEN Duy Tung, Promotion IX TIEU LUAN MOI download : [e-mail] Dépliage du modèle en langage AltaRica Page 6 Remerciement Je tiens à remercier mes responsables, en particulier M.

Jean-Michel COUVREUR qui m'a aidé à maîtriser le sujet du stage, a corrigé mes fautes au début et m'a favorisé enfin de trouver de nouvelles solutions pour le dépliage. Gérald POINT et M. Alaine GRIFFAULT qui me donnent des documents intéressants concernant à l'AltaRica. André ARNOLD pour l'idée du LCA, et M.

Gérald POINT pour sa bibliothèque altatool pour que je puisse économiser le temps. Je suis heureux d'avoir rencontré et de m'être intégré dans le groupe MVTsi (Modélisation, Vérification et Test des systèmes informatisés), en particulier M. The Quang TRAN qui m'a aidé à surmonter des difficultés dans un nouvel environnement. Victor KHOMENKO qui m'a donné des tests standards pour tester mes implémentations expérimentales et les comparer avec les autres.

Je tiens à remercier les professeurs à l'IFI en particulier M. Thanh Thuy NGUYEN qui m'ont contribué des meilleures conditions pour mon stage au LaBRI, Université Bordeaux 1. Enfin, je veux envoyer un grand merci pour ma famille, mes amis qui ont partagé mes obstacles, m'ont favorisé durant mon stage. Mémoire de fin d'études de NGUYEN Duy Tung, Promotion IX TIEU LUAN MOI download : [e-mail] Dépliage du modèle en langage AltaRica Page 7 1.

Introduction générale Né de la volonté d'industriels et de chercheurs, le langage de modélisation en haut niveau AltaRica [Arnold03] a beaucoup d'avantages tels qu'il est utilisé plus facilement que des langages de modélisation en bas niveau comme le réseau de Petri ou il est naturel de pouvoir décrire par de nombreuses façons différentes un système donné. La vérification basée sur des préfixes finis [Esparza01, Couvreur04] est une nouvelle approche pour éviter l'explosion combinatoire de nombre d'états du système compliqué, mais ces techniques ne sont développées que sur le réseau de Petri, un langage de modélisation en bas niveau. L'objectif de mon stage est de réaliser un dépliage sur le langage AltaRica: pas seulement de construire un outil de tranformation de l'AltaRica au réseau de Petri, mais aussi de chercher des algorithmes plus efficaces pour déplier un modèle en AltaRica. Grâce aux caractéristiques du modèle en AltaRica, on peut utiliser un dépliage supplémentaire, c'est le dépliage de produits d'automates [Esparza et al, 99, Couvreur04].

De plus, dans leur dépliage local, pour améliorer la complexité du test de conflit, du test de la configuration ou la complexité du problème en général, nous pouvons intégrer la technique basée sur le préfixe local, les techniques Dernière Ancêtre Commun (LCA) ou Requête Minimale du Rang (RMQ) [Demaine03, Bender00] et la technique basée sur le RMQ dynamique [Shibuya03]. L'introduction de langage AltaRica est donnée dans la section 2. Nous allons présenter l'état de l'art du dépliage et le dépliage de produits d'automates dans la section 3. En suite, on peut trouver aussi les implémentations expérimentales et les comparaisons entre le dépliage normal et le dépliage de produits d'automates dans la section 4.

En fin, on discute sur les inconvénients et les améliorations du dépliage de produits d'automates dans la section 5. Mémoire de fin d'études de NGUYEN Duy Tung, Promotion IX TIEU LUAN MOI download : [e-mail] Dépliage du modèle en langage AltaRica Page 8 2. Langage AltaRica Langage AltaRica est un langage de modélisation en haut niveau ayant des avantages tels que la construction des systèmes complexes plus facile que des langages de modélisation en bas niveau comme le réseau de Petri. Plus en détail dans [Arnold03].1 Introduction Le projet AltaRica est né de la volonté d'industriels et de chercheurs pour établir divers ponts entre : • la sûreté de fonctionnement et les méthodes formelles, • les analyses quantitatives des dysfonctionnements et les analyses qualitatives des comportements fonctionnels, • les divers outils et méthodes d'aide à la modélisation, afin de fournir aux ingénieurs concepteurs de systèmes complexes où critiques un atelier outillé.

Dans ce contexte, un outil de la vérification d'AltaRica basé sur le préfixe est attentatif. Ce projet commence depuis 1996 et se compose de trois phases. AltaRica : phase I (de Novembre 1996 à Octobre 1997) Objectifs : Etude de la faisabilité de couplages de différents outils en précisant si nécessaire la sémantique de certains d'entre eux. Résultats : Définition d'un langage de description de systèmes complexes, validé par l'expérimentation sur des cas tests.

Les partenaires : Les sociétés IXI et ELF Aquitaine Production d'une part; les laboratoires LaBRI et LADS d'autre part. AltaRica : phase II (de Novembre 1997 à Octobre 1999) Objectifs : Stabilisation du langage AltaRica, réalisation d'un prototype et méthodologie d'utilisation. Résultats : La sémantique du langage a été fixée. Des prototypes d'outils nécessaires à la simulation d'un modèle AltaRica ont été développés.

Des prototypes de compilateurs Mémoire de fin d'études de NGUYEN Duy Tung, Promotion IX TIEU LUAN MOI download : [e-mail] Dépliage du modèle en langage AltaRica Page 9 vers les outils Aralia et Mec ont été développés et un premier manuel méthodologique a été écrit. Les partenaires : La société d'ingénierie IXI, les industriels Dassault Aviation, ELF EP, Schneider Electric, Renault, IPSN et Thomson Detexis, et enfin les laboratoires LaBRI et LADS. AltaRica : phase III (de Juin 2001 à Mai 2003) Objectifs : Réalisation d'un atelier AltaRica Les partenaires : La société d'ingénierie IXI, les industriels Dassault Aviation, TotalFinaElf, Schneider Electric, France Telecom, Thales systèmes aéroportés, et enfin les laboratoires LaBRI, IRCCyN et ONERA. Jusqu'à maintenant, on continue à développer des outils dans ce langage.

Et un outil de vérification basée sur le préfixe dans ce mémoire est un exemple.2 Définition Tout d'abord, on concerne le réseau de Petri, étant un des langages de modélisation en bas niveau. Il est défini dans [Couvreur04] comme le suivant: Définition 2.1 (Réseau de Petri) Un réseau de Petri R est une structure <P, T, Pre, Post> où • P et T sont des ensembles (finis ou infinis) disjoints, • Pre et Post sont de fonctions de T dans IN|P| \ {0}. Les éléments de P et T sont appelés des places et des transitions, et Pre et Post sont les fonctions de pré- et post-conditions des transitions. Un marquage m de R est un multi-ensembles de P (m ∈ IN|P|).

Un réseau marqué <R, m0> est la donnée d'un réseau de Petri R et d'un marquage initial m0. Un réseau étiqueté <R, Σ, λ> est la donnée d'un réseau de Petri R, d'un alphabet fini Σ et d'une fonction d'étiquetage sur les transitions λ: T → Σ. L'ensemble des prédécesseurs (resp. des successeurs) d'une place p est défini par : •p = { t ∈ T| Post (t) (p) ≠ 0} (resp.

L'ensemble des prédécesseurs (resp. des successeurs) d'une transition t est défini par : •t = { p ∈ P| Pre (t) (p) ≠ 0} (resp. Si S est un ensemble de P ∪ T, alors *s (resp. s*) désigne l'ensemble de ses prédécesseurs (resp.

successeurs) directs et indirects.