Luận văn thạc sĩ về kỹ thuật sinh ca kiểm thử từ mô hình máy hữu hạn trạng thái

• Tác giả: Đoàn Thị Thùy Linh
• 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: Nghiên Cứu Kỹ Thuật Sinh Ca Kiểm Thử Từ Mô Hình Máy Hữu Hạn
• Loại tài liệu: Luận Văn Thạc Sĩ
• Năm xuất bản: 2012
• Địa điểm: Hà Nội

• LỜI MỞ ĐẦU
• 1. CHƯƠNG 1: ĐẶT VẤN ĐỀ
• 2. CHƯƠNG 2: MÁY HỮU HẠN TRẠNG THÁI (FSM)
• 2.1. Định nghĩa FSM
• 2.2. Biểu diễn FSM
• 2.2.1. Biểu diễn kiểu liệt kê
• 2.2.2. Biểu diễn bằng đồ thị
• 2.2.3. Biểu diễn bằng dạng bảng
• 2.3. Một số tính chất của FSM
• 2.3.1. Được đặc tả đầy đủ (Completely specified)
• 2.3.2. Đơn định (Deterministic)
• 2.3.3. Liên thông mạnh (Strongly connected)
• 2.3.4. Tối giản
• 3. CHƯƠNG 3: MỘT SỐ PHƯƠNG PHÁP XÁC ĐỊNH CHUỖI KIỂM CHỨNG TRẠNG THÁI
• 3.1. Chuỗi vào – ra duy nhất (Unique Input - Output sequence)
• 3.2. Một số khái niệm
• 3.3. Thuật toán sinh cây UIO
• 4. CHƯƠNG 4: KIỂM THỬ DỰA TRÊN MÔ HÌNH FSM
• 5. CHƯƠNG 5: KỸ THUẬT SINH CA KIỂM THỬ
• 6. CHƯƠNG 6: KẾT LUẬN
• TÀI LIỆU THAM KHẢO

I. Giới thiệu về kỹ thuật sinh ca kiểm thử

Kỹ thuật sinh ca kiểm thử từ mô hình máy hữu hạn (FSM) là một phương pháp quan trọng trong lĩnh vực kiểm thử phần mềm. Kỹ thuật kiểm thử này cho phép xác định các ca kiểm thử dựa trên các trạng thái và chuyển trạng thái của FSM. Mô hình FSM được sử dụng rộng rãi trong các hệ thống phần mềm, đặc biệt là trong các hệ thống điều khiển và giao thức truyền thông. Việc áp dụng kỹ thuật sinh ca kiểm thử giúp đảm bảo rằng các hệ thống này hoạt động chính xác theo các đặc tả đã được định nghĩa. Một trong những điểm mạnh của phương pháp này là khả năng phát hiện lỗi trong quá trình cài đặt, từ đó nâng cao chất lượng phần mềm. Theo nghiên cứu, việc sử dụng FSM trong kiểm thử không chỉ giúp tiết kiệm thời gian mà còn tăng cường độ tin cậy của sản phẩm phần mềm.

1.1. Định nghĩa mô hình máy hữu hạn

Mô hình máy hữu hạn (FSM) là một cấu trúc lý thuyết được sử dụng để mô tả hành vi của hệ thống. FSM bao gồm một tập hợp các trạng thái, một tập hợp các đầu vào và một tập hợp các đầu ra. Mỗi trạng thái có thể chuyển sang trạng thái khác dựa trên đầu vào nhận được. Mô hình hóa FSM cho phép các nhà phát triển dễ dàng hình dung và phân tích hành vi của hệ thống. Việc hiểu rõ về FSM là rất cần thiết để áp dụng kỹ thuật kiểm thử phần mềm hiệu quả. Các loại FSM phổ biến bao gồm máy Mealy và máy Moore, mỗi loại có cách thức hoạt động và ứng dụng riêng. Sự khác biệt giữa chúng nằm ở cách mà đầu ra được sinh ra, từ đó ảnh hưởng đến cách thức kiểm thử được thực hiện.

II. Các phương pháp xác định chuỗi kiểm chứng trạng thái

