Luận văn thạc sĩ: Mô hình hóa hệ thống platoon xe tự hành bằng CSP||B

Luận văn thạc sĩ nghiên cứu vnu construction dun platoon en cspllb, đá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ả: Huu-Nghia Nguyen
• Người hướng dẫn: Jean-Pierre Jacquot
• Trường học: IFI LORIA Hanoï
• Chuyên ngành: Công nghệ thông tin
• Đề tài: Construction D'un Platoon En CSP||B
• Loại tài liệu: Luận văn thạc sĩ
• Năm xuất bản: 2009
• Địa điểm: Nancy

Tóm tắt

I. Tổng quan luận văn thạc sĩ VNU về xây dựng đoàn xe tự hành

Luận văn thạc sĩ với chủ đề "Construction d'un platoon en CSP||B" (Xây dựng một đoàn xe tự hành bằng CSP||B) là một công trình nghiên cứu khoa học xây dựng hệ thống tiêu biểu, được thực hiện trong khuôn khổ các dự án TACOS và CRISTAL. Đề tài tập trung vào việc thiết kế các hệ thống giao thông đô thị mới dựa trên xe điện tự hành. Mục tiêu cốt lõi của luận văn thạc sĩ kỹ thuật xây dựng hệ thống này là sử dụng phương pháp hình thức CSP||B để mô hình hóa và xác minh hành vi phức tạp của các phương tiện khi chúng hoạt động theo đội hình, hay còn gọi là "platoon". Nghiên cứu này không chỉ giải quyết các vấn đề kỹ thuật trong lĩnh vực xe tự hành mà còn đóng góp một công cụ phần mềm quan trọng, giúp tự động hóa một bước kiểm chứng vốn phải thực hiện thủ công trong phương pháp CSP||B. Toàn bộ nội dung và phương pháp luận được trình bày một cách hệ thống, thể hiện chiều sâu nghiên cứu và là một tài liệu tham khảo giá trị trong kho luận văn VNU. Luận văn cung cấp một cái nhìn chi tiết về cách tiếp cận hình thức trong việc đảm bảo tính đúng đắn và an toàn cho các hệ thống phần mềm phức tạp, đặc biệt là trong các ứng dụng có tính tương tác và đồng thời cao như xe tự hành. Công trình này là minh chứng cho sự kết hợp hiệu quả giữa lý thuyết khoa học máy tính và ứng dụng thực tiễn trong ngành công nghệ giao thông thông minh.

1.1. Bối cảnh và mục tiêu của đề tài thạc sĩ ngành xây dựng hệ thống

Bối cảnh nghiên cứu của đề tài thạc sĩ ngành xây dựng hệ thống này xuất phát từ các dự án TACOS và CRISTAL, nhằm phát triển một hệ thống xe điện tự hành cho dịch vụ công cộng. Trong hệ thống này, các xe có khả năng tự tổ chức thành các đoàn xe (platoon) để di chuyển hiệu quả hơn. Mục tiêu ban đầu của luận văn là mở rộng một mô hình CSP||B đã có sẵn. Mô hình cũ chỉ mô tả được hai trạng thái ổn định của xe: di chuyển độc lập (SOLO) và di chuyển trong đoàn (PLATOON). Nhiệm vụ đặt ra là phải mô hình hóa thêm hai trạng thái chuyển tiếp phức tạp: quá trình một xe xin gia nhập đoàn (JOINT) và quá trình rời khỏi đoàn (DISJOINT). Ngoài ra, một mục tiêu quan trọng khác là giải quyết vấn đề trong quy trình xác minh của phương pháp CSP||B. Cụ thể là chưa có công cụ nào tự động kiểm tra được tính nhất quán giữa máy B (B-machine) và bộ điều khiển CSP (CSP controller), một bước cốt yếu để đảm bảo mô hình là chính xác. Do đó, luận văn còn hướng tới việc xây dựng một phần mềm để tự động hóa công đoạn này, nâng cao hiệu quả và độ tin cậy của toàn bộ phương pháp.

1.2. Giới thiệu phương pháp CSP B trong nghiên cứu khoa học xây dựng

CSP||B là một phương pháp hình thức tiên tiến, kết hợp sức mạnh của hai công cụ lý thuyết đã được chứng minh: phương pháp B (B-Method) và Đại số các tiến trình giao tiếp tuần tự (Communicating Sequential Processes - CSP). Phương pháp B, dựa trên logic vị từ và lý thuyết tập hợp, được sử dụng để mô tả các trạng thái của hệ thống và các hoạt động làm thay đổi trạng thái đó. Trong khi đó, CSP là một đại số tiến trình, chuyên dùng để mô tả và phân tích sự tương tác và giao tiếp giữa các thành phần đồng thời. Sự kết hợp này cho phép mô tả cả hai khía cạnh của một hệ thống: khía cạnh trạng thái (dữ liệu, biến) và khía cạnh hành vi (sự kiện, tương tác). Trong khóa luận thạc sĩ xây dựng hệ thống này, máy B được dùng để mô tả trạng thái vật lý của xe (vận tốc, vị trí), còn bộ điều khiển CSP dùng để quy định chuỗi các hành động mà xe thực hiện, ví dụ như nhận thông tin từ xe phía trước và ra quyết định tăng hay giảm tốc. Cách tiếp cận này tận dụng được các công cụ hỗ trợ sẵn có cho cả B và CSP, giúp việc xác minh mô hình trở nên hiệu quả hơn.

