Kiểm chứng phần mềm dựa trên biểu đồ tuần tự trong công nghệ thông tin

LỜI CAM ĐOAN

LỜI CẢM ƠN

TÓM TẮT

1. CHƯƠNG 1: GIỚI THIỆU

1.1. Đặt vấn đề

2. CHƯƠNG 2: KIÊN THỨC NỀN TẢNG

2.1. Mô hình của thành phần phần mềm

2.2. Hệ thống chuyển trạng thái được gán nhãn

2.3. Phép ghép nối song song

2.4. LTS an toàn, thuộc tính an toàn, tính thỏa mãn và LTS lỗi

2.5. Ôtômát hữu hạn trạng thái đơn định

2.6. OtOmat VÀO/Tâ

2.7. Kiểm chứng giả định - đảm bảo (Assume - Guarantee Verification)

2.8. Lý thuyết giả định

2.9. Bộ công cụ LTSA (Labelled Transition Systems Analyzer)

3. CHƯƠNG 3: PHƯƠNG PHÁP SINH MÔ HÌNH VÀ KIỂM CHỨNG TÍNH ĐÚNG DẠNG THIẾT KẾ CHO CÁC PHẦN MỀM DỰA TRÊN THÀNH PHẦN

3.1. Các nghiên cứu liên quan

3.2. Phân tích biểu đồ tuần tự

3.3. Định dạng của đầu vào biểu đồ tuần tự

3.4. Sinh biểu thức chính quy cho phân đoạn Option

3.5. Sinh biểu thức chính quy cho phân đoạn Break/Critical/Strict

3.6. Sinh biểu thức chính quy cho phân đoạn Alternative

3.7. Sinh biểu thức chính quy cho phân đoạn Loop

3.8. Sinh biểu thức chính quy cho phân đoạn Consider

3.9. Sinh biểu thức chính quy cho phân đoạn Ignore

3.10. Sinh biểu thức chính quy cho phân đoạn Parallel và Sequencing

3.11. Sinh biểu thức chính quy cho biểu đồ tuần tự

3.12. Sinh mô hình cho thành phần sử dụng thuật toán CNNFA

3.13. Tổng quan về CNNFA

3.14. Sinh biểu diễn CNNFA cho các biểu thức chính quy thành phần

3.15. Phương pháp duyệt biểu thức chính quy

3.16. Sinh các mô hình cho các thành phần

3.17. Tối ưu hóa mô hình

3.18. Ví dụ sinh mô hình cho thành phần phần mềm bằng thuật toán CNNFA

3.19. Kiểm chứng tính đúng đắn của biểu đồ tuần tự

3.20. Công cụ hỗ trợ và thực nghiệm

3.21. Kiến trúc công cụ

3.22. Thực nghiệm và đánh giá phần sinh mô hình

3.23. Thực nghiệm và đánh giá phần kiểm chứng giả định - đảm bảo

4. CHƯƠNG 4: PHƯƠNG PHÁP SINH MÔ HÌNH VÀ KIỂM CHỨNG TÍNH ĐÚNG DẠNG CỦA CÁC BIỂU ĐỒ TUẦN TỰ UML 2.0 SỬ DỤNG ÔTÔMÁT VÀO/RA

4.1. Các nghiên cứu liên quan

4.2. Phân tích biểu đồ tuần tự thành các khối đơn

4.3. Định dạng của đầu vào biểu đồ tuần tự

4.4. Phân tích biểu đồ tuần tự thành các khối đơn

4.5. Sinh mô hình từ các khối đơn của biểu đồ tuần tự

4.6. Thuật toán xác định tập các luật chuyển cho ôtômát vào/ra từ khối đơn không chứa phân đoạn nào

4.7. Thuật toán xác định tập các luật chuyển cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Option

4.8. Thuật toán xác định tập các luật chuyển cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Alternative

4.9. Thuật toán xác định tập các luật chuyển cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Loop

4.10. Thuật toán xác định tập các luật chuyển cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Break

4.11. Thuật toán xác định tập các luật chuyển cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Parallel

4.12. Thuật toán xác định tập các luật chuyển cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Sequencing

4.13. Thuật toán xác định tập các luật chuyển cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Refine

4.14. Thuật toán xác định tập các luật chuyển cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Consider

4.15. Thuật toán xác định tập các luật chuyển cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Ignore

4.16. Xây dựng ôtômát vào/ra cho đối tượng từ biểu đồ tuần tự

4.17. Sinh đặc tả Promela từ Ôtômát vào/ra

4.18. Công cụ hỗ trợ và thực nghiệm

4.19. Kiến trúc công cụ

5. CHƯƠNG 5: MỘT SỐ CẢI TIẾN PHƯƠNG PHÁP KIỂM CHỨNG GIẢ ĐỊNH - ĐẢM BẢO

5.1. Giới thiệu

5.2. Các nghiên cứu liên quan

5.3. Phương pháp sinh giả định sử dụng thuật toán L*

5.4. Sinh giả định sử dụng thuật toán Ƒ*

5.5. Cập nhật bảng quan sát

5.6. Cải tiến phương pháp sinh giả định sử dụng thuật toán L*

5.7. Một ví dụ về lặp vô hạn

5.8. Cải tiến về phân tích phân ví dụ

5.9. Cải tiến giảm số truy vấn thành viên

5.10. Công cụ hỗ trợ và thực nghiệm

5.11. Phương pháp sinh giả định nhỏ nhất cục bộ

5.12. Kỹ thuật cải tiến cho trả lời truy vấn thành viên

5.13. Sinh giả định nhỏ nhất cục bộ

5.14. Cải tiến kỹ thuật cập nhật cho bảng quan sát

5.15. Phân tích kết quả truy vấn ứng viên

5.16. Ví dụ minh họa

5.17. Công cụ hỗ trợ và thực nghiệm

6. CHƯƠNG 6: CÁC KẾT QUẢ ĐẠT ĐƯỢC, NHỮNG HẠN CHẾ VÀ HƯỚNG NGHIÊN CỨU TIẾP THEO

DANH SÁCH HÌNH VẼ

DANH SÁCH BẢNG

THUẬT NGỮ VÀ TỪ VIẾT TẮT

I. Giới thiệu

Trong bối cảnh phát triển phần mềm hiện đại, kiểm chứng phần mềm trở thành một yếu tố quan trọng để đảm bảo chất lượng và tính đúng đắn của sản phẩm. Luận án này tập trung vào việc sử dụng biểu đồ tuần tự trong công nghệ thông tin để hỗ trợ quá trình kiểm chứng. Phân tích phần mềm thông qua các mô hình như Labeled Transition Systems (LTS) giúp xác định các thuộc tính an toàn và tính thỏa mãn của hệ thống. Việc áp dụng các phương pháp kiểm chứng như kiểm chứng giả định - đảm bảo (Assume-Guarantee Verification) cho phép kiểm tra tính đúng đắn của các thành phần phần mềm mà không cần ghép nối chúng lại với nhau. Điều này không chỉ giảm thiểu độ phức tạp mà còn giải quyết vấn đề bùng nổ không gian trạng thái trong kiểm chứng mô hình.

1.1. Các đóng góp chính của luận án

Luận án đã đề xuất một phương pháp hoàn chỉnh nhằm tự động sinh mô hình và kiểm chứng tính đúng đắn của các thiết kế phần mềm được biểu diễn bằng biểu đồ tuần tự UML 2.0. Phương pháp này không chỉ giúp giảm thiểu thời gian và chi phí phát triển mà còn đảm bảo chất lượng sản phẩm. Các mô hình được sinh ra từ biểu đồ tuần tự sẽ được kiểm chứng bằng các công cụ hiện có, từ đó cung cấp một cái nhìn tổng quan về tính đúng đắn của thiết kế. Việc áp dụng các công cụ như LTSA (Labelled Transition Systems Analyzer) cho phép thực hiện kiểm chứng một cách hiệu quả và chính xác.

II. Phương pháp kiểm chứng

Phương pháp kiểm chứng được đề xuất trong luận án dựa trên việc sử dụng mô hình hóa và kiểm chứng mô hình. Các mô hình được sinh ra từ biểu đồ tuần tự sẽ được chuyển đổi thành các ô-tô-mát vào/ra (I/O automata) để thực hiện kiểm chứng. Điều này giúp duy trì tính hướng đối tượng của thiết kế phần mềm trong các biểu đồ tuần tự. Hơn nữa, việc chuyển đổi từ mô hình sang ngôn ngữ PROMELA cho phép sử dụng bộ công cụ SPIN để kiểm chứng tính đúng đắn của hệ thống. Phương pháp này không chỉ giúp kiểm chứng các thuộc tính an toàn mà còn mở rộng khả năng kiểm chứng cho nhiều loại thuộc tính khác.

2.1. Kiểm chứng giả định đảm bảo

Kiểm chứng giả định - đảm bảo là một phương pháp hứa hẹn trong việc kiểm chứng từng phần của hệ thống. Phương pháp này yêu cầu các giả định về môi trường mà mỗi hệ thống con sẽ được thực hiện. Tuy nhiên, độ phức tạp trong việc sinh giả định vẫn còn cao, và các phương pháp hiện tại chỉ mới giải quyết được các hệ thống đơn giản. Luận án đã đề xuất các cải tiến nhằm giảm thiểu độ phức tạp này, từ đó nâng cao hiệu quả của phương pháp kiểm chứng. Việc áp dụng các thuật toán như L* giúp tối ưu hóa quá trình sinh giả định và kiểm chứng, từ đó cải thiện đáng kể tính hiệu quả của phương pháp.

III. Kết quả thực nghiệm

Luận án đã thực hiện nhiều thí nghiệm để đánh giá tính hiệu quả của các phương pháp đề xuất. Các kết quả cho thấy rằng việc sử dụng biểu đồ tuần tự trong công nghệ thông tin không chỉ giúp cải thiện quy trình phát triển phần mềm mà còn nâng cao chất lượng sản phẩm cuối cùng. Các công cụ hỗ trợ đã được cài đặt và thực nghiệm với nhiều ví dụ điển hình, cho thấy tính đúng đắn và hiệu quả của phương pháp kiểm chứng. Kết quả thực nghiệm cũng chỉ ra rằng việc áp dụng các phương pháp này có thể giảm thiểu đáng kể thời gian và chi phí kiểm chứng, đồng thời đảm bảo tính đúng đắn của thiết kế phần mềm.

3.1. Đánh giá và phân tích

Các kết quả thực nghiệm cho thấy rằng phương pháp kiểm chứng đề xuất có khả năng xử lý các hệ thống phức tạp với nhiều thành phần. Việc kiểm chứng từng phần giúp giảm thiểu bùng nổ không gian trạng thái, từ đó nâng cao khả năng áp dụng trong thực tế. Hơn nữa, các công cụ hỗ trợ đã được phát triển cho phép tự động hóa quá trình kiểm chứng, giúp tiết kiệm thời gian và nguồn lực. Điều này chứng tỏ rằng việc áp dụng kiểm chứng phần mềm dựa trên biểu đồ tuần tự là một giải pháp khả thi và hiệu quả cho các vấn đề hiện tại trong phát triển phần mềm.

Luận án tiến sĩ về kiểm chứng phần mềm dựa trên biểu đồ tuần tự trong công nghệ thông tin