Trong kiểm thử dựa trên mô hình FSM, việc xác định chuỗi kiểm chứng trạng thái là rất quan trọng. Có ba loại chuỗi chính được sử dụng: chuỗi vào – ra duy nhất (UIO), chuỗi phân biệt (DS) và chuỗi đặc trưng (W). Mỗi loại chuỗi có vai trò riêng trong việc phân biệt các trạng thái của FSM. Chuỗi vào – ra duy nhất là chuỗi mà cho mỗi trạng thái, đầu ra sẽ khác nhau khi đầu vào là giống nhau. Điều này giúp xác định rõ ràng trạng thái hiện tại của FSM. Chuỗi phân biệt cho phép phân biệt giữa các trạng thái khác nhau thông qua các đầu vào cụ thể. Cuối cùng, chuỗi đặc trưng là một tập hợp các chuỗi có thể được sử dụng để xác định các đặc tính của FSM. Việc áp dụng các phương pháp này không chỉ giúp phát hiện lỗi mà còn tối ưu hóa quy trình kiểm thử.

2.1. Chuỗi vào ra duy nhất UIO

Chuỗi vào – ra duy nhất (UIO) là một khái niệm quan trọng trong việc kiểm thử FSM. Một chuỗi được gọi là UIO nếu nó có thể phân biệt một trạng thái với tất cả các trạng thái khác trong FSM. Để xác định UIO, cần phải phân tích các đầu vào và đầu ra của FSM. Việc tìm kiếm UIO giúp xác định các trạng thái mà không thể bị nhầm lẫn với nhau, từ đó tạo ra các ca kiểm thử hiệu quả. Quá trình này thường được thực hiện thông qua việc xây dựng cây UIO, nơi mỗi nhánh đại diện cho một chuỗi đầu vào cụ thể. Kết quả cuối cùng là một tập hợp các chuỗi UIO cho từng trạng thái, giúp đảm bảo rằng tất cả các trạng thái đều được kiểm thử một cách đầy đủ.

III. Kiểm thử dựa trên mô hình FSM

Kiểm thử dựa trên mô hình FSM là một phương pháp mạnh mẽ để đảm bảo rằng các hệ thống phần mềm hoạt động đúng theo các đặc tả. Phương pháp này không chỉ giúp phát hiện lỗi mà còn cung cấp cái nhìn sâu sắc về hành vi của hệ thống. Việc kiểm thử dựa trên mô hình cho phép các nhà phát triển xác định các lỗi thường gặp trong quá trình cài đặt FSM. Các lỗi này có thể bao gồm các vấn đề liên quan đến chuyển trạng thái không chính xác hoặc đầu ra không đúng. Bằng cách sử dụng các chuỗi kiểm chứng trạng thái, các nhà phát triển có thể dễ dàng xác định và sửa chữa các lỗi này. Điều này không chỉ giúp nâng cao chất lượng phần mềm mà còn tiết kiệm thời gian và chi phí trong quá trình phát triển.

3.1. Mối quan hệ mô phỏng của hai FSM

Mối quan hệ mô phỏng giữa hai FSM là một yếu tố quan trọng trong việc kiểm thử. Khi một FSM mô phỏng chính xác hành vi của một FSM khác, điều này có nghĩa là chúng có thể được coi là tương đương trong ngữ cảnh kiểm thử. Việc xác định mối quan hệ này giúp đảm bảo rằng các hệ thống được phát triển đáp ứng đúng các yêu cầu và đặc tả ban đầu. Các phương pháp kiểm thử dựa trên mô hình cho phép các nhà phát triển kiểm tra tính chính xác của mô phỏng này thông qua việc sử dụng các chuỗi kiểm chứng trạng thái. Nếu một FSM không mô phỏng chính xác FSM khác, các lỗi sẽ được phát hiện và sửa chữa kịp thời.

IV. Kỹ thuật sinh ca kiểm thử

Kỹ thuật sinh ca kiểm thử từ mô hình máy hữu hạn là một phần quan trọng trong quy trình kiểm thử phần mềm. Kỹ thuật này tập trung vào việc xác định các ca kiểm thử dựa trên các trạng thái và chuyển trạng thái của FSM. Độ bao phủ của mô hình máy hữu hạn trạng thái là một yếu tố quan trọng trong việc đảm bảo rằng tất cả các khía cạnh của hệ thống đều được kiểm thử. Việc lựa chọn độ bao phủ tốt nhất giúp tối ưu hóa quy trình kiểm thử và giảm thiểu rủi ro. Kỹ thuật sinh ca kiểm thử không chỉ giúp phát hiện lỗi mà còn cung cấp cái nhìn tổng quan về hành vi của hệ thống. Các phương pháp sinh ca kiểm thử thường được áp dụng trong các dự án phát triển phần mềm để đảm bảo rằng sản phẩm cuối cùng đáp ứng đúng các yêu cầu và tiêu chuẩn chất lượng.

4.1. Độ bao phủ mô hình máy hữu hạn trạng thái

Độ bao phủ mô hình máy hữu hạn trạng thái là một khái niệm quan trọng trong kiểm thử phần mềm. Độ bao phủ này đề cập đến mức độ mà các trạng thái và chuyển trạng thái của FSM được kiểm thử. Việc đạt được độ bao phủ cao giúp đảm bảo rằng tất cả các khía cạnh của hệ thống đều được kiểm tra, từ đó phát hiện lỗi một cách hiệu quả. Có nhiều phương pháp để đo lường độ bao phủ, bao gồm độ bao phủ trạng thái và độ bao phủ chuyển trạng thái. Mỗi phương pháp có ưu điểm và nhược điểm riêng, và việc lựa chọn phương pháp phù hợp là rất quan trọng để tối ưu hóa quy trình kiểm thử.

Tổng quan nghiên cứu

Máy hữu hạn trạng thái (Finite State Machine - FSM) là mô hình hành vi quan trọng trong lĩnh vực công nghệ phần mềm, đặc biệt ứng dụng rộng rãi trong thiết kế hệ thống nhúng, giao thức truyền thông và hệ thống điều khiển. Theo ước tính, hơn 70% các hệ thống reactive hiện nay được đặc tả dưới dạng FSM nhằm mô tả chính xác hành vi thay đổi trạng thái dựa trên các kích thích đầu vào. Tuy nhiên, việc kiểm thử các hệ thống này để đảm bảo tính chính xác và phù hợp với đặc tả vẫn còn nhiều thách thức do sự phức tạp trong mô hình hóa và kiểm chứng trạng thái.

Luận văn tập trung nghiên cứu các phương pháp sinh chuỗi kiểm thử (test case) dựa trên mô hình FSM nhằm kiểm thử sự mô phỏng giữa mô hình đặc tả và mô hình cài đặt. Mục tiêu chính là phát triển phương pháp sinh ca kiểm thử hiệu quả dựa trên các chuỗi kiểm chứng trạng thái như chuỗi vào-ra duy nhất (UIO), chuỗi phân biệt (DS) và chuỗi đặc trưng (W), từ đó đánh giá tính chấp nhận được của hệ thống cài đặt so với đặc tả. Nghiên cứu được thực hiện trên phạm vi các FSM có tính chất đơn định, được đặc tả đầy đủ và có tính liên thông mạnh, với dữ liệu thực nghiệm từ các mô hình FSM tiêu chuẩn trong ngành công nghệ phần mềm.

Ý nghĩa của nghiên cứu được thể hiện qua việc nâng cao độ tin cậy của phần mềm, giảm thiểu lỗi trong quá trình phát triển và tăng hiệu quả kiểm thử với độ bao phủ trạng thái và chuyển trạng thái đạt khoảng 100%. Kết quả nghiên cứu góp phần hoàn thiện các kỹ thuật kiểm thử dựa trên FSM, hỗ trợ các nhà phát triển và kiểm thử viên trong việc đảm bảo chất lượng phần mềm.

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

Khung lý thuyết áp dụng

Luận văn dựa trên các lý thuyết và mô hình sau:

• Máy hữu hạn trạng thái (FSM): Mô hình Mealy được sử dụng làm cơ sở, trong đó FSM được định nghĩa bởi bộ sáu thành phần ( M = \langle S, I, O, s_0, \delta, \lambda \rangle ), với (S) là tập trạng thái, (I) tập đầu vào, (O) tập đầu ra, (s_0) trạng thái ban đầu, (\delta) hàm chuyển trạng thái và (\lambda) hàm đầu ra.

• Chuỗi kiểm chứng trạng thái: Bao gồm ba loại chuỗi chính là chuỗi vào-ra duy nhất (UIO), chuỗi phân biệt (DS) và chuỗi đặc trưng (W). Các chuỗi này giúp phân biệt các trạng thái khác nhau trong FSM, từ đó xác định tính đúng đắn của hệ thống.

• Mối quan hệ mô phỏng giữa hai FSM: Định nghĩa mô phỏng được sử dụng làm tiêu chí đánh giá sự phù hợp giữa mô hình đặc tả và mô hình cài đặt. FSM cài đặt được coi là mô phỏng FSM đặc tả nếu mọi hành vi đầu vào-đầu ra của FSM đặc tả đều được FSM cài đặt phản ánh chính xác.

• Độ bao phủ mô hình FSM: Bao gồm độ bao phủ trạng thái (state coverage) và độ bao phủ chuyển trạng thái (transition coverage). Độ bao phủ chuyển trạng thái được chọn làm tiêu chí chính để sinh ca kiểm thử nhằm đảm bảo phát hiện tối đa lỗi.

Các khái niệm chuyên ngành như cây UIO, cây DS, phân vùng tương đương mức k, và thuật toán sinh ca kiểm thử dựa trên cây kiểm thử được áp dụng để xây dựng và đánh giá các chuỗi kiểm thử.

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

Nguồn dữ liệu nghiên cứu bao gồm các mô hình FSM tiêu chuẩn được biểu diễn dưới dạng đồ thị và bảng chuyển trạng thái, cùng với các ví dụ thực tế về FSM đặc tả hàm toán học và hệ thống cài đặt tương ứng. Cỡ mẫu nghiên cứu là tập hợp các FSM có số trạng thái từ 4 đến 10, được lựa chọn theo phương pháp chọn mẫu ngẫu nhiên có chủ đích nhằm đảm bảo tính đại diện.

Phương pháp phân tích bao gồm:

• Xây dựng cây UIO, cây DS và phân vùng tương đương để xác định các chuỗi kiểm chứng trạng thái.

• Áp dụng thuật toán sinh ca kiểm thử dựa trên độ bao phủ chuyển trạng thái, kết hợp với chuỗi kiểm chứng trạng thái để tạo bộ ca kiểm thử đầy đủ.

• So sánh hành vi đầu ra của FSM cài đặt với FSM đặc tả qua các ca kiểm thử để đánh giá tính mô phỏng.

Timeline nghiên cứu kéo dài trong 12 tháng, bao gồm các giai đoạn: thu thập dữ liệu và xây dựng mô hình (3 tháng), phát triển thuật toán sinh ca kiểm thử (4 tháng), thực nghiệm và đánh giá (3 tháng), tổng hợp kết quả và hoàn thiện luận văn (2 tháng).

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

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

1. Hiệu quả của chuỗi UIO trong kiểm chứng trạng thái: Qua thực nghiệm với FSM có 4 trạng thái, chuỗi UIO được xác định cho từng trạng thái với độ dài trung bình khoảng 4-5 ký tự đầu vào, giúp phân biệt chính xác các trạng thái. Ví dụ, trạng thái A có chuỗi UIO là "010" với đầu ra tương ứng "000", trong khi trạng thái D có chuỗi "11010" với đầu ra "00000". Tỷ lệ phân biệt trạng thái đạt 100%.

2. Chuỗi phân biệt (DS) giúp rút ngắn ca kiểm thử: Với FSM 4 trạng thái, một chuỗi DS duy nhất "11" có thể phân biệt tất cả các trạng thái, giảm số lượng ca kiểm thử cần thiết so với UIO. Đầu ra tương ứng cho các trạng thái khác nhau như A: "00", B: "11", C: "10", D: "01" cho thấy tính hiệu quả của DS trong việc kiểm thử.

3. Phương pháp W áp dụng cho FSM không có UIO và DS: Qua phân vùng tương đương mức k, tập chuỗi đặc trưng W được xác định gồm các chuỗi như "a", "aa", "aaa", "baaa", giúp phân biệt các trạng thái trong FSM phức tạp hơn. Điều này mở rộng khả năng kiểm thử cho các FSM khó phân biệt bằng UIO hoặc DS.

4. Độ bao phủ chuyển trạng thái đạt 100% giúp phát hiện lỗi hiệu quả: Sử dụng cây kiểm thử xây dựng từ FSM C1 với 10 trạng thái, chuỗi chuyển trạng thái được thiết kế để bao phủ tất cả các cạnh của đồ thị. Ví dụ, đường đi q1 → q4 → q3 → q5 → q2 → q1 bao phủ 5/10 chuyển trạng thái, trong khi toàn bộ cây kiểm thử đảm bảo bao phủ 100%. Điều này giúp phát hiện các lỗi về output và trạng thái trong quá trình cài đặt.

Thảo luận kết quả

Kết quả cho thấy việc sử dụng chuỗi kiểm chứng trạng thái kết hợp với độ bao phủ chuyển trạng thái là phương pháp hiệu quả để sinh ca kiểm thử cho FSM. Chuỗi UIO và DS giúp giảm số lượng ca kiểm thử cần thiết, trong khi phương pháp W mở rộng khả năng kiểm thử cho các FSM phức tạp hơn. Độ bao phủ chuyển trạng thái được chứng minh là tiêu chí mạnh nhất để phát hiện lỗi, vượt trội hơn so với độ bao phủ trạng thái đơn thuần.

So sánh với các nghiên cứu trước đây, phương pháp sinh ca kiểm thử dựa trên cây kiểm thử và chuỗi kiểm chứng trạng thái cho phép kiểm thử toàn diện hơn, giảm thiểu rủi ro bỏ sót lỗi. Việc áp dụng mối quan hệ mô phỏng giữa hai FSM làm tiêu chí đánh giá tính chấp nhận được của hệ thống cài đặt cũng là điểm mới, giúp kiểm thử viên có căn cứ rõ ràng để đánh giá kết quả kiểm thử.

Dữ liệu có thể được trình bày qua biểu đồ cây UIO, cây DS, bảng phân vùng tương đương và sơ đồ cây kiểm thử, giúp trực quan hóa quá trình sinh ca kiểm thử và đánh giá độ bao phủ.

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

1. Áp dụng phương pháp sinh ca kiểm thử dựa trên độ bao phủ chuyển trạng thái: Để đảm bảo phát hiện tối đa lỗi, các tổ chức phát triển phần mềm nên ưu tiên thiết kế ca kiểm thử đạt độ bao phủ chuyển trạng thái 100% trong các dự án sử dụng FSM. Thời gian thực hiện có thể từ 2-4 tuần tùy quy mô dự án.

2. Sử dụng chuỗi kiểm chứng trạng thái UIO hoặc DS để giảm thiểu số lượng ca kiểm thử: Khi FSM có chuỗi UIO hoặc DS, nên tận dụng để tối ưu hóa bộ ca kiểm thử, giảm chi phí và thời gian kiểm thử. Chủ thể thực hiện là nhóm kiểm thử phần mềm, áp dụng trong giai đoạn thiết kế ca kiểm thử.

3. Phát triển công cụ tự động sinh ca kiểm thử dựa trên cây kiểm thử và chuỗi kiểm chứng trạng thái: Đề xuất xây dựng phần mềm hỗ trợ tự động hóa quá trình sinh ca kiểm thử, giúp tăng hiệu quả và độ chính xác. Thời gian phát triển dự kiến 6-8 tháng, chủ thể là các nhóm nghiên cứu và phát triển công cụ kiểm thử.

4. Đào tạo và nâng cao nhận thức về kiểm thử dựa trên FSM cho đội ngũ phát triển và kiểm thử: Tổ chức các khóa đào tạo chuyên sâu về FSM, phương pháp sinh ca kiểm thử và đánh giá mô phỏng để nâng cao năng lực kiểm thử. Thời gian đào tạo khoảng 1-2 tháng, chủ thể là các trung tâm đào tạo và phòng ban phát triển phần mềm.

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

1. Nhà phát triển phần mềm: Giúp hiểu rõ về mô hình FSM và các phương pháp kiểm thử hiệu quả, từ đó cải thiện chất lượng sản phẩm và giảm thiểu lỗi trong quá trình phát triển.

2. Kiểm thử viên phần mềm: Cung cấp kiến thức chuyên sâu về kỹ thuật sinh ca kiểm thử dựa trên FSM, giúp thiết kế bộ ca kiểm thử toàn diện và hiệu quả hơn.

3. Nhà nghiên cứu trong lĩnh vực công nghệ phần mềm: Là tài liệu tham khảo quan trọng để phát triển các phương pháp kiểm thử mới, đặc biệt trong kiểm thử hệ thống reactive và nhúng.

4. Quản lý dự án phần mềm: Hỗ trợ đánh giá và lựa chọn các phương pháp kiểm thử phù hợp nhằm đảm bảo tiến độ và chất lượng dự án, đồng thời tối ưu chi phí kiểm thử.

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

1. FSM là gì và tại sao lại quan trọng trong kiểm thử phần mềm?
   FSM là mô hình hữu hạn trạng thái dùng để mô tả hành vi của hệ thống dựa trên trạng thái và chuyển trạng thái. Nó quan trọng vì giúp mô hình hóa chính xác các hệ thống reactive, từ đó thiết kế ca kiểm thử hiệu quả để phát hiện lỗi.

2. Chuỗi UIO, DS và W khác nhau như thế nào?
   Chuỗi UIO là chuỗi đầu vào-đầu ra duy nhất phân biệt từng trạng thái, DS là chuỗi đầu vào phân biệt tất cả trạng thái cùng lúc, còn W là tập chuỗi đặc trưng dùng khi FSM không có UIO hoặc DS. Mỗi loại có ưu nhược điểm riêng trong việc sinh ca kiểm thử.

3. Làm thế nào để đánh giá một FSM cài đặt có mô phỏng FSM đặc tả hay không?
   Bằng cách so sánh hành vi đầu ra của FSM cài đặt với FSM đặc tả qua các chuỗi kiểm chứng trạng thái và các ca kiểm thử dựa trên độ bao phủ chuyển trạng thái. Nếu mọi hành vi đều phù hợp, FSM cài đặt được coi là mô phỏng FSM đặc tả.

4. Độ bao phủ chuyển trạng thái có ưu điểm gì so với độ bao phủ trạng thái?
   Độ bao phủ chuyển trạng thái mạnh hơn vì đảm bảo mỗi chuyển trạng thái được kiểm thử ít nhất một lần, giúp phát hiện lỗi liên quan đến chuyển trạng thái mà độ bao phủ trạng thái có thể bỏ sót.

5. Phương pháp sinh ca kiểm thử dựa trên FSM có thể áp dụng cho những hệ thống nào?
   Phương pháp này phù hợp với các hệ thống reactive, hệ thống nhúng, giao thức truyền thông và các phần mềm có mô hình hành vi phức tạp được đặc tả bằng FSM, đặc biệt khi cần kiểm thử hộp đen.

Kết luận

• Luận văn đã phát triển thành công phương pháp sinh ca kiểm thử dựa trên mô hình máy hữu hạn trạng thái, kết hợp chuỗi kiểm chứng trạng thái và độ bao phủ chuyển trạng thái để đảm bảo kiểm thử toàn diện.
• Các chuỗi UIO, DS và W được áp dụng hiệu quả trong việc phân biệt trạng thái và giảm thiểu số lượng ca kiểm thử cần thiết.
• Độ bao phủ chuyển trạng thái được xác định là tiêu chí mạnh nhất để phát hiện lỗi trong quá trình cài đặt FSM.
• Phương pháp kiểm thử dựa trên mối quan hệ mô phỏng giữa hai FSM giúp đánh giá chính xác tính chấp nhận được của hệ thống cài đặt so với đặc tả.
• Hướng nghiên cứu tiếp theo là phát triển công cụ tự động sinh ca kiểm thử và mở rộng áp dụng cho các FSM phức tạp hơn trong thực tế.

Để nâng cao chất lượng phần mềm, các nhà phát triển và kiểm thử viên nên áp dụng các kỹ thuật sinh ca kiểm thử dựa trên FSM được trình bày trong luận văn này. Hãy bắt đầu xây dựng bộ ca kiểm thử hiệu quả ngay hôm nay để đảm bảo hệ thống của bạn hoạt động chính xác và tin cậy!