Phương Pháp Mô Hình và Xác Minh Hệ Thống Dựa Trên Sự Kiện

• Trường học: Trường Đại Học
• Chuyên ngành: Kỹ Thuật Phần Mềm
• Đề tài: Phương Pháp Mô Hình và Xác Minh Hệ Thống Dựa Trên Sự Kiện
• Loại tài liệu: Luận Văn
• Năm xuất bản: 2023
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI MỞ ĐẦU
• 1. CHƯƠNG 1: INTRODUCTION
• 1.1. Classical set theory
• 1.2. Fuzzy sets and Fuzzy If-Then rules
• 1.3. Formal methods
• 1.4. Event-B mathematical language
• 1.5. Database systems and database triggers
• 2. CHƯƠNG 2: MODELING AND VERIFYING DATABASE TRIGGER SYSTEMS
• 2.1. Modeling database systems
• 2.2. Verifying system properties
• 2.3. A case study: Human resource management application
• 3. CHƯƠNG 3: MODELING AND VERIFYING CONTEXT-AWARE SYSTEMS
• 3.1. Formalizing context awareness
• 3.2. Modeling context-aware systems
• 3.3. Implementation using refinement
• 3.4. A case study: Adaptive cruise control system
• 3.5. Refinement: Adding weather and road sensors
• 3.6. Verifying system properties
• 4. CHƯƠNG 4: MODELING AND VERIFYING IMPRECISE SYSTEM REQUIREMENTS
• 4.1. Modeling fuzzy requirements
• 4.2. Representation of fuzzy terms in classical sets
• 4.3. Modeling discrete states
• 4.4. Verifying safety and eventuality properties
• 4.5. A case study: Container crane control
• 4.6. Modeling the container crane control system
• 4.7. First refinement: Modeling continuous behavior
• 4.8. Second refinement: Modeling eventuality property
• 5. CHƯƠNG 5: MODELING AND VERIFYING IMPRECISE SYSTEM REQUIREMENTS
• 5.1. Modeling fuzzy requirements
• 5.2. Representation of fuzzy terms in classical sets
• 5.3. Modeling discrete states
• 5.4. Verifying safety and eventuality properties
• 5.5. A case study: Container crane control
• 5.6. Modeling the container crane control system
• 5.7. First refinement: Modeling continuous behavior
• 5.8. Second refinement: Modeling eventuality property
• PHỤ LỤC
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan Phương Pháp Mô Hình Hóa Hệ Thống Dựa Trên Sự Kiện

Mô hình hóa và xác minh độ tin cậy của phần mềm đóng vai trò quan trọng trong kỹ thuật phát triển phần mềm. Các công nghệ kỹ thuật phần mềm giới thiệu nhiều phương pháp hoặc kiểu kiến trúc khác nhau, mỗi hệ thống dựa trên một kiến trúc khác nhau để xác minh tính chính xác của nó. Trong số các kiến trúc này, kiến trúc hướng sự kiện thường được sử dụng rộng rãi trong cả học thuật và công nghiệp. Mục tiêu của luận án này là đề xuất các phương pháp hiệu quả để mô hình hóa và xác minh các quy tắc của hệ thống hướng sự kiện. Luận án này xem xét các loại hệ thống cụ thể như hệ thống cơ sở dữ liệu sử dụng Event-Condition-Action (ECA) và các hệ thống nhận biết ngữ cảnh, sau đó sử dụng Event-B và các công cụ hỗ trợ của nó để phân tích các hệ thống này. "Mô hình hóa là một trong những cách hiệu quả để xử lý sự phức tạp của phát triển phần mềm cho phép thiết kế và đánh giá các yêu cầu của hệ thống."

1.1. Tầm quan trọng của mô hình hóa hệ thống phần mềm

Mô hình hóa hệ thống phần mềm là rất quan trọng vì nó giúp các kỹ sư phần mềm hiểu rõ hơn về những gì họ đang phát triển. Mô hình hóa cho phép thiết kế và đánh giá các yêu cầu của hệ thống, giúp giảm thiểu rủi ro và chi phí phát triển. Có nhiều loại ngôn ngữ mô hình hóa, bao gồm ngôn ngữ đồ họa, ngôn ngữ văn bản và ngôn ngữ đại số. Việc lựa chọn ngôn ngữ mô hình hóa phù hợp phụ thuộc vào loại hệ thống và mục tiêu của dự án. Mô hình hóa hệ thống thông tin không chỉ thể hiện nội dung một cách trực quan mà còn cung cấp nội dung bằng văn bản.

1.2. Các loại kiến trúc hệ thống hướng sự kiện phổ biến