II. Phân tích các thách thức trong việc mô hình hóa hệ thống phức tạp

Việc mô hình hóa hệ thống xe tự hành theo đoàn đặt ra nhiều thách thức lớn, đòi hỏi các phương pháp phải đủ mạnh để đảm bảo tính an toàn và đúng đắn. Một trong những khó khăn chính là việc xử lý các tương tác đồng thời và phức tạp giữa nhiều phương tiện. Mỗi xe là một thực thể tự hành, phải liên tục nhận dữ liệu từ môi trường và từ các xe khác, sau đó ra quyết định trong thời gian thực. Quản lý dự án xây dựng một hệ thống như vậy đòi hỏi phải có một mô hình chính xác để mô tả các giao thức giao tiếp và các quy tắc đồng bộ hóa, nhằm tránh các tình huống nguy hiểm như va chạm hay tắc nghẽn. Hơn nữa, các trạng thái của hệ thống không chỉ bao gồm các chế độ hoạt động ổn định mà còn có các giai đoạn chuyển tiếp. Các quá trình như gia nhập hay rời đoàn xe là những chuỗi hành động phức tạp, cần được đặc tả một cách chặt chẽ để đảm bảo an toàn tuyệt đối. Các mô hình hiện có thường tập trung vào trạng thái ổn định mà bỏ qua sự phức tạp của các pha chuyển tiếp này. Đây chính là lỗ hổng mà đồ án tốt nghiệp thạc sĩ xây dựng hệ thống này nhắm tới giải quyết, bằng cách cung cấp một mô hình toàn diện và có khả năng xác minh hình thức.

2.1. Vấn đề đồng bộ hóa và tương tác giữa các xe tự hành

Đồng bộ hóa là bài toán cốt lõi khi các xe di chuyển theo đội hình. Không có liên kết vật lý, mỗi xe phải tự điều chỉnh tốc độ và khoảng cách dựa trên thông tin nhận được từ xe phía trước. Luận văn chỉ ra rằng mô hình ban đầu sử dụng kênh giao tiếp trực tiếp giữa hai xe. Tuy nhiên, cách tiếp cận này gặp khó khăn khi mô hình hóa quá trình một xe mới gia nhập hoặc rời đi, vì cấu trúc kênh giao tiếp trong CSP là tĩnh, không thể thêm bớt một cách linh động. Để giải quyết vấn đề này, luận văn đề xuất một thực thể trung gian gọi là "Net". Net đóng vai trò là một trung tâm thông tin, nơi tất cả các xe gửi thông tin của mình (vị trí, tốc độ) và nhận thông tin về các xe khác. Nhờ đó, các kênh giao tiếp trở nên cố định (giữa mỗi xe và Net), giúp đơn giản hóa việc mô hình hóa các hành vi động như gia nhập và rời đoàn. Net cũng quản lý thông tin về các đoàn xe, chẳng hạn như số lượng thành viên, để xử lý các yêu cầu xin phép gia nhập.

2.2. Hạn chế của các mô hình hiện có trong xử lý trạng thái chuyển tiếp

Mô hình P LAT OON ban đầu do nhóm DEDALE phát triển đã đặc tả thành công hai chế độ hoạt động SOLO và PLATOON. Tuy nhiên, nó không đủ phức tạp để mô tả các quy trình gia nhập (JOINT) và rời đoàn (DISJOINT). Các quá trình này không chỉ đơn thuần là thay đổi tốc độ, mà còn liên quan đến một loạt các bước logic: gửi yêu cầu, chờ cấp phép, thực hiện chuỗi hành động để tiếp cận hoặc rời xa đoàn, và cuối cùng là xác nhận hoàn tất. Ví dụ, một xe muốn gia nhập phải kiểm tra xem đoàn xe mục tiêu còn chỗ trống hay không và có xe nào khác đang thực hiện thao tác tương tự không. Những logic phức tạp này đòi hỏi một cấu trúc mô hình chi tiết hơn. Luận văn đã cải tiến mô hình ban đầu để xây dựng một hệ thống hoàn chỉnh, mô tả được cả bốn chế độ hoạt động. Đây là một đóng góp quan trọng, giúp mô hình phản ánh gần hơn với hoạt động thực tế của một hệ thống xe tự hành linh hoạt.

III. Hướng dẫn áp dụng phương pháp CSP B để mô hình hóa platoon

Luận văn cung cấp một hướng dẫn chi tiết về cách áp dụng phương pháp CSP||B vào bài toán mô hình hóa đoàn xe tự hành. Cách tiếp cận này chia hệ thống thành các thành phần (component), mỗi thành phần bao gồm một máy B và một bộ điều khiển CSP. Máy B được sử dụng để mô tả khía cạnh trạng thái của hệ thống. Ví dụ, trong thành phần Vehicle, máy B lưu trữ các biến trạng thái như speed (tốc độ) và xpos (vị trí), đồng thời cung cấp các hoạt động (operation) để truy vấn hoặc cập nhật các biến này, như getSpeed và setAccel. Bộ điều khiển CSP, mặt khác, lại đặc tả hành vi, hay luồng điều khiển của hệ thống. Nó định nghĩa chuỗi các sự kiện và tương tác. Bộ điều khiển CSP sẽ gọi các hoạt động của máy B thông qua các "kênh máy" (machine channel). Sự kết hợp này tạo ra một mẫu luận văn thạc sĩ chuẩn về cách mô hình hóa các hệ thống phản ứng (reactive system), nơi hành vi tuần tự được điều khiển bởi các sự kiện và trạng thái nội tại. Quy trình xác minh cũng được trình bày rõ ràng, bao gồm ba bước chính: xác minh máy B, xác minh bộ điều khiển CSP, và quan trọng nhất là xác minh tính nhất quán giữa chúng.

3.1. Nguyên lý cơ bản của phương pháp B và đại số xử lý CSP

Phương pháp B là một phương pháp hình thức để phát triển phần mềm, cho phép đặc tả hệ thống một cách trừu tượng và sau đó tinh chỉnh (refinement) dần dần để tiến tới mã thực thi. Nền tảng của nó là logic vị từ và lý thuyết tập hợp. Một máy B (B-machine) định nghĩa một tập các biến trạng thái, một bất biến (invariant) để ràng buộc các giá trị của biến, và một tập các hoạt động (operation) được đặc tả bằng các phép thế. Trong khi đó, CSP là một ngôn ngữ để mô tả các mẫu tương tác trong hệ thống đồng thời. Các khái niệm cốt lõi của CSP bao gồm sự kiện (event), tiến trình (process), và các toán tử để kết hợp các tiến trình như lựa chọn (choice) và song song (parallel composition). Trong luận văn, CSP được dùng để điều khiển thứ tự gọi các hoạt động của máy B, đảm bảo hệ thống hoạt động theo đúng kịch bản mong muốn. Đây là một ví dụ điển hình về công nghệ thi công hệ thống phần mềm hiện đại, sử dụng các công cụ toán học để đảm bảo chất lượng.

3.2. Cách kết hợp CSP và B để tạo một thành phần CSP B hoàn chỉnh

Một thành phần CSP||B là sự lắp ráp của một máy B và một bộ điều khiển CSP. Máy B quản lý dữ liệu và trạng thái nội bộ, trong khi bộ điều khiển CSP xử lý các tương tác và điều phối luồng thực thi. Giao tiếp giữa hai phần này được thực hiện thông qua các kênh máy. Với mỗi hoạt động trong máy B, ví dụ val ← getSpeed(), sẽ có một kênh tương ứng trong CSP, ví dụ getSpeed?val, để gọi hoạt động đó. Bộ điều khiển CSP sẽ ra quyết định dựa trên các sự kiện đầu vào (ví dụ, nhận thông tin từ kênh giao tiếp) và sau đó gọi các hoạt động của máy B để cập nhật trạng thái hệ thống. Ví dụ, bộ điều khiển CtrlRobot trong luận văn nhận khoảng cách d từ cảm biến, sau đó gọi getSpeed?v để lấy tốc độ hiện tại từ máy B, và cuối cùng gọi setSpeed!new_speed để thiết lập tốc độ mới. Kiến trúc này phân tách rõ ràng giữa logic điều khiển (control logic) và quản lý trạng thái (state management), giúp mô hình trở nên rõ ràng và dễ bảo trì.

3.3. Quy trình xác minh một mô hình hóa trong CSP B

Để chứng minh một mô hình CSP||B là đúng, cần thực hiện ba bước xác minh. Đầu tiên, máy B phải được chứng minh là đúng, nghĩa là cú pháp của nó chính xác và tất cả các nghĩa vụ chứng minh (Proof Obligations - POs) đều được thỏa mãn. Việc này thường được thực hiện bằng các công cụ như AtelierB. Thứ hai, bộ điều khiển CSP phải đúng, tức là không có bế tắc (deadlock-free) và không có phân kỳ (divergence-free). Thuộc tính này được kiểm tra bằng các công cụ model-checker như FDR2. Cuối cùng, và cũng là phần thách thức nhất, là phải chứng minh tính nhất quán (consistency) giữa máy B và bộ điều khiển CSP. Điều này có nghĩa là bộ điều khiển CSP không bao giờ được gọi một hoạt động của máy B khi tiền điều kiện (pre-condition) của hoạt động đó không được thỏa mãn. Đây là bước quan trọng để đảm bảo hệ thống hoạt động an toàn. Luận văn tập trung giải quyết việc tự động hóa bước thứ ba này.

IV. Bí quyết xây dựng mô hình 4 trạng thái cho xe tự hành

Điểm nhấn của luận văn là việc xây dựng thành công một mô hình hoàn chỉnh, mô tả chi tiết bốn chế độ hoạt động của một xe tự hành: SOLO, PLATOON, JOINT và DISJOINT. Bí quyết đằng sau thành công này nằm ở việc thiết kế một kiến trúc hệ thống linh hoạt và tái cấu trúc mô hình ban đầu một cách thông minh. Thay vì chỉ tập trung vào kết cấu công trình phần mềm đơn giản, tác giả đã giới thiệu một thành phần trung gian là Net để quản lý thông tin và giao tiếp, giải quyết bài toán kênh tĩnh của CSP. Kiến trúc tổng thể của hệ thống bao gồm n thành phần Cristal (đại diện cho mỗi xe) và một thành phần Net. Mỗi Cristal lại được cấu thành từ hai thành phần con: Vehicle (mô phỏng phần cứng vật lý của xe) và DrivingSystem (bộ não ra quyết định). Sự phân chia rành mạch này cho phép đặc tả các hành vi phức tạp một cách có hệ thống. Luồng thay đổi trạng thái cũng được định nghĩa rõ ràng: người dùng có thể kích hoạt việc chuyển từ SOLO sang JOINT hoặc từ PLATOON sang DISJOINT. Các quá trình chuyển đổi còn lại (ví dụ từ JOINT sang PLATOON) sẽ diễn ra tự động dựa trên kết quả của quá trình (thành công hay thất bại).

4.1. Thiết kế kiến trúc hệ thống với các thành phần Vehicle và DrivingSystem

Kiến trúc của một xe (Cristal) được phân tách thành hai thành phần chính. Thành phần Vehicle đóng vai trò mô phỏng lớp vật lý. Máy B của nó chứa các thông tin cơ bản như tốc độ và vị trí, và cung cấp các hoạt động để cập nhật chúng, ví dụ như setAccel(accel). Thành phần DrivingSystem là bộ não của xe. Nó nhận thông tin từ các xe khác (thông qua Net), nhận lệnh từ người dùng (ví dụ, yêu cầu gia nhập đoàn), và ra quyết định về gia tốc cần áp dụng. Máy B của DrivingSystem chứa logic phức tạp hơn, chẳng hạn như tính toán gia tốc mới để giữ khoảng cách an toàn trong đoàn, hoặc để tiếp cận đoàn xe mục tiêu. Sự phân tách này tuân theo nguyên tắc thiết kế phần mềm tốt, giúp cô lập các mối quan tâm khác nhau: Vehicle chỉ lo về cơ học chuyển động, trong khi DrivingSystem xử lý logic điều khiển cấp cao.

4.2. Mô tả chi tiết 4 chế độ hoạt động SOLO PLATOON JOINT DISJOINT

Luận văn định nghĩa chi tiết hoạt động của xe trong từng chế độ. Ở chế độ SOLO, xe di chuyển độc lập dưới sự điều khiển của người dùng. Ở chế độ PLATOON, xe tự động bám theo xe phía trước để duy trì khoảng cách lý tưởng. Đây là logic đã có trong mô hình cũ. Chế độ JOINT mô tả quá trình gia nhập. Xe sẽ gửi yêu cầu đến Net, nếu được chấp thuận, nó sẽ thực hiện một vòng lặp để tính toán gia tốc nhằm tiếp cận đuôi đoàn xe. Quá trình kết thúc thành công khi xe đạt khoảng cách phù hợp và chuyển sang PLATOON, hoặc thất bại (ví dụ, do timeout) và quay về SOLO. Ngược lại, chế độ DISJOINT mô tả quá trình rời đoàn. Xe (phải là xe cuối cùng) gửi yêu cầu, nếu được chấp thuận, nó sẽ giảm tốc để tạo khoảng cách an toàn với đoàn xe và sau đó chuyển sang chế độ SOLO. Cách đặc tả chi tiết này giúp mô hình trở nên toàn diện và thực tế.

4.3. Vai trò của thành phần Net trong việc quản lý truyền thông

Thành phần Net là một sáng kiến quan trọng trong mô hình được đề xuất. Nó hoạt động như một thực thể trung gian, giải quyết hạn chế về kênh giao tiếp tĩnh trong CSP. Thay vì các xe giao tiếp trực tiếp với nhau, tất cả đều giao tiếp với Net. Net duy trì trạng thái của toàn bộ hệ thống, bao gồm thông tin (ID, tốc độ, vị trí) của tất cả các xe và danh sách thành viên của từng đoàn xe. Khi một xe cần thông tin về xe phía trước, nó sẽ truy vấn Net. Khi một xe muốn gia nhập hoặc rời đoàn, nó phải gửi yêu cầu và nhận sự cho phép từ Net. Mặc dù có vẻ tập trung hóa, luận văn lập luận rằng Net không phải là "nhạc trưởng" điều khiển mọi hành vi của xe. Các xe vẫn tự chủ ra quyết định. Net chỉ đóng vai trò cung cấp thông tin và điều phối các yêu cầu để tránh xung đột, đảm bảo tính toàn vẹn của hệ thống.

V. Cách tự động hóa xác minh tính nhất quán của mô hình

Một trong những đóng góp đột phá nhất của luận văn là việc xây dựng một công cụ phần mềm để tự động hóa bước xác minh tính nhất quán giữa máy B và bộ điều khiển CSP. Trước đây, bước này phải thực hiện thủ công, rất tốn thời gian và dễ xảy ra sai sót, là một rào cản lớn khi áp dụng CSP||B trong thực tế. Tác giả đã dựa trên kỹ thuật "Bất biến Vòng lặp Điều khiển" (Control Loop Invariant - CLI) do Helen Treharne đề xuất. Ý tưởng chính là dịch bộ điều khiển CSP thành một máy B tương đương (gọi là máy điều khiển), sau đó chứng minh tính đúng đắn của máy điều khiển này. Công cụ được phát triển bằng ngôn ngữ OCaml, sử dụng các công cụ phân tích từ vựng (Ocamllex) và cú pháp (Ocamlyacc). Nó có khả năng đọc mã nguồn CSP, phân tích cấu trúc, loại bỏ các thành phần không liên quan, và tự động tạo ra mã nguồn cho máy B điều khiển. Đáng chú ý, công cụ còn có thể phát hiện khi nào một bất biến CLI là cần thiết và đề xuất dạng của nó, giúp người dùng dễ dàng hoàn thiện quá trình chứng minh. Kết quả này có ý nghĩa lớn, giúp cho việc bảo vệ luận văn thạc sĩ thành công và được hội đồng chấm luận văn đánh giá cao.

5.1. Giới thiệu kỹ thuật Bất biến Vòng lặp Điều khiển CLI

Kỹ thuật Control Loop Invariant (CLI) là nền tảng lý thuyết cho việc xác minh tính nhất quán. Một bộ điều khiển CSP thường có cấu trúc vòng lặp, chuyển qua lại giữa các trạng thái xử lý. Ý tưởng là dịch bộ điều khiển này thành một máy B, với một biến điều khiển cb để theo dõi trạng thái hiện tại của tiến trình CSP. CLI là một bất biến có dạng (cb = x₀ ⇒ P₀) ∧ (cb = x₁ ⇒ P₁) ∧ ..., trong đó Pᵢ là tiền điều kiện của khối mã tương ứng với trạng thái xᵢ. Bất biến này đảm bảo rằng mỗi khi hệ thống chuyển sang một trạng thái mới, các điều kiện cần thiết để thực thi các hoạt động tiếp theo đều được thỏa mãn. Việc chứng minh được máy B điều khiển cùng với bất biến CLI này là tương đương với việc chứng minh rằng bộ điều khiển CSP luôn gọi các hoạt động của máy B một cách chính xác. Đây là một phương pháp toán học chặt chẽ để đảm bảo sự tương thích giữa hai thành phần.

5.2. Xây dựng công cụ dịch CSP sang B và đề xuất dạng CLI

Công cụ do tác giả xây dựng thực hiện một chuỗi các bước thông minh. Đầu tiên, nó phân tích cú pháp file CSP và B để trích xuất các thông tin cần thiết. Tiếp theo, nó thực hiện các bước tối ưu hóa như loại bỏ các biến và kênh giao tiếp không liên quan đến việc gọi các hoạt động của máy B. Một bước quan trọng là xử lý vấn đề tương đồng tên (homonym) và tự động suy ra kiểu dữ liệu cho các biến được dịch từ CSP (vì CSP không yêu cầu khai báo kiểu chặt chẽ như B). Cuối cùng, nó tạo ra hai file: một máy B trừu tượng và một máy B tinh chỉnh (refinement). Máy B tinh chỉnh chứa logic điều khiển được dịch từ CSP. Điểm đặc biệt là công cụ có thể phân tích các biến toàn cục được sử dụng trong mỗi khối xử lý để xác định xem một mệnh đề (cb = xᵢ ⇒ Pᵢ) có cần thiết trong CLI hay không. Nếu cần, nó sẽ chỉ ra dạng của Pᵢ, giúp người dùng giảm đáng kể công sức.

5.3. Kết quả kiểm chứng trên AtelierB và FDR2 cho đồ án tốt nghiệp

Toàn bộ mô hình hệ thống xe tự hành đã được xác minh thành công bằng các công cụ chuyên dụng. Các bộ điều khiển CSP (CtrlVehicle, CtrlDrivingSystem, CtrlNet) được chứng minh là deadlock-free và divergence-free bằng công cụ FDR2. Các máy B (Vehicle, DrivingSystem, Net) được chứng minh là đúng đắn bằng công cụ AtelierB, với tất cả các nghĩa vụ chứng minh đều được thông qua. Quan trọng nhất, tính nhất quán của các thành phần đã được xác minh bằng chính công cụ do tác giả phát triển. Các máy B điều khiển được tạo ra tự động đều được AtelierB chứng minh là đúng, cho thấy sự tương thích hoàn hảo giữa các bộ điều khiển CSP và máy B tương ứng. Thành công này không chỉ xác nhận tính đúng đắn của mô hình xe tự hành mà còn chứng minh tính hiệu quả và giá trị thực tiễn của công cụ tự động hóa đã được xây dựng trong khuôn khổ đồ án tốt nghiệp thạc sĩ xây dựng hệ thống này.

VI. Kết luận và định hướng phát triển từ luận văn thạc sĩ VNU

Luận văn thạc sĩ này đã đạt được hai thành tựu lớn. Thứ nhất, nó đã xây dựng thành công một mô hình hình thức toàn diện bằng CSP||B cho hệ thống xe tự hành theo đoàn, bao gồm cả bốn chế độ hoạt động quan trọng. Mô hình này, với việc giới thiệu thành phần trung gian Net, đã giải quyết được các thách thức trong việc mô tả các hành vi động và phức tạp của hệ thống. Đây là một luận văn thạc sĩ kỹ thuật xây dựng hệ thống phần mềm mẫu mực, thể hiện khả năng áp dụng lý thuyết cao cấp vào giải quyết vấn đề thực tiễn. Thứ hai, và có lẽ quan trọng hơn, luận văn đã đóng góp một công cụ phần mềm giúp tự động hóa việc xác minh tính nhất quán trong CSP||B. Công cụ này làm giảm đáng kể rào cản về chuyên môn và thời gian, giúp phương pháp CSP||B trở nên dễ tiếp cận và khả thi hơn trong các dự án công nghiệp. Các đóng góp này không chỉ có giá trị học thuật mà còn mở ra nhiều hướng phát triển trong tương lai, đặc biệt trong bối cảnh các hệ thống tự hành và tương tác ngày càng trở nên phổ biến. Luận văn này, dù được viết bằng tiếng Pháp (như một luận văn tiếng Anh ngành xây dựng hệ thống cần tham khảo), là một tài liệu quan trọng trong thư viện đại học quốc gia.

6.1. Tổng kết những đóng góp chính của khóa luận thạc sĩ xây dựng hệ thống

Những đóng góp cốt lõi của khóa luận thạc sĩ xây dựng hệ thống này có thể được tóm tắt như sau. Về mặt mô hình hóa, luận văn đã cải tiến và mở rộng một mô hình hiện có để bao quát toàn bộ vòng đời hoạt động của một xe tự hành, từ di chuyển độc lập đến tham gia và rời khỏi đội hình. Việc sử dụng thành phần Net là một giải pháp kiến trúc hiệu quả để xử lý giao tiếp động. Về mặt xác minh, đóng góp nổi bật là việc phát triển một công cụ tự động dịch CSP sang B và hỗ trợ tìm kiếm Bất biến Vòng lặp Điều khiển (CLI). Công cụ này không chỉ giúp xác minh thành công mô hình của chính luận văn mà còn có thể được áp dụng cho các mô hình CSP||B khác, tăng cường tính thực tiễn của phương pháp. Việc trích dẫn tài liệu tham khảo từ các công trình của H. Treharne và áp dụng thành công cho thấy sự nắm vững lý thuyết của tác giả.

6.2. Hướng nghiên cứu tương lai và tiềm năng ứng dụng thực tiễn

Luận văn cũng đã mở ra nhiều hướng nghiên cứu tiềm năng trong tương lai. Mô hình hiện tại vẫn ở mức độ trừu tượng. Một hướng phát triển tự nhiên là thực hiện các bước tinh chỉnh (refinement) để đưa mô hình đến gần hơn với mã nguồn có thể thực thi. Tác giả đề xuất một ý tưởng là thêm một thành phần con Perception vào mỗi xe. Thành phần này sẽ tự xây dựng một "bức tranh" về môi trường xung quanh, giúp xe giảm sự phụ thuộc vào Net và tiến tới một kiến trúc phân tán hơn. Về mặt công cụ, trình dịch tự động có thể được cải tiến để có khả năng tạo ra một CLI hoàn chỉnh thay vì chỉ đề xuất dạng. Về ứng dụng thực tiễn, mô hình và phương pháp xác minh này có thể được áp dụng không chỉ cho xe tự hành mà còn cho các hệ thống phức tạp khác như robot công nghiệp, hệ thống không người lái, hay các giao thức mạng, nơi tính an toàn và đúng đắn là yêu cầu tối quan trọng.

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

IFI LORIA Hanoï, Vietnam Nancy, France MÉMOIRE DE FIN D'ÉTUDES Construction d'un platoon en CSP||B Stagiaire : Huu-Nghia Nguyen Promotion 13, option Systèmes et Réseaux Encadrants : Jean-Pierre Jacquot Jeanine Souquières Lieu de stage : Équipe DEDALE - LORIA Campus Scientique, BP 239 F-54506 Vandu÷vre lès Nancy Cedex Nancy, le 28 octobre 2009 LUAN VAN CHAT LUONG download : add [e-mail] i Remerciements Je tiens tout d'abord à remercier Jeanine Souquières de m'avoir accueilli au sein de l'équipe de recherche DEDALE - LORIA Je tiens particulièrement à remercier Jean-Pierre Jacquot qui m'a aidé beaucoup avec les conseils utiles sur la direction et la méthode de recherche pendant toute la durée du stage. Je voudrais remercier également les personnes dans l'équipe DEDALE pour leur sympathie et leur environnement de travail très chaleureux Mes plus sincères remerciements vont à tous les professeurs et les personnels de l'IFI pour m'avoir donné des cours et pour leur soutien tout au long de mes études à l'IFI. En n, un grand merci à mes amis, à ma famille qui sont toujours près de moi et m'encourage à passer la diculté. LUAN VAN CHAT LUONG download : add [e-mail] ii Résumé : Ce travail a été réalisé dans le cadre des projets TACOS et CRISTAL qui ont pour but de construire un système des véhicules autonomes en libre-service.

Dans ce système, les véhicules peuvent se déplacer en convoi. Nous partons d'une modélisation d'un convoi en CSP||B. Elle décrit les processus internes des véhicules membres qui maintiennent la distance entre véhicules, de sorte que la propriété de déplacement en convoi est conservée. Le travail de stage a eu pour premier but de modéliser en CSP||B les processus internes des véhicules pour accrocher et décrocher d'un convoi.

Nous avons amélioré le modèle existant pour avoir un nouveau modèle qui présente les processus de quatre modes de fonctionnement : déplacement en convoi, décrochage d'un convoi, déplacement indépendant et accrochage à un convoi. Un second axe a été consacré à la théorie de l'approche CSP||B. CSP||B, qui apparait dans les années 2000, est la combinaison de la méthode B et de l'algèbre CSP. Elle n'est pas encore totalement achevée.

Une modélisation en CSP||B comporte plusieurs composants CSP||B. Chaque composant CSP||B contient une machine B et un contrôleur CSP. Il existe des outils pour vérier les machines B et leur contrôleur CSP. Cependant, il n'existe pas encore d'outil qui permet de vérier la cohérence entre la machine B et son contrôleur CSP.

Nous avons construit un logiciel qui permet de résoudre ce problème. Mots clés : CSP||B, composants logiciel, platoon, vérication formelle Abstract : First, we want to model in CSP||B the behavior of a vehicle when it joins or disjoins a platoon. We extend a model of platoon in which members maintain the distance between them so that the form of the platoon is preserved. However, the hooking and unhooking processes of a vehicle in a convoy are more complex.

We have a new model, written in CSP||B, of platoons. This models de- scribes all behaviors of vehicles : autonomous movement, joining a convoy, movement as a member of a convoy, and disjoining a convoy. Second, our work addressed the practical implementation of the theory of the CSP||B approach. This approach, which appeared in 2000, is driven by the desire to exploit existing tool support for verifying both CSP and B specications and by the need for compositional proof techniques.

However, there is no tool for verifying the con- sistency between B-machines and their CSP controler. We built a tool to solve this problem. Keywords : CSP||B, software component, platoon, formal verication LUAN VAN CHAT LUONG download : add [e-mail] Table des matières 1 Introduction 1 1.2 Objectifs initiaux du stage .4 Structure du rapport .2 Communicating sequential processes - CSP .3 Vérication d'une modélisation CSP||B. 15 3 Modèle du système des véhicules 16 3.1 Modèle P LAT OON existant .2 Système des véhicules .2 Modes de fonctionnement du véhicule .3 Structure du code CSP||B.

28 LUAN VAN CHAT LUONG download : add [e-mail] Table des matières iv 3. 29 4 Vérication de la cohérence entre la machine B et le contrôleur CSP 31 4.1 Cohérence entre la machine B et son contrôleur CSP .1 Control Loop Invariant - CLI .2 Les règles de traduction .2 Comment ça marche ? .3 Les problèmes à résoudre .4 Recherche de la forme du CLI .4 Programmation en Ocaml. 43 5 Conclusion et perspectives 44 Bibliographie 46 A Modèle du système en CSP||B 48 A.1 Dénitions générales .1 Le contrôleur CSP : Vehicle.2 La machine B : Vehicle.1 Le contrôleur CSP : DrivingSystem. 52 LUAN VAN CHAT LUONG download : add [e-mail] Table des matières v A.2 La machine B : DrivingSystem.1 Le contrôleur CSP : Net.2 La machine B : Net.

57 B La vérication des machines B 62 C La vérication des contrôleurs CSP 63 D La vérication de la cohérence des composants 64 D.1 La machine traduite du contrôleur CSP CtrlV ehicle .1 La machine abstraite .2 Le ranement .2 La machine traduite du contrôleur CSP CtrlDrivingSystem .1 La machine abstraite .2 Le ranement .3 La machine traduite du contrôleur CSP CtrlN et .1 La machine abstraite .2 Le ranement .2 Structure du projet .1 Traiter des données .2 Construire la machine abstraite .3 Éviter des non pertinences .4 Éviter des homonymes. 79 LUAN VAN CHAT LUONG download : add [e-mail] Table des matières vi E.6 Chercher la form CLI .7 Construire le ranement. 81 LUAN VAN CHAT LUONG download : add [e-mail] Table des gures 1.1 Véhicules se déplacent en convoi .2 Modes des fonctionnement du système .2 Exemple de copie de donnée .4 Architecture CSP||B de Robot .5 La modélisation CSP||B du Robot .1 Modèle du convoi sans Net .2 Activité de véhicule dans le convoi .3 Modèle du convoi avec Net .4 Structure en CSP||B du Cristal .5 Système des véhicules .6 Changement du mode .7 Cristal en CSP||B .8 Structure du système en CSP||B .12 Vérication de la machine B .13 Vérication du contrôleur CSP .1 Le prototype de la machine B traduite d'un contrôleur CSP .2 Traduction de CSP en B. 40 LUAN VAN CHAT LUONG download : add [e-mail] Table des gures viii 4.4 Fichiers de codage .5 Vérication de la cohérence entre la machine B et le contrôleur CSP 41 LUAN VAN CHAT LUONG download : add [e-mail] Chapitre 1 Introduction Sommaire 1.2 Objectifs initiaux du stage .4 Structure du rapport.

5 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.1 Contexte 1 2 Ce stage se situe dans le cadre des projets TACOS et CRISTAL. Ils ont pour ob- jectif d'étudier la conception de nouveaux systèmes de transports urbains construits sur la base de véhicules électriques autonomes en libre-service. Un système se compose de n véhicules. Chaque véhicule fonctionne de façon au- tonome.

Un véhicule est muni des équipements qui ont la capacité de détecter la vitesse et la position des autres véhicules. Voici quelques informations sur le véhicule :  vitesse maximale en convoi 40 km/h  vitesse maximale d'une remorque 50 km/h  masse à vide et en charge : 900 kg  2000 kg  accélération max : 1m/s 2 2  décélération max : 1.3m/s , jusqu'à 3m/s 2 en urgence Dans ce système, on veut former des convois de véhicules (par exemple, à partir des véhicules qui se déplacent dans une même direction). Le nombre de véhicules dans un convoi est inférieur à un nombre prédéterminé. Le premier véhicule d'un convoi (le leader) est conduit par un utilisateur.

Il n'y a pas de relation physique entre les membres d'un convoi. Un membre du convoi va percevoir des informations du véhicule précédent pour ajuster sa vitesse an de maintenir une distance convenable avec son prédécesseur.1: Véhicules se déplacent en convoi Un véhicule peut quitter un convoi (décrochage) pour en rejoindre un autre (ac- 1 http://tacos.fr/ 2 http://projet-cristal.net/ LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Après avoir décroché d'un convoi, le véhicule est conduit manuellement ; il passera à nouveau en mode automatique quand il s'accrochera à un autre convoi. Ainsi, nous avons 4 modes de fonctionnement d'un véhicule : SOLO , P LAT OON , JOIN T et DISJOIN T .2: Modes des fonctionnement du système  Dans le mode stable SOLO , les véhicules se déplacent indépendamment les uns des autres.

Ils sont conduits manuellement.  Dans le mode stable P LAT OON , les véhicules se déplacent en convoi. Chaque véhicule suit celui qui le précède. Le leader du convoi est conduit manuellement.

 Le mode transitoire JOIN T représente le processus d'accrochage d'un véhicule à un convoi. Il intervient pour faire basculer le véhicule du mode SOLO au mode P LAT OON.  Le véhicule fonctionne dans le mode transitoire DISJOIN T quand il veut décrocher d'un convoi. L'équipe DEDALE a utilisé CSP||B pour modéliser le fonctionnement d'un convoi.

Dans ce modèle, deux modes de fonctionnement du véhicule, SOLO et P LAT OON , ont été spéciés. 3 L'approche CSP||B apparait dans des années 2000. Elle est la combinaison de deux méthodes formelles : la méthode B et l'algèbre CSP. Elle prote des avantages de ces deux méthodes, en particulier des bases théoriques ainsi que des outils supports.

3 Prononciation : CSP parallèle B LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Objectifs initiaux du stage 4 1.2 Objectifs initiaux du stage À partir du modèle existant, nous allons continuer à réaliser les modes JOIN T et DISJOIN T. Modélisation du comportement d'un convoi avec l'accrochage et décrochage de véhicules à partir de la spécication CSP||B existante. Introduction des contraintes de position et d'intégrité pour prendre en compte les propriétés de non-collision.

Convergence de ces deux évolutions dans un même modèle.3 Résultats L'avantage de modèle existant est que les processus interne du véhicule dans les modes PLATOON et SOLO sont simples et explicites. Cependant, pour les proces- sus d'accrochage et de décrochage, le véhicule a besoin de processus plus complexes. Nous avons reformulé ce modèle pour avoir un modèle de système de véhicules qui présente les 4 modes de fonctionnement. Ce modèle est présenté en détail dans le chapitre 3.

Il est écrit en CSP||B. La vérication d'une modélisation en CSP||B pose un problème : il y a une étape de vérication qui est faite manuellement. Une modélisation en CSP||B comporte plusieurs composants CSP||B. Chaque composant CSP||B se compose également d'une machine B et d'un contrôleur CSP.

Il existe déjà des outils pour vérier les machines B (comme AtelierB, ProB, B4free, .) et les contrôleurs CSP (comme FDR2, ProB, Arc,. Cependant, il n'existe pas encore d'outil qui permet de véri- er la cohérence entre les machine B et leur contrôleur CSP. Nous avons construit un logiciel qui permet de résoudre ce problème. Il est basé sur la technique du Con- trol Loop Invariant proposée par Helen Treharne.

Avec ce logiciel, on peut vérier totalement automatiquement une modélisation CSP||B. LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Structure du rapport 5 1.4 Structure du rapport La suite du rapport contient 4 chapitres et des annexes. Chapitre 2 - Approche CSP||B.

C'est un résumé de l'approche CSP||B. Nous avons présenté également un exemple 2.4 pour mieux comprendre cette ap- proche. Chapitre 3 - Modèle du système des véhicules. Ce chapitre présente rapide- ment le modèle existant.

Il présente également notre modèle : la structure, les modes de fonctionnement du véhicule et la vérication. Chapitre 4 - Vérication de la cohérence entre la machine B et le con- trôleur CSP. Ce chapitre présente la théorie de la cohérence entre la machine B et le contrôleur CSP dans un composant CSP||B. L'essentiel du chapitre est consacré à présenter un logiciel qui a pour but d'automatiser cette vérication.

Chapitre 5 - Conclusion et perspective. Elles contiennent les spécications développées au cours du stage ainsi qu'une documentation sur l'implantation du traducteur.