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

Luận án tiến sĩ công nghệ thông tin nghiên cứu đặc tả và kiểm chứng phần mềm qua biểu đồ tuần tự, nâng cao chất lượng phát triển phần mềm.

• Tác giả: Lê Chí Luận
• Người hướng dẫn: PGS. Phạm Ngọc Hùng
• Trường học: Đại học Quốc gia Hà Nội
• Chuyên ngành: Công nghệ thông tin
• Đề tài: Kiểm Chứng Phần Mềm Dựa Trên Biểu Đồ Tuần Tự Trong Công Nghệ Thông Tin
• Loại tài liệu: luận án tiến sĩ
• Năm xuất bản: 2018
• Địa điểm: Hà Nội

Mục lục chi tiết

• 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

Tóm 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.

Nội dung chính

Tổng quan luận án

Luận án tiến sĩ ngành Công nghệ thông tin, chuyên ngành Kỹ thuật phần mềm (mã số: 62.03) của nghiên cứu sinh Lê Chí Luận, được thực hiện dưới sự hướng dẫn khoa học của PGS. Phạm Ngọc Hùng và PGS. Hồ Sĩ Đàm tại Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội (bảo vệ năm 2018), tập trung vào đề tài sinh mô hình tự động và kiểm chứng tính đúng đắn cho các thiết kế phần mềm dựa trên thành phần.

Phát triển phần mềm dựa trên công nghệ hướng thành phần (Component-based Software Development - CBSD) là phương thức xây dựng phần mềm thông qua việc tích hợp các thành phần sẵn có nhằm rút ngắn thời gian và chi phí phát triển. Tuy nhiên, thách thức kỹ thuật cốt lõi của CBSD là việc bảo đảm các thành phần độc lập có thể cộng tác chính xác sau khi ghép nối ("plug-and-play"), đặc biệt trong các hệ thống đòi hỏi độ tin cậy cao như điều khiển máy bay, tàu hỏa, tên lửa, y tế và an ninh quốc phòng. Kiểm chứng mô hình (model checking) là giải pháp tự động hóa giúp bảo đảm chất lượng phần mềm ngay từ pha thiết kế. Dẫu vậy, phương pháp này gặp hai rào cản lớn:

1. Việc xây dựng mô hình đặc tả hành vi hình thức cho phần mềm từ tài liệu thiết kế (phổ biến là biểu đồ tuần tự UML 2.0) thường thực hiện thủ công, tốn kém thời gian và dễ phát sinh lỗi;
2. Vấn đề bùng nổ không gian trạng thái (state explosion problem) khi ghép nối mô hình của nhiều thành phần phần mềm để tiến hành kiểm chứng toàn cục.

Khoảng trống nghiên cứu được luận án xác định gồm: thiếu một quy trình khép kín tự động chuyển đổi từ tài liệu thiết kế UML 2.0 sang mô hình hình thức; các nghiên cứu kiểm chứng biểu đồ tuần tự trước đây không tách biệt bước sinh mô hình và bước kiểm chứng khiến mô hình không thể tái sử dụng; chưa hỗ trợ đầy đủ cú pháp các phân đoạn tương tác phức tạp của UML 2.0; và các thuật toán sinh giả định trong kiểm chứng từng phần hiện hành có độ phức tạp tính toán cao hoặc dễ rơi vào vòng lặp vô hạn.

Mục tiêu nghiên cứu của luận án được xác định gồm ba nội dung:

1. Đề xuất phương pháp tự động sinh mô hình đặc tả hành vi của thiết kế phần mềm dựa trên thành phần từ biểu đồ tuần tự UML 2.0 dưới dạng hệ thống chuyển trạng thái được gán nhãn (Labeled Transition Systems - LTS) và kết hợp với kỹ thuật kiểm chứng giả định - đảm bảo (Assume - Guarantee Verification - AGV) để kiểm chứng các thuộc tính an toàn (safety properties).
2. Đề xuất phương pháp sinh mô hình hành vi dưới dạng ôtômát vào/ra (I/O automata) cho các đối tượng trong biểu đồ tuần tự UML 2.0 nhằm duy trì tính tương tác hướng đối tượng, đồng thời chuyển đổi mô hình này sang ngôn ngữ Promela để kiểm chứng các thuộc tính logic thời gian tuyến tính (Linear Temporal Logic - LTL) thông qua công cụ SPIN.
3. Đề xuất các giải pháp cải tiến thuật toán học $L^*$ trong kiểm chứng giả định - đảm bảo nhằm giảm số lượng truy vấn, xử lý dứt điểm hiện tượng lặp vô hạn khi phân tích phản ví dụ, và sinh ra các giả định có ngôn ngữ nhỏ nhất cục bộ phục vụ tái kiểm chứng trong bối cảnh phần mềm tiến hóa.

Đối tượng và phạm vi nghiên cứu:

• Đối tượng nghiên cứu: Thiết kế của các hệ thống phần mềm dựa trên thành phần được mô hình hóa bằng biểu đồ tuần tự UML 2.0.
• Phạm vi nghiên cứu: Về mặt thiết kế, luận án giới hạn ở các biểu đồ tuần tự UML 2.0 được lưu trữ dưới định dạng tệp XML chuẩn hóa. Về mặt thuộc tính kiểm chứng, phương pháp tiếp cận với LTS hỗ trợ các thuộc tính an toàn (safety properties); phương pháp tiếp cận với ôtômát vào/ra và SPIN hỗ trợ kiểm chứng tập thuộc tính rộng hơn biểu diễn bằng công thức LTL. Về kiến trúc thực nghiệm, các thuật toán tập trung giải quyết hệ thống gồm hai thành phần và các ca kiểm thử điển hình, định hướng mở rộng cho hệ thống đa thành phần.

Tổng quan tài liệu và vị trí của luận án

Luận án đã phân tích và hệ thống hóa bốn hướng nghiên cứu chính liên quan đến đề tài:

Hướng thứ nhất: Các phương pháp sinh mô hình tự động cho thành phần phần mềm.

• Hung và cộng sự [27] tiếp cận thành phần phần mềm theo cơ chế hộp đen, thực thi các vết hành vi để thu thập chuỗi hành động, coi chuỗi này là biểu thức chính quy và dùng thuật toán Thompson [87] để sinh mô hình. Nhược điểm của giải pháp này là bị giới hạn bởi độ dài tối đa của vết thử nghiệm.
• Lorenzoli và cộng sự [71] đề xuất thuật toán GK-tail trích xuất mô hình máy trạng thái hữu hạn mở rộng (Extended Finite State Machine - EFSM) từ chuỗi tương tác kèm dữ liệu và điều kiện trên tham số gọi hàm, phụ thuộc vào phần mềm giám sát động.
• Corbett và cộng sự [26] phát triển bộ công cụ Bandera trích xuất mô hình từ mã nguồn Java, không thể áp dụng cho các thành phần phần mềm thương mại đóng gói từ bên thứ ba (COTS) do không có sẵn mã nguồn.
• Whittle và cộng sự [88] sinh mô hình môi trường phần mềm dựa trên giả định người dùng cung cấp thông tin môi trường, điều này thiếu tính khả thi trong thực tế thiết kế.
• Inoue và cộng sự [43] áp dụng thuật toán học $L^*$ để sinh mô hình từ biểu đồ tuần tự qua biểu thức chính quy, tuy nhiên chi phí tính toán bộ nhớ và thời gian rất lớn, đồng thời bị giới hạn bởi độ dài chuỗi hành vi.

Hướng thứ hai: Kiểm chứng từng phần và kiểm chứng mô hình trong bối cảnh tiến hóa.

• Fisler và Krishnamurthi [79] đưa ra phương pháp kiểm chứng từng phần (modular verification) cho các thiết kế phần mềm. Thang và Katayama [86] mở rộng phương pháp này cho ngữ cảnh phần mềm tiến hóa (khi thêm mới một thành phần) bằng cách sinh các ràng buộc hệ thống. Tuy nhiên, thuật toán sinh ràng buộc có độ phức tạp cao và giả định các mô hình thành phần đã có sẵn và chính xác.

Hướng thứ ba: Kỹ thuật kiểm chứng giả định - đảm bảo (Assume - Guarantee Verification - AGV).

• Bắt nguồn từ các nghiên cứu nền tảng của Pnueli [80] và Jones [55], phương pháp AGV được tự động hóa nổi bật bởi Cobleigh và cộng sự [25] nhờ việc áp dụng thuật toán học máy $L^*$ của Angluin [6] để sinh giả định $A$ biểu diễn môi trường của thành phần.
• Giannakopoulou, Pasareanu và Cobleigh [33, 34] nghiên cứu sâu về giả định yếu nhất (weakest assumption $A_w$).
• Li và cộng sự [50, 51, 52, 53] áp dụng $L^$ cho kiểm chứng giả định - đảm bảo và tối thiểu hóa giả định trong ngữ cảnh tiến hóa cho hệ thống hai thành phần. Dù vậy, độ phức tạp của thuật toán $L^$ khi mở rộng bảng quan sát vẫn cao và khả năng áp dụng thực tế còn hạn chế.

Hướng thứ tư: Hình thức hóa và kiểm chứng biểu đồ tuần tự UML.

• Các công trình của Aredo [8], Lima và cộng sự [70], Knapp và Wuttke [61], Zhao và cộng sự [90] (sử dụng Event Deterministic Finite Automata - EDTFA). Điểm hạn chế chung của các nghiên cứu này là không tách rời pha sinh mô hình khỏi pha kiểm chứng, dẫn tới không tái sử dụng được mô hình hình thức cho các hoạt động kiểm thử hay kiểm chứng lại về sau.

Khoảng trống luận án lựa chọn giải quyết: Luận án định vị nghiên cứu vào việc thiết lập một quy trình hoàn chỉnh: tự động phân tích cú pháp biểu đồ tuần tự UML 2.0 từ tệp XML, sinh biểu thức chính quy đầy đủ cho các phân đoạn tương tác phức tạp; áp dụng thuật toán CNNFA để tối ưu hóa việc chuyển đổi sang mô hình LTS; tích hợp mô hình này với AGV để kiểm chứng mà không cần ghép nối toàn cục; song song đó phát triển hướng tiếp cận dùng ôtômát vào/ra kết hợp SPIN/Promela; và trực tiếp giải quyết các điểm nghẽn tính toán của thuật toán học $L^*$ thông qua lưu trữ truy vấn bằng từ điển, kiểm soát việc chọn hậu tố tránh lặp vô hạn và sinh giả định nhỏ nhất cục bộ.

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

Luận án dựa trên nền tảng toán học của lý thuyết ngôn ngữ hình thức, ôtômát và logic kiểm chứng mô hình:

1. Hệ thống chuyển trạng thái được gán nhãn (Labeled Transition System - LTS): Mô hình của mỗi thành phần phần mềm được đặc tả bởi một LTS $M = (Q, \alpha M, \delta, q_0)$, trong đó:

   • $Q$ là tập hữu hạn các trạng thái khác rỗng;
   • $\alpha M \subseteq Act$ là tập các hành động quan sát được (bảng chữ cái của $M$);
   • $\delta \subseteq Q \times (\alpha M \cup {\tau}) \times Q$ là hàm chuyển trạng thái ($\tau$ là hành động nội bộ không quan sát được);
   • $q_0 \in Q$ là trạng thái khởi đầu.
   • Vết (trace) $\sigma$ trên $M$ là chuỗi hữu hạn các hành động $a_1 a_2 \dots a_n$ xuất phát từ $q_0$. Ngôn ngữ $L(M)$ là tập tất cả các vết của $M$.
   • Phép ghép nối song song giữa hai LTS $M_1 = (Q_1, \alpha M_1, \delta_1, q_0^1)$ và $M_2 = (Q_2, \alpha M_2, \delta_2, q_0^2)$, ký hiệu $M_1 \parallel M_2$, đồng bộ các hành động chung trên $\alpha M_1 \cap \alpha M_2$ và cho phép xen kẽ (interleaving) các hành động độc lập.
   • Thuộc tính an toàn (safety property) $p$ được biểu diễn bởi một LTS an toàn (không chứa trạng thái lỗi $\pi$). LTS lỗi $p_{err}$ được xây dựng từ $p$ bằng cách thêm trạng thái bẫy lỗi $\pi$. Hệ thống ghép nối $M \parallel p_{err}$ vi phạm thuộc tính $p$ nếu tồn tại vết dẫn tới trạng thái lỗi $\pi$.

2. Ôtômát hữu hạn và thuật toán CNNFA:

   • Ôtômát hữu hạn đơn định (DFA), ôtômát hữu hạn không đơn định (NFA), Normal NFA (NNFA) và McNaughton/Yamada NNFA (MYNNFA).
   • Biểu diễn CNNFA (Compressed NNFA) của Chang và Paige [18, 19]: Là dạng biểu diễn nén của ôtômát đuôi MYNNFA $M^T = (\Sigma^T, Q^T, \delta^T, I^T, F^T, \Lambda^T)$, được định nghĩa bằng bộ bảy thành phần $P^T = (\Sigma_D^T, Q_D^T, ld_D^T, l\delta_D^T, I_D^T, F_D^T, \Lambda_D^T)$. CNNFA quản lý các tập trạng thái bắt đầu và kết thúc thông qua hai cấu trúc dữ liệu rừng cây nhị phân kết hợp danh sách liên kết đôi là I-Forest và F-Forest, cho phép thực hiện phép hợp tập hợp không giao nhau trong thời gian đơn vị $O(1)$, giúp giảm đáng kể chi phí chuyển từ biểu thức chính quy sang ôtômát.

3. Ôtômát vào/ra (Input/Output Automata): Được định nghĩa lại theo hướng sự kiện là một bộ sáu: $A_{I/O} = (Q, \Sigma_1, \Sigma_2, \delta, q_0, F)$, trong đó:

   • $Q$ là tập trạng thái;
   • $\Sigma_1 = {(c, e) \mid c \in \mathcal{C}, e \in \mathcal{E}_{in}}$ là tập ký tự vào (nhận thông điệp $e$ từ kênh $c$);
   • $\Sigma_2 = {(c, e) \mid c \in \mathcal{C}, e \in \mathcal{E}_{out}}$ là tập ký tự ra (gửi thông điệp $e$ qua kênh $c$);
   • $\delta: Q \times (\mathcal{C} \times \mathcal{E}) \to Q$ là tập luật chuyển trạng thái;
   • $q_0$ là trạng thái khởi đầu và $F$ là tập trạng thái kết thúc.

4. Khung phân tích kiểm chứng giả định - đảm bảo (AGV): Sử dụng công thức bộ ba $\langle A(p) \rangle M \langle p \rangle$. Để kiểm chứng hệ thống hai thành phần $M = M_1 \parallel M_2$ thỏa mãn thuộc tính $p$, kỹ thuật áp dụng hai luật suy diễn:

   • Luật 1: $\langle A(p) \rangle M_1 \langle p \rangle$ (tương đương kiểm tra $A(p) \parallel M_1 \parallel p_{err}$ không chạm tới trạng thái lỗi $\pi$);
   • Luật 2: $\langle \text{true} \rangle M_2 \langle A(p) \rangle$ (tương đương kiểm tra $M_2 \parallel A(p)_{err}$ không chạm tới lỗi). Giả định $A(p)$ được học tự động thông qua thuật toán học $L^*$ của Angluin [6]. Thuật toán tương tác giữa người học (Learner) và người dạy (Teacher) thông qua bảng quan sát (Observation Table - $OT = (S, E, T)$) với tập tiền tố $S$, tập hậu tố $E$, và bảng ánh xạ $T$. Quá trình học sử dụng hai loại truy vấn: truy vấn thành viên (Membership Query - MQ) và truy vấn tương đương/ứng viên (Equivalence Query - EQ). Khái niệm giả định yếu nhất $A_w$ bảo đảm $M_1 \parallel E \models p \iff E \models A_w$.

Phương pháp thực nghiệm:

• Luận án xây dựng các bộ công cụ phần mềm độc lập bằng ngôn ngữ C# trên môi trường Microsoft Visual Studio.
• Nguồn dữ liệu: Các mô hình thiết kế chuẩn hóa dưới dạng tệp XML của hệ thống Mod2, hệ thống đặt vé, và các trường hợp thử nghiệm tổng hợp (TestCase1, TestCase2, TestCase3).
• Công cụ kiểm chứng phối hợp: LTSA (Labelled Transition Systems Analyzer) dùng để phân tích LTS và kiểm chứng AGV; SPIN model checker dùng để kiểm chứng mã Promela sinh từ ôtômát vào/ra.

Nội dung chính theo từng chương

Chương 1. Đặt vấn đề

Chương này phân tích bối cảnh phát triển phần mềm dựa trên thành phần (CBSD) và vai trò của các phương pháp hình thức trong việc bảo đảm chất lượng thiết kế. Tác giả luận giải nguyên nhân dẫn tới bài toán bùng nổ không gian trạng thái khi kiểm chứng hệ thống tích hợp và sự thiếu vắng các phương pháp tự động sinh đặc tả hình thức từ UML 2.0. Chương 1 làm rõ mục tiêu, đối tượng, phạm vi nghiên cứu, cấu trúc tổng thể của luận án và trình bày sơ đồ mối quan hệ tương hỗ giữa ba đóng góp cốt lõi (Hình 1.1).

Chương 2. Kiến thức nền tảng

Chương 2 trình bày có hệ thống các khái niệm toán học và mô hình hình thức phục vụ các chương tiếp theo, bao gồm:

• Định nghĩa chi tiết về LTS, kích thước của LTS $|M| = |Q|$, tính đơn định và không đơn định của hệ chuyển trạng thái;
• Khái niệm vết (trace), ngôn ngữ $L(M)$, phép chiếu vết $\sigma \uparrow \alpha M$;
• Thuật toán ghép nối song song hai LTS ($M_1 \parallel M_2$);
• Định nghĩa LTS an toàn, thuộc tính an toàn $p$, LTS lỗi $p_{err}$, và cơ chế phát hiện lỗi thông qua trạng thái $\pi$;
• Định nghĩa DFA, NFA, vết được đoán nhận, ngôn ngữ tiền tố đóng (prefix-closed);
• Kỹ thuật chuyển đổi từ DFA thu được qua thuật toán $L^*$ sang LTS bằng cách loại bỏ các trạng thái không kết thúc ($nas$ - non-accepting states);
• Cấu trúc biểu thức chính quy, các khối cơ bản, NNFA, MYNNFA, và biểu diễn ôtômát đuôi nén CNNFA với cấu trúc I-Forest và F-Forest;
• Định nghĩa ôtômát vào/ra hướng sự kiện;
• Khung lý thuyết kiểm chứng giả định - đảm bảo (AGV), định nghĩa giả định yếu nhất ($A_w$), và quy trình vận hành của công cụ LTSA với ngôn ngữ FSP.

Chương 3. Phương pháp sinh mô hình và kiểm chứng tính đúng đắn thiết kế cho các phần mềm dựa trên thành phần

Chương này đề xuất giải pháp tích hợp từ khâu sinh mô hình tới khâu kiểm chứng AGV:

• Quy trình phân tích biểu đồ tuần tự: Tệp XML đầu vào của biểu đồ tuần tự UML 2.0 được chuẩn hóa và phân tích cú pháp để tách thành hai cấu trúc dữ liệu: mảng các chu kỳ sống (Lifelines) và mảng các phân đoạn (Fragments) hoặc thông điệp (Messages) xếp theo thứ tự thời gian.
• Sinh biểu thức chính quy cho các phân đoạn tương tác của UML 2.0: Đề xuất quy tắc chuyển đổi cho từng loại phân đoạn: phân đoạn tùy chọn (Option), phân đoạn rẽ nhánh điều kiện (Alternative), vòng lặp (Loop), ngắt (Break), vùng tranh chấp găng (Critical), thực thi nghiêm ngặt (Strict), phân đoạn xử lý song song (Parallel), tuần tự (Sequencing), xem xét (Consider), và bỏ qua (Ignore). Biểu thức chính quy đại diện cho hành vi của từng thành phần được tổng hợp từ các phân đoạn này.
• Sinh mô hình bằng thuật toán CNNFA: Thay vì dùng thuật toán Thompson có chi phí lớn, luận án áp dụng thuật toán CNNFA để chuyển đổi biểu thức chính quy của từng thành phần thành ôtômát đuôi nén MYNNFA, sau đó khôi phục về NFA, chuyển sang DFA và tối thiểu hóa trạng thái trước khi chuyển thành LTS.
• Quy trình kiểm chứng AGV: Mô hình LTS của từng thành phần và LTS của thuộc tính an toàn được nạp vào quy trình AGV để kiểm chứng mà không cần ghép nối toàn cục.
• Thực nghiệm và công cụ: Tác giả xây dựng công cụ hỗ trợ và tiến hành thử nghiệm trên hệ thống Mod2 (gồm hai thành phần $M_1$ và $M_2$). Kết quả thực nghiệm cho thấy thời gian sinh mô hình và kích thước trạng thái trung gian theo phương pháp đề xuất giảm so với phương pháp sử dụng thuật toán Thompson và phương pháp dựa trên $L^*$ trong nghiên cứu của Inoue [43].

Chương 4. Phương pháp sinh mô hình và kiểm chứng tính đúng đắn của các biểu đồ tuần tự UML 2.0 sử dụng ôtômát vào/ra

Chương 4 tiếp cận bài toán kiểm chứng thiết kế theo hướng duy trì tính hướng đối tượng:

• Phân rã khối đơn: Biểu đồ tuần tự được phân tích và phân rã thành các khối đơn (Basic Blocks). Khối đơn có thể không chứa phân đoạn nào hoặc chỉ chứa duy nhất một loại phân đoạn tương tác UML 2.0.
• Thuật toán sinh luật chuyển cho ôtômát vào/ra: Đề xuất hệ thống các thuật toán xác định tập luật chuyển $\delta$ của ôtômát vào/ra hướng sự kiện cho từng đối tượng ứng với từng loại khối đơn: khối cơ bản (chỉ chứa gửi/nhận thông điệp thông thường), khối Option, khối Alternative, khối Loop, khối Break, khối Parallel, khối Strict, khối Critical, khối Consider, và khối Ignore.
• Xây dựng ôtômát vào/ra cho đối tượng: Kết hợp các luật chuyển từ các khối đơn để tạo thành ôtômát vào/ra hoàn chỉnh cho từng đối tượng tương ứng với đường đời (lifeline) trong biểu đồ tuần tự.
• Chuyển đổi sang đặc tả Promela: Thiết lập thuật toán ánh xạ các thành phần của ôtômát vào/ra sang cấu trúc tiến trình proctype, kênh truyền thông điệp chan, biến trạng thái và câu lệnh điều kiện của ngôn ngữ Promela.
• Kiểm chứng bằng SPIN: Tệp đặc tả Promela sinh ra được kết hợp với thuộc tính kiểm chứng viết bằng công thức logic thời gian tuyến tính LTL để nạp vào bộ công cụ SPIN. Thử nghiệm trên biểu đồ tuần tự của hệ thống đặt vé cho thấy phương pháp cho phép phát hiện lỗi thiết kế đối với các thuộc tính ngoài phạm vi thuộc tính an toàn (như liveness), khắc phục được hạn chế của phương pháp dùng EDTFA trong nghiên cứu của Zhao và cộng sự [90].

Chương 5. Một số cải tiến phương pháp kiểm chứng giả định - đảm bảo

Chương này tập trung nâng cao hiệu năng của thuật toán học $L^*$ trong kiểm chứng AGV thông qua hai cải tiến độc lập:

1. Cải tiến 1: Giảm truy vấn lặp lại và xử lý phản ví dụ tránh lặp vô hạn:

   • Xây dựng cấu trúc từ điển (Dictionary) để lưu trữ mọi cặp kết quả (vết, kết quả truy vấn) đã thực hiện trong quá trình hỏi truy vấn thành viên (MQ). Learner kiểm tra từ điển trước khi gửi truy vấn đến Teacher, loại bỏ hoàn toàn các truy vấn lặp lại đối với các hành động trùng lặp.
   • Giải quyết bài toán lặp vô hạn khi phân tích phản ví dụ (counterexample - $cex$): Phương pháp truyền thống trong Cobleigh [25] chỉ chọn hành động cuối cùng của $cex$ làm hậu tố (suffix) thêm vào tập $E$ của bảng quan sát, dẫn đến nguy cơ bảng không đóng và vòng lặp học không dừng. Cải tiến của tác giả kiểm tra tuần tự các hậu tố có chiều dài từ 1 đến $|cex|$; hậu tố đầu tiên làm cho bảng quan sát không đóng sẽ được chọn để bổ sung vào $E$.

2. Cải tiến 2: Phương pháp sinh giả định nhỏ nhất cục bộ (Local Strongest Assumption):

   • Trong ngữ cảnh phần mềm tiến hóa, một giả định có ngôn ngữ nhỏ hơn (giả định mạnh hơn) sẽ giúp giảm không gian tìm kiếm khi phải tái kiểm chứng hệ thống sau khi các thành phần bị thay đổi.
   • Ý tưởng giải thuật: Xuất phát từ giả thiết ban đầu là ngôn ngữ của giả định $L(A) = \emptyset$. Thuật toán sử dụng phương pháp tìm kiếm theo chiều rộng (BFS) trên không gian các vết được trích xuất từ giả định yếu nhất $A_w$, thêm dần từng vết vào ngôn ngữ cho đến khi tìm được ứng viên giả định $A_s$ đầu tiên thỏa mãn hai luật của AGV. Giả định $A_s$ tạo ra bảo đảm $L(A_s) \subseteq L(A_{org})$, trong đó $A_{org}$ là giả định sinh bởi phương pháp gốc của Cobleigh [25].
   • Kết quả thực nghiệm kiểm chứng bằng công cụ LTSA khẳng định hệ thống $IS_{STRONGEST} = A_s \parallel A_{org}$ không vi phạm tiến trình (No progress violations detected), xác thực tính bao hàm ngôn ngữ $L(A_s) \subseteq L(A_{org})$.

Dữ liệu thực nghiệm của Chương 5: Thực nghiệm so sánh hiệu năng được thực hiện trên công cụ IAGTool cài đặt trên máy tính có cấu hình nêu tại Bảng 5.4:

Thông số phần cứng / phần mềm	Giá trị chi tiết
Bộ vi xử lý (Processor)	Intel(R) Core(TM) i5-3230M CPU @ 2.60GHz (2 lõi, 4 luồng logic)
Bộ nhớ vật lý (Physical Memory)	5.88 GB RAM
Hệ điều hành (OS Name)	Microsoft Windows 10 Home
Môi trường phát triển (IDE)	Microsoft Visual Studio Community 2015

Kết quả so sánh giữa phương pháp gốc trong Cobleigh [25] và phương pháp đề xuất sinh giả định nhỏ nhất cục bộ (LSAG) được tổng hợp tại Bảng 5.5:

| Ca thử nghiệm | $|M_1|$ | $|M_2|$ | $|p|$ | Giả định mạnh hơn | MQ gốc [25] | EQ gốc [25] | Thời gian gốc (ms) | MQ đề xuất (LSAG) | EQ đề xuất (LSAG) | Thời gian đề xuất (ms) | | :--- | :---: | :---: | :---: | :---: | :---: | :---: | :---: | :---: | :---: | :---: | :---: | | TestCase1 | 3 | 3 | 2 | no | 49 | 4 | 15 | 49 | 15 | 87 | | TestCase2 | 5 | 4 | 2 | yes | 38 | 3 | 9 | 38 | 17 | 43 | | TestCase3 | 4 | 4 | 2 | yes | 73 | 4 | 21 | 38 | 12 | 35 |

Số liệu thực nghiệm cho thấy tại TestCase2 và TestCase3, phương pháp đề xuất đã sinh ra được các giả định có ngôn ngữ nhỏ hơn giả định gốc của Cobleigh [25] (xác nhận "yes" tại cột stronger). Để đạt được giả định mạnh hơn, số lượng truy vấn ứng viên (EQ) và thời gian thực thi có thể tăng lên (như ở TestCase1 và TestCase2), nhưng số lượng truy vấn thành viên (MQ) ở TestCase3 giảm từ 73 xuống còn 38.

Chương 6. Kết luận

Chương cuối cùng tổng kết toàn bộ ba kết quả chính đã đạt được, đồng thời trình bày các hạn chế còn tồn tại và xác định các hướng nghiên cứu mở rộng trong tương lai.

Kết quả và những đóng góp mới

Luận án đã tự công bố ba đóng góp khoa học chính về mặt lý thuyết và thực tiễn:

1. Đóng góp thứ nhất: Xây dựng phương pháp hoàn chỉnh tự động sinh mô hình và kiểm chứng từng phần cho thiết kế phần mềm đặc tả bằng biểu đồ tuần tự UML 2.0. Đóng góp cụ thể gồm thuật toán phân tích và chuyển đổi đầy đủ các phân đoạn tương tác UML 2.0 sang biểu thức chính quy, ứng dụng biểu diễn ôtômát đuôi nén CNNFA để sinh mô hình LTS của từng thành phần phần mềm với chi phí bộ nhớ và thời gian tối ưu, tích hợp với bộ công cụ LTSA để kiểm chứng các thuộc tính an toàn qua cơ chế giả định - đảm bảo mà không cần ghép nối toàn cục.
2. Đóng góp thứ hai: Đề xuất phương pháp sinh mô hình ôtômát vào/ra hướng sự kiện từ các khối đơn của biểu đồ tuần tự UML 2.0, bảo toàn tính tương tác hướng đối tượng của thiết kế. Đề xuất quy tắc chuyển đổi tự động từ ôtômát vào/ra sang ngôn ngữ Promela để kiểm chứng bằng bộ công cụ SPIN, mở rộng phạm vi kiểm chứng sang các thuộc tính LTL (như thuộc tính liveness, fairness) thay vì chỉ giới hạn ở thuộc tính an toàn.
3. Đóng góp thứ ba: Đưa ra hai giải pháp cải tiến cho phương pháp kiểm chứng giả định - đảm bảo dùng thuật toán học $L^*$:
   • Giải pháp giảm số truy vấn thành viên bằng kỹ thuật lưu trữ từ điển (Dictionary) và thuật toán chọn hậu tố theo độ dài tăng dần từ phản ví dụ $cex$, khắc phục triệt để hiện tượng lặp vô hạn của thuật toán $L^*$ truyền thống;
   • Thuật toán sinh giả định có ngôn ngữ nhỏ nhất cục bộ (local minimal assumption) dựa trên tìm kiếm theo chiều rộng từ giả định yếu nhất $A_w$, giúp tạo ra các giả định có hành vi chặt chẽ hơn, phục vụ hiệu quả cho việc tái kiểm chứng khi thành phần phần mềm bị thay đổi trong bối cảnh tiến hóa.

Kiến nghị và giải pháp kỹ thuật đề xuất: Luận án kiến nghị áp dụng quy trình kiểm chứng tách rời khâu sinh mô hình và kiểm chứng mô hình trong các công đoạn thiết kế phần mềm yêu cầu độ tin cậy cao; tích hợp công cụ IAGTool vào quy trình phát triển thực tế để giảm chi phí kiểm thử lại.

Hạn chế và hướng nghiên cứu tiếp

Dựa trên các nội dung văn bản luận án thừa nhận, công trình còn một số hạn chế kỹ thuật:

• Phương pháp kiểm chứng giả định - đảm bảo ở Chương 3 và Chương 5 hiện chỉ mới áp dụng cho các thuộc tính an toàn (safety properties), chưa kiểm chứng được các thuộc tính như tính sống (liveness) và tính công bằng (fairness).
• Phạm vi thiết kế mới chỉ khai thác thông tin từ biểu đồ tuần tự UML 2.0, chưa kết hợp với các dạng biểu đồ UML khác (như sơ đồ lớp - class diagram, sơ đồ trạng thái - statechart diagram) để mô tả toàn diện hành vi hệ thống.
• Các mô hình thực nghiệm của kiểm chứng giả định - đảm bảo chủ yếu giải quyết cho các hệ thống gồm hai thành phần; việc phân tách và sinh giả định cho các hệ thống có nhiều hơn hai thành phần còn gặp khó khăn do độ phức tạp cao.
• Thuật toán sinh giả định mới chỉ dừng lại ở việc tạo ra giả định nhỏ nhất cục bộ chứ chưa sinh được giả định nhỏ nhất toàn cục; phần chứng minh toán học hình thức về tính đầy đủ và tính đúng đắn tổng quát của thuật toán này vẫn đang trong quá trình hoàn thiện.
• Các công cụ hỗ trợ chưa có giao diện đồ họa người dùng trực quan hoàn chỉnh để chuyển giao vào quy trình sản xuất phần mềm công nghiệp.

Các hướng nghiên cứu tiếp theo được tác giả xác định:

1. Mở rộng kiểm chứng giả định - đảm bảo cho các thuộc tính liveness và fairness;
2. Nghiên cứu mở rộng phương pháp cho các hệ thống chứa nhiều hơn hai thành phần và nghiên cứu thuật toán phân tách hệ thống tối ưu;
3. Tích hợp thêm các loại biểu đồ UML khác (sơ đồ lớp, sơ đồ máy trạng thái) và tích hợp các ôtômát có yếu tố thời gian (timed automata) để áp dụng cho hệ thống thời gian thực và hệ thống phần cứng;
4. Kết hợp kết quả của luận án với các phương pháp kiểm chứng phần mềm hồi quy trong ngữ cảnh tiến hóa phần mềm;
5. Hoàn thiện chứng minh lý thuyết và xây dựng giao diện đồ họa cho bộ công cụ để thử nghiệm trên các hệ thống công nghiệp quy mô lớn.

Giá trị tham khảo

Luận án là tài liệu tham khảo chuyên khảo hữu ích cho các nhóm đối tượng:

• Nghiên cứu sinh và học viên cao học chuyên ngành Kỹ thuật phần mềm và Khoa học máy tính: Cung cấp cơ sở lý thuyết chuẩn xác và chi tiết về lý thuyết ôtômát (CNNFA, I/O automata, LTS), kỹ thuật kiểm chứng mô hình, thuật toán học máy $L^*$ của Angluin, và cơ chế giả định - đảm bảo (AGV).
• Giảng viên giảng dạy các học phần Phương pháp hình thức (Formal Methods), Đảm bảo chất lượng phần mềm, Thiết kế phần mềm nâng cao: Có thể sử dụng các thuật toán chuyển đổi biểu đồ tuần tự sang biểu thức chính quy và ôtômát (Chương 3 và Chương 4) làm học liệu giảng dạy và bài tập thực hành.
• Kỹ sư thiết kế và chuyên gia kiểm thử hệ thống phần mềm nhúng, an toàn cao: Có thể tham khảo phương pháp ánh xạ từ ôtômát vào/ra sang Promela/SPIN để tự động hóa việc thẩm tra các đặc tả thiết kế UML trước khi bước vào giai đoạn viết mã nguồn.

Phần đáng tham khảo nhất trong luận án là Chương 3 (với các thuật toán chuyển đổi phân đoạn UML 2.0 sang biểu thức chính quy) và Chương 5 (với thuật toán phân tích hậu tố phản ví dụ và kỹ thuật sinh giả định nhỏ nhất cục bộ).

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

Câu hỏi 1: Vì sao luận án lựa chọn thuật toán CNNFA thay vì thuật toán Thompson truyền thống để sinh mô hình LTS từ biểu thức chính quy?
Trả lời: Thuật toán Thompson truyền thống sinh ra ôtômát chứa nhiều chuyển dời rỗng ($\epsilon$-transitions) và có kích thước trạng thái trung gian lớn, đòi hỏi chi phí tính toán cao để khử không đơn định. Thuật toán CNNFA (Compressed NNFA) của Chang và Paige sử dụng cấu trúc rừng cây nhị phân I-Forest và F-Forest kết hợp danh sách liên kết đôi, cho phép thực hiện phép hợp các tập trạng thái không giao nhau trong thời gian $O(1)$, từ đó giảm đáng kể số trạng thái trung gian và thời gian chuyển đổi từ biểu thức chính quy sang ôtômát.

Câu hỏi 2: Sự khác nhau cơ bản giữa cách tiếp cận kiểm chứng ở Chương 3 và Chương 4 là gì?
Trả lời: Ở Chương 3, luận án chuyển đổi biểu đồ tuần tự thành mô hình LTS, tích hợp với kỹ thuật giả định - đảm bảo (AGV) và công cụ LTSA; hướng tiếp cận này tập trung giải quyết bài toán bùng nổ không gian trạng thái nhưng chỉ hỗ trợ kiểm chứng thuộc tính an toàn (safety properties). Ở Chương 4, luận án chuyển đổi biểu đồ tuần tự thành các ôtômát vào/ra hướng sự kiện (giữ nguyên tính hướng đối tượng), sau đó ánh xạ sang mã nguồn Promela và kiểm chứng bằng công cụ SPIN; hướng tiếp cận này hỗ trợ kiểm chứng tập thuộc tính phong phú hơn biểu diễn qua công thức LTL (bao gồm cả thuộc tính liveness).

Câu hỏi 3: Thuật toán cải tiến ở Chương 5 khắc phục hiện tượng lặp vô hạn của thuật toán $L^$ như thế nào?*
Trả lời: Phương pháp truyền thống của Cobleigh chỉ lấy hành động cuối cùng của phản ví dụ $cex$ để làm hậu tố thêm vào tập $E$ của bảng quan sát $OT$, dẫn tới trường hợp bảng quan sát không thể đóng và vòng lặp tiếp tục vô hạn. Cải tiến của tác giả kiểm tra lần lượt các hậu tố có chiều dài tăng dần từ 1 cho tới độ dài của $cex$; hậu tố đầu tiên làm cho bảng quan sát không đóng sẽ được chọn để bổ sung vào tập $E$, bảo đảm quá trình học của $L^*$ tìm được trạng thái phân tách hợp lệ và kết thúc.

Câu hỏi 4: Khái niệm "giả định nhỏ nhất cục bộ" (local minimal assumption) mang lại lợi ích gì trong bối cảnh phần mềm tiến hóa?
Trả lời: Giả định nhỏ nhất cục bộ $A_s$ có ngôn ngữ nhỏ hơn giả định sinh bởi phương pháp gốc ($L(A_s) \subseteq L(A_{org})$), đồng nghĩa với việc hành vi của giả định chặt chẽ hơn. Khi một thành phần trong hệ thống bị tiến hóa hoặc thay đổi, việc kiểm chứng lại tính đúng đắn của toàn hệ thống bằng cách sử dụng giả định mạnh hơn sẽ thu hẹp không gian tìm kiếm trạng thái, từ đó giảm chi phí tính toán và số lượng truy vấn khi kiểm chứng lại.

Câu hỏi 5: Dữ liệu thực nghiệm của luận án đã kiểm chứng trên những hệ thống cụ thể nào?
Trả lời: Luận án đã tiến hành thực nghiệm trên hệ thống phần cứng/phần mềm Mod2 (đánh giá sinh biểu thức chính quy và kiểm chứng AGV ở Chương 3), hệ thống phần mềm đặt vé (Ticket Reservation System - đánh giá sinh ôtômát vào/ra và kiểm chứng Promela/SPIN ở Chương 4), và ba bộ ca kiểm thử mô hình tổng hợp TestCase1, TestCase2, TestCase3 trên công cụ IAGTool (đánh giá số lượng truy vấn MQ, EQ và thời gian sinh giả định ở Chương 5).

Kết luận

Luận án tiến sĩ của Lê Chí Luận đã giải quyết trọn vẹn bài toán tự động sinh mô hình đặc tả hình thức từ tài liệu thiết kế biểu đồ tuần tự UML 2.0 và kiểm chứng tính đúng đắn cho các phần mềm dựa trên thành phần. Tác giả đã kết hợp hài hòa giữa mô hình hóa LTS với kỹ thuật kiểm chứng giả định - đảm bảo, đồng thời phát triển song song hướng tiếp cận dùng ôtômát vào/ra kết hợp công cụ SPIN để mở rộng phạm vi thuộc tính kiểm chứng. Hai đóng góp cải tiến thuật toán học $L^*$ không chỉ xử lý được điểm nghẽn lặp vô hạn mà còn cung cấp cơ chế sinh giả định nhỏ nhất cục bộ, tạo tiền đề kỹ thuật quan trọng cho việc kiểm chứng mô hình trong bối cảnh phần mềm tiến hóa.

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

Chương 1 GIỚI THIỆU 1. Đặt vẫn đề Phát triển phần mềm dựa trên công nghệ hướng thành phần (Component- based Software Development - CBSD) đang được quan tâm như là cách tiếp cận chủ yếu để xây dựng các phần mềm hiện nay. Phần mềm dựa trên thành phần được xây dựng bằng cách ghép nối các thành phần đã có sẵn. Các thành phần này hoặc do công ty tự phát triển trước đó hoặc được cung cấp bởi bên thứ ba.

Với cách tiếp cận này, chúng ta có thể giảm đáng kể chi phí và thời gian phat triển trong khi vẫn đảm bảo được chất lượng của phần mềm. Tuy nhiên, một trong những hạn chế lớn nhất của công nghệ hướng thành phần là làm thế nào để đảm bảo rằng các thành phần sau khi ghép nối với nhau có thể cộng tác để đạt được mục tiêu của hệ thống - việc đảm bao cơ chế “plug-and-play”. Dac biệt, đối với những ứng dụng yêu cầu chất lượng cao như các hệ thống điều khiển tên lửa, máy bay, an ninh quốc phòng, v. thì việc dam bảo tính đúng đắn của thiết kế trước khi thực hiện các pha tiếp theo là bắt buộc.

Hiện tại, các công nghệ hỗ trợ phát triển hướng thành phần chỉ cho phép kiểm tra khả năng ghép nối giữa các thành phần chứ không có cơ chế đảm bảo tính cộng tác của chúng. Kết quả, các sản phẩm phần mềm hiện nay có chất lượng thấp, không đáp ứng yêu cầu. Để giải quyết các nhược điểm của CBSD, hiện nay cùng với chứng minh định lý (theorem proving) [36], kiểm chứng mô hình (model checking) [23, 73] được biết đến như một giải pháp phổ biến để giải quyết vấn đề này. Để áp dụng các phương pháp kiểm chứng mô hình, ta cần phải xây dựng các mô hình đặc tả hành vi của hệ thống cần kiểm chứng [27, 26, 88].

Những mô hình này thường được biểu diễn bằng các máy hữu hạn trạng thái đơn định. Các nghiên cứu hiện tai hầu hết giả sử các mô hình này đã có và đúng đắn [54, 52, 51]. Tuy nhiên, giả thiết này rất khó đáp ứng trong thực tế vì việc xây dựng mô hình cho các phần mềm là một công việc khó khăn và tiềm an nhiều lỗi. Trong thực tế, các thiết kế biểu diễn bằng UML 2.0 rất phổ biến ở các công ty.

Nếu như chúng ta có cơ chế chuyển đổi dang đặc tả UML 2.0 sang các máy hữu hạn trạng thái đơn định thì khả năng ứng dụng sẽ tốt hơn. Làm thế nào để kiểm chứng tính đúng đắn của biểu đồ tuần tự nói riêng và các thiết kế nói chung là vấn đề mở và chưa có lời giải thỏa đáng. Giả sử chúng ta đã có các mô hình của các thành phần mô tả chính xác hành vi của chúng. Để áp dụng các phương pháp kiểm chứng mô hình, chúng ta phải chép nối các mô hình này để thu được một mô hình ghép nối duy nhất của hệ thống.

Mô hình sau khi được ghép nối kết hợp với đặc tả thuộc tính cần kiểm tra là dữ liệu vào đối với các công cụ kiểm chứng. Tuy nhiên, số lượng trạng thái của mô hình ghép nối thường rất lớn nên vấn đề bùng nổ không gian trạng thái có thể xảy ra khi kiểm chứng các phần mềm có kích thước lớn. Khó khăn trong việc xây dựng mô hình và vấn đề bùng nổ không gian trạng thái được xem là nguyên nhân chủ yếu cho việc khó áp dụng các phương pháp kiểm chứng mô hình trong thực tế. Kiểm chứng từng phần (modular verification) [30, 62, 65] là giải pháp hứa hẹn nhằm xử lý sự bùng nổ không gian trạng thái đối với kiểm chứng mô hình.

Trong cách tiếp cận này, thay vì kiểm chứng trên toàn bộ mô hình ghép nối, chúng ta chỉ cần kiểm chứng trên từng mô hình của mỗi thành phần riêng biệt. Khi tất cả các thành phần đã được kiểm chứng, chúng ta có thể kết luận phần mềm thỏa mãn thuộc tính cần kiểm chứng mà không cần ghép nối các mô hình của các thành phần với nhau. Kiểm chứng giả định - đảm bảo (Assume — Guarentee Verification) [25, 33] và sau đó được cải tiến trong [52| là hiện thực hóa của tư tưởng kiểm chứng từng phần. Trong phương pháp này, để kiểm chứng các hệ thống con một cách riêng biệt, chúng ta cần các giả định (assumptions) về môi trường mà mỗi hệ thống con sẽ được thực hiện ứng với thuộc tính cần kiểm chứng [24].

Tuy nhiên, độ phức tap của việc sinh giả định còn cao. Hơn nữa, các phương pháp này chỉ mới giải quyết được các hệ thống đơn giản gồm hai thành phần. Các phần mềm thực tế thường có nhiều hơn hai thành phần và ý tưởng của các phương pháp này khó tổng quát hóa cho trường hợp này. Mặc dù đã có nhiều nghiên cứu quan tâm giải quyết vấn đề đặc tả và kiểm chứng tính đúng đắn của thiết kế phần mềm dựa trên thành phần, các vấn đề sau vẫn còn là các bài toán mở và chưa có giải pháp thỏa đáng.

e Chưa có giải pháp để xây dựng mô hình đặc tả hình thức hành vi của từng thành phần phần mềm nói riêng và hệ thống dựa trên thành phần nói chung. Cần đề xuất một giải pháp đầy đủ từ đầu đến cuối cho bài toán kiểm chứng mô hình phần mềm dựa trên thành phần, từ bước sinh đặc tả hình thức đến áp dụng công cụ kiểm chứng để nhận được kết quả về tính đúng đắn của thiết kế. Mặc dù đã có nhiều phương pháp và công cụ kiểm chứng mô hình phần mềm khác nhau với yêu cầu đầu vào là các đặc tả hình thức phù hợp tương ứng, bản thân việc sinh các đặc tả hình thức đúng đắn, tiêu chuẩn hóa, từ các tài liệu thiết kế phần mềm là một thách thức cần giải quyết. Hạn chế này là nguyên nhân chính dẫn đến việc khó áp dụng các phương pháp kiểm chứng mô hình trong thực tế.

e Biểu đồ tuần tự UML là một tài liệu thiết kế phần mềm tiêu chuẩn. Đã có các nghiên cứu về kiểm chứng tính đúng đắn của biểu đồ tuần tự UML, nhưng không tách biệt quá trình sinh mô hình với bước kiểm chứng mô hình. Việc tự động sinh mô hình từ biểu đồ tuần tự UML và cho phép sự dụng lại mô hình một cách hợp lý là rất cần thiết. e Với sự tăng nhanh về kích thước cũng như sự phức tạp của phần mềm, việc kiểm chứng và đảm bảo tính đúng đắn của phần mềm ngày càng trở nên quan trọng và ngày càng khó khăn hơn do các phần mềm ngày càng phức tạp.

Hiện tại, chưa có một giải pháp đủ tốt để giải quyết vấn đề này. e Chưa có một công cụ đủ tốt tích hợp các giải pháp trên trong một công cụ kiểm chứng nhằm tự động hóa quá trình đặc tả và kiểm chứng cho thành phần phần mềm dựa trên biểu đồ tuần tự. Mục tiêu của luận án để giải quyết các vấn đề nêu trên. Kiểm chứng mô hình cho phần mềm dựa trên thành phần là một giải pháp đảm bảo chất lượng phần mềm ngay từ bước thiết kế.

Thách thức của kiểm chứng mô hình là cần có các đặc tả hình thức tiêu chuẩn, đúng đắn và công cụ phù hợp. Đã có nhiều nghiên cứu về phương pháp kiểm chứng mô hình phần mềm và một số bộ công cụ kiểm chứng khác nhau đã được phát triển. Để áp dụng kiểm chứng mô hình trong thực tiễn, cần lựa chọn giải pháp, sinh mô hình đặc tả đúng, phù hợp với phương pháp kiểm chứng và yêu cầu của bộ công cụ kiểm chứng được lựa chọn. Một cách lý tưởng, phương pháp đề xuất cần xây dựng mô hình cho mỗi thành phần phần mềm bằng cách phân tích tất cả các biểu đồ UML đặc tả các khung nhìn khác nhau về thành phần này.

Tuy nhiên, do hạn chế về thời gian nên phạm vi nghiên cứu của luận án này là các thiết kế của các thành phần phần mềm được biểu diễn dưới dang các biểu đồ tuần tự UML bởi đây là biểu đồ có hành vi chi tiết nhất trong các biểu đồ UML, một loại tài liệu thiết kế phần mềm phổ biến và nghiên cứu xuyên suốt quy trình, đề xuất giải quyết các khó khăn thách thức gặp phải, hoàn thiện thuật toán nâng cao tính hiệu quả khi áp dụng thực tiễn để có thể nhận được kết quả kiểm chứng cuối cùng. Mục tiêu của luận án là đề xuất một số phương pháp hỗ trợ sinh tự động mô hình đặc tả hành vi của thiết kế phần mềm dưới dạng biểu đồ tuần tự UML và kết hợp phương pháp kiểm chứng giả định - đảm bảo kiểm chứng tính đúng đắn của các thiết kế này một cách hiệu quả. Mặt khác, luận án đề xuất phương pháp sinh mô hình và kiểm chứng tính đúng đắn của các biểu đồ tuần tự UML sử dụng ôtômát vào/ra và công cụ kiểm chứng SPIN. Để giải quyết một số hạn chế trong kiểm chứng giả định - đảm bảo, luận án đề xuất một phương pháp để tạo ra các giả định nhỏ nhất cục bộ cho phương pháp kiểm chứng giả định - đảm bảo và hai cải tiến nhằm giảm độ phức tạp trong việc sinh giả định.

Luận án hướng đến một giải pháp đầy đủ cho việc kiểm chứng tính đúng đắn của các thiết kế có khả năng ứng dụng trong thực tế. Đối tượng nghiên cứu của luận án là thiết kế của các hệ thống phần mềm dựa trên thành phần. Các phần mềm này được phát triển bằng cách ghép nối các thành phần sẵn có với chất lượng cao. Đây là giải pháp phổ biến nhất hiện nay để phát triển các ứng dụng vì nó giảm thiểu thời gian cũng như chi phí phát triển trong khi vẫn đảm bảo được chất lượng phần mềm.

Tuy nhiên, chúng ta chưa có cơ chế đảm bảo tính cộng tác giữa các thành phần. Hệ quả là các thành phần không thể cộng tác được với nhau sau khi được ghép nối. Một cách lý tưởng, phương pháp đề xuất cần xây dựng mô hình cho mỗi thành phần phần mềm bằng cách phân tích tất cả các biểu đồ UML đặc tả các khung nhìn khác nhau về thành phần này. Tuy nhiên, do hạn chế về thời gian nên phạm vi nghiên cứu của luận án này là các thiết kế của các thành phần phần mềm được biểu diễn dưới dạng các biểu đồ tuần tự UML 2.0 bởi đây là biểu đồ có hành vi chỉ tiết nhất trong các biểu đồ UML.

Để đạt được mục tiêu nghiên cứu, luận án sẽ tiến hành khảo sát các giải pháp đã có. Từ đó, luận án sẽ xác định các hạn ché/van đề chưa giải quyết được và đề xuất phương pháp mới hoặc cải tiến các phương pháp hiện có.