Kiến trúc hướng sự kiện là một trong những kiến trúc phổ biến nhất trong phát triển dự án phần mềm, cung cấp lời gọi ngầm thay vì gọi trực tiếp các quy trình. Mỗi thành phần của một hệ thống hướng sự kiện có thể tạo ra các sự kiện, sau đó hệ thống sẽ gọi tất cả các quy trình đã đăng ký với các sự kiện này. Một hệ thống hướng sự kiện bao gồm ba phần thiết yếu: thành phần giám sát, thành phần truyền dẫn và thành phần phản hồi. Hệ thống hướng sự kiện làm việc bằng cách tạo và phản hồi các sự kiện, nó làm mất liên kết giữa các thành phần phần mềm và cải thiện khả năng tương tác với môi trường của nó.

II. Thách Thức Trong Xác Minh Hệ Thống Dựa Trên Sự Kiện Phức Tạp

Trong các hệ thống phần mềm, lỗi có thể gây ra nhiều thiệt hại không chỉ về kinh tế mà còn cả con người, đặc biệt là trong các ứng dụng trong hệ thống nhúng, điều khiển giao thông và thiết bị dịch vụ y tế. Lỗi thường xảy ra khi quá trình thực thi hệ thống không đáp ứng các đặc điểm và ràng buộc của đặc tả hệ thống phần mềm. Do đó, đảm bảo tính chính xác của hệ thống phần mềm luôn là một thách thức của quá trình phát triển phần mềm và độ tin cậy đóng vai trò quan trọng trong việc quyết định sự thành công của một dự án phần mềm. "Việc đảm bảo tính chính xác của hệ thống phần mềm là một thách thức trong quá trình phát triển phần mềm."

2.1. Hạn chế của kiểm thử truyền thống trong xác minh

Các kỹ thuật kiểm thử được sử dụng trong quá trình phát triển thông thường để kiểm tra xem quá trình thực thi phần mềm có đáp ứng các yêu cầu của người dùng hay không. Tuy nhiên, kiểm thử là một quá trình xác nhận không đầy đủ vì nó chỉ có thể xác định lỗi chứ không thể đảm bảo rằng quá trình thực thi phần mềm là chính xác trong mọi trường hợp. Kiểm thử phần mềm chỉ có thể xác định lỗi chứ không thể đảm bảo rằng phần mềm hoạt động chính xác trong mọi trường hợp.

2.2. Sự cần thiết của xác minh hình thức trong hệ thống phức tạp

Xác minh phần mềm là một trong những phương pháp mạnh mẽ để tìm hoặc chứng minh bằng toán học sự vắng mặt của các lỗi phần mềm. Một số kỹ thuật và phương pháp đã được đề xuất để xác minh phần mềm, chẳng hạn như kiểm tra mô hình, chứng minh định lý và phân tích chương trình. Trong số các kỹ thuật này, chứng minh định lý có những ưu điểm riêng biệt, chẳng hạn như kích thước vượt trội của hệ thống và khả năng suy luận quy nạp. Xác minh hệ thống giúp giảm chi phí xây dựng phần mềm.

III. Phương Pháp Mô Hình Hóa Hệ Thống Dựa Trên Sự Kiện Với Event B

Luận án đề xuất các phương pháp mới để đạt được mong muốn đó bằng cách sử dụng phương pháp hình thức Event-B. Đây là một sự phát triển của hình thức B đã được phát triển hơn mười năm trước và đã được áp dụng trong một số dự án công nghiệp. Nhiều nhà nghiên cứu và nhóm nghiên cứu trên khắp thế giới đã được truyền cảm hứng từ mô hình hóa và xác minh hệ thống với Event-B. Các ký hiệu Event-B dựa trên lý thuyết tập hợp, các phép thay thế tổng quát và logic bậc nhất. Nó phù hợp hơn để phát triển các hệ thống phản ứng và phân tán lớn. "Event-B hoàn toàn phù hợp để mô hình hóa và xác minh các hệ thống hướng sự kiện."

3.1. Giới thiệu về Event B và các thành phần chính

Phát triển phần mềm trong Event-B bắt đầu bằng cách chỉ định một cách trừu tượng các yêu cầu của toàn bộ hệ thống, sau đó tinh chỉnh chúng thông qua một số bước để đạt được mô tả về hệ thống chi tiết đến mức có thể được dịch thành mã. Tính nhất quán của mỗi mô hình và mối quan hệ giữa mô hình trừu tượng và các tinh chỉnh của nó được thu được bằng các chứng minh hình thức. Các công cụ hỗ trợ đã được cung cấp cho đặc tả và chứng minh Event-B trong nền tảng Rodin. Event-B là một phương pháp hình thức dựa trên lý thuyết tập hợp, các phép thay thế tổng quát và logic bậc nhất.

3.2. Quy trình tinh chỉnh mô hình trong Event B

Luận án hướng đến việc cung cấp các công cụ hỗ trợ cho việc dịch tự động từ một ứng dụng của hệ thống hướng sự kiện sang một mô hình Event-B mục tiêu giúp giảm bớt nỗ lực và giảm bớt những khó khăn trong quá trình mô hình hóa. Đầu ra của các công cụ này dự kiến sẽ có thể sử dụng được trong các công cụ hỗ trợ Event-B như Rodin. Quy trình tinh chỉnh giúp giảm chi phí phát triển hệ thống.

IV. Xác Minh Hệ Thống Cơ Sở Dữ Liệu Với Trigger Sử Dụng Event B

Đầu tiên, chúng tôi giới thiệu một phương pháp mới để dịch các phần tử để chính thức hóa hệ thống cơ sở dữ liệu bao gồm các cấu trúc trigger. Bằng cách đề xuất một tập hợp các quy tắc, chúng tôi chính thức kiểm tra tính bảo toàn ràng buộc dữ liệu và phát hiện các vòng lặp vô hạn của hệ thống. Sau khi mô hình hóa và luận án đề xuất một phương pháp tinh chỉnh hệ thống nhận biết ngữ cảnh cũng sử dụng các quy tắc Event-B để tăng dần công cụ. Xác minh hệ thống cơ sở dữ liệu giúp đảm bảo tính toàn vẹn của dữ liệu.

4.1. Mô hình hóa trigger cơ sở dữ liệu bằng Event B

Luận án này xem xét các loại hệ thống cụ thể như hệ thống cơ sở dữ liệu sử dụng Event-Condition-Action (ECA) và các hệ thống nhận biết ngữ cảnh, sau đó sử dụng Event-B và các công cụ hỗ trợ của nó để phân tích các hệ thống này. Mô hình hóa hệ thống cơ sở dữ liệu giúp đảm bảo tính toàn vẹn của dữ liệu.

4.2. Xác minh tính toàn vẹn dữ liệu và phát hiện vòng lặp vô hạn

Bằng cách đề xuất một tập hợp các quy tắc, chúng tôi chính thức kiểm tra tính bảo toàn ràng buộc dữ liệu và phát hiện các vòng lặp vô hạn của hệ thống. Phát hiện vòng lặp vô hạn giúp đảm bảo tính ổn định của hệ thống.

V. Mô Hình Hóa và Xác Minh Hệ Thống Nhận Biết Ngữ Cảnh

Thứ hai, xác minh các hệ thống nhận biết ngữ cảnh cũng sử dụng các quy tắc Event-B để tăng dần công cụ. Các ràng buộc mô hình hóa bảo tồn ngữ cảnh mà sử dụng ECA được chứng minh tự động với Rodin. Thứ ba, luận án này tiếp tục công việc về mô hình hóa các hệ thống hướng sự kiện có hành vi được chỉ định bởi các hệ thống thời gian dựa trên tinh chỉnh Fuzzy If-Then được mô tả với các yêu cầu không chính xác. Hệ thống nhận biết ngữ cảnh giúp hệ thống thích ứng với môi trường.

5.1. Biểu diễn ngữ cảnh và mô hình hóa hệ thống

Luận án này xem xét các loại hệ thống cụ thể như hệ thống cơ sở dữ liệu sử dụng Event-Condition-Action (ECA) và các hệ thống nhận biết ngữ cảnh, sau đó sử dụng Event-B và các công cụ hỗ trợ của nó để phân tích các hệ thống này. Mô hình hóa hệ thống nhận biết ngữ cảnh giúp hệ thống thích ứng với môi trường.

5.2. Tinh chỉnh mô hình và xác minh tính chất hệ thống

Các ràng buộc mô hình hóa bảo tồn ngữ cảnh mà sử dụng ECA được chứng minh tự động với Rodin. Xác minh tính chất hệ thống giúp đảm bảo tính chính xác của hệ thống.

VI. Kết Luận và Hướng Phát Triển Phương Pháp Mô Hình Hóa

Cuối cùng, chúng tôi sử dụng Event-B tinh chỉnh các phương pháp lý luận hiện có để xác minh cả các yêu cầu an toàn và các yêu cầu về tính chất và tính chất của các hệ thống. Luận án này đề xuất các phương pháp mới để đạt được mong muốn đó bằng cách sử dụng phương pháp hình thức Event-B. Phương pháp mô hình hóa giúp giảm chi phí phát triển hệ thống.

6.1. Tóm tắt các đóng góp chính của luận án

Luận án này xem xét các loại hệ thống cụ thể như hệ thống cơ sở dữ liệu sử dụng Event-Condition-Action (ECA) và các hệ thống nhận biết ngữ cảnh, sau đó sử dụng Event-B và các công cụ hỗ trợ của nó để phân tích các hệ thống này. Đóng góp chính của luận án là đề xuất các phương pháp mới để mô hình hóa và xác minh hệ thống.

6.2. Hướng nghiên cứu tiếp theo và ứng dụng tiềm năng

Luận án hướng đến việc cung cấp các công cụ hỗ trợ cho việc dịch tự động từ một ứng dụng của hệ thống hướng sự kiện sang một mô hình Event-B mục tiêu giúp giảm bớt nỗ lực và giảm bớt những khó khăn trong quá trình mô hình hóa. Hướng nghiên cứu tiếp theo là phát triển các công cụ hỗ trợ cho việc dịch tự động.