Báo cáo " Nghiên cứu kỹ thuật sinh ca kiểm thử từ mô hình máy hữu hạn trạng thái "

Chia sẻ: Phạm Huy | Ngày: | Loại File: PDF | Số trang:12

Thêm vào BST

Báo xấu

101
lượt xem 14
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Trình bày về mô hình FSM và cách biểu diễn một FSM theo kiểu liệt kê, đồ thị hoặc dạng bảng. Ngoài ra, trình bày một số tính chất của một máy hữu hạn trạng thái. Nghiên cứu một số phƣơng pháp xác định chuỗi kiểm chứng trạng thái của mô hình FSM nhƣ: chuỗi vào – ra duy nhất (UIO), chuỗi phân biệt (DS), chuỗi đặc trƣng (W). Tìm hiểu mối quan hệ mô phỏng của hai FSM và kiểm thử sự mô phỏng của hai FSM và tổng hợp các lỗi thƣờng gặp khi cài đặt FSM. Trình...

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Báo cáo " Nghiên cứu kỹ thuật sinh ca kiểm thử từ mô hình máy hữu hạn trạng thái "

Nghiên cứu kỹ thuật sinh ca kiểm thử từ mô hình máy hữu hạn trạng thái Research the method to generate test case from finite state machine model NXB H. : ĐHCN, 2012 Số trang 58 tr. + Đoàn Thị Thùy Linh Trƣờng Đại học Công nghệ Luận văn ThS ngành: Công nghệ phần mềm; Mã số: 60 48 10 Cán bộ hƣớng dẫn khoa học: TS. Đặng Văn Hƣng Năm bảo vệ: 2012 Abstract. Trình bày về mô hình FSM và cách biểu diễn một FSM theo kiểu liệt kê, đồ thị hoặc dạng bảng. Ngoài ra, trình bày một số tính chất của một máy hữu hạn trạng thái. Nghiên cứu một số phƣơng pháp xác định chuỗi kiểm chứng trạng thái của mô hình FSM nhƣ: chuỗi vào – ra duy nhất (UIO), chuỗi phân biệt (DS), chuỗi đặc trƣng (W). Tìm hiểu mối quan hệ mô phỏng của hai FSM và kiểm thử sự mô phỏng của hai FSM và tổng hợp các lỗi thƣờng gặp khi cài đặt FSM. Trình bày độ bao phủ của mô hình máy hữu hạn trạng thái và lựa chọn độ bao phủ tốt nhất để làm tiền đề sinh ca kiểm thử, phƣơng pháp sinh ca kiểm thử và đƣa ra ví dụ để cụ thể hóa phƣơng pháp đã nêu. Tổng kết những kết quả đã đạt đƣợc và hƣớng phát triển nghiên cứu tiếp theo. Keywords: Công nghệ phần mềm; Kiểm thử phần mềm; Kỹ thuật sinh ca; Mô hình máy Content. I. CHƢƠNG 1. GIỚI THIỆU A. 1.1. Đặt vấn đề Hiện nay có rất nhiều hệ thống có thể đƣợc đặc tả nhƣ là một máy trạng thái, đó là các hệ thống nhƣ: giao thức truyền thông, hệ thống điều khiển, hệ thống nhúng. Điều này thúc đẩy việc nghiên cứu các phƣơng pháp tiếp cận chính thức để kiểm thử các máy trạng thái hữu hạn để khám phá các khía cạnh của hành vi của chúng và để đảm bảo chức năng chính xác của hệ thống. Tuy nhiên tính chính xác của hệ thống cài đặt so với đặc tả đƣợc đo đạc nhƣ thế nào, khi nào thì một hệ thống cài đặt đƣợc gọi là chấp nhận đƣợc thì hiện nay các tài liệu còn đang viết rất chung chung. Trong luận văn này tôi xin giới thiệu khái niệm mô phỏng của hai máy hữu hạn trạng thái nhƣ là một tiêu chí để đánh giá tính chấp nhận đƣợc của hệ thống và trình bày 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 để kiểm thử sự mô phỏng của hai máy hữu hạn trạng thái. B. 1.2. Nội dung nghiên cứu Luận văn tập trung nghiên cứu một số phƣơng pháp xác định 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), chuỗi đặc trƣng (W), phƣơng pháp kiểm thử hệ thống dựa trên mô hình máy hữu hạn trạng thái để từ đó nghiên cứu, tìm ra phƣơng pháp sinh ca kiểm
thử để kiểm thử xem mô hình cài đặt có mô phỏng bản đặc tả phần mềm theo mô hình máy hữu hạn trạng thái hay không. C. 1.3. Cấu trúc luận văn Phần còn lại của luận văn có cấu trúc nhƣ sau: Chương 2: Máy hữu hạn trạng thái (FSM). Chƣơng này trình bày về mô hình FSM và cách biểu diễn một FSM theo kiểu liệt kê, đồ thị hoặc dạng bảng. Ngoài ra, trong chƣơng này cũng trình bày một số tính chất của một máy hữu hạn trạng thái. Chương 3: Một số phương pháp xác định chuỗi kiểm chứng trạng thái. Chƣơng này trình bày một số phƣơng pháp xác định chuỗi kiểm chứng trạng thái của mô hình FSM nhƣ: chuỗi vào – ra duy nhất (UIO), chuỗi phân biệt (DS), chuỗi đặc trƣng (W). Chương 4: Kiểm thử dựa trên mô hình FSM. Ngoài việc trình bày mối quan hệ mô phỏng của hai FSM và kiểm thử sự mô phỏng của hai FSM, chƣơng này còn tổng hợp các lỗi thƣờng gặp khi cài đặt FSM. Chương 5: Kỹ thuật sinh ca kiểm thử. Ngoài việc trình bày độ bao phủ của mô hình máy hữu hạn trạng thái và lựa chọn độ bao phủ tốt nhất để làm tiền đề sinh ca kiểm thử, chƣơng này còn trình bày phƣơng pháp sinh ca kiểm thử và đƣa ra ví dụ để cụ thể hóa phƣơng pháp đã nêu. Chương 6: Kết luận tổng kết những kết quả đã đạt đƣợc của luận văn và hƣớng phát triển nghiên cứu tiếp theo. II. CHƢƠNG 2. MÁY HỮU HẠN TRẠNG THÁI (FSM) A. 2.1. Định nghĩa FSM Máy hữu hạn trạng thái là một bộ M = . Trong đó  S là tập các trạng thái  I là tập thông tin đầu vào  O là tập thông tin đầu ra  s0 là trạng thái ban đầu  δ: S x I → S là hàm chuyển trạng thái  λ: S x I → O là hàm thông tin đầu ra B. 2.2. Biểu diễn FSM 1) 2.2.1. Biểu diễn kiểu liệt kê Cho FSM M1 =
2) 2.2.2. Biểu diễn bằng đồ thị Các FSM và các yếu tố của chúng đƣ ợc biểu diễn bằng đồ thị. Các yế u tố chinh trong đồ thi ̣bao ́ gồm:  Mỗi tra ̣ng thái đƣơ ̣c mô tả nhƣ là mô ̣t nút (node) trong đồ thi.̣  Mỗi sƣ̣ chuyể n tiế p đƣơ ̣c diễn tả nhƣ mô ̣t đƣờng link đƣơ ̣c kế t nố i trƣ̣c tiế p tƣ̀ tra ̣ng thái này sang tra ̣ng thái khác đƣợc coi là cạnh của đồ thị với nhãn là cặp Input/Output (ký hiệu / để phân biệt input và output). Ví dụ về biểu diễn bằng đồ thị của FSM M1: Hình 2.1: Minh họa việc biểu diễn FSM M1 bằng đồ thị 3) 2.2.3. Biểu diễn bằng dạng bảng Một FSM có thể biểu diễn bằng dạng bảng, bảng thƣờng là kiể u ma trâ ̣n vuông (N x N ô) C. 2.3. Một số tính chất của FSM  Đặc tả đầy đủ (Completely specified)  Đơn định (Deterministic  Liên thông mạnh (Strongly connected)  Tối giản (Reduced Các thuật toán trình bày trong luận văn chỉ áp dụng với FSM có tính chất reduced. Các phƣơng pháp tìm chuỗi input y – chuỗi phân biệt các trạng thái sẽ đƣợc trình bày ở chƣơng 3. III. CHƢƠNG 3. MỘT SỐ PHƢƠNG PHÁP TÌM CHUỖI KIỂM CHỨNG TRẠNG THÁI Chuỗi kiểm chứng trạng thái (state verification sequence) là chuỗi mà có thể phân biệt trạng thái này với trạng thái khác của một FSM. Theo [5] có 3 loại chuỗi thƣờng dùng để kiểm chứng trạng thái của FSM, đó là:  Chuỗi vào – ra duy nhất (Unique Input - Output sequence)  Chuỗi phân biệt (Distinguishing sequence)  Chuỗi đặc trƣng (Characterizing sequence) Các phần tiếp theo sẽ trình bày chi tiết phƣơng pháp để tìm 3 loại chuỗi này.
A. .1. Chuỗi vào – ra duy nhất (Unique Input - Output sequence) 1) 3.1.1. Một số khái niệm  Chuỗi vào - ra duy nhất (Unique input – output sequence): Một chuỗi y/λ(si, y) đƣợc gọi là chuỗi UIO cho mỗi trạng thái si của FSM M nếu và chỉ nếu y/λ(si, y) y/λ(sj, y) với i j và ∀sj ∈ M. 2) 3.1.2. Thuật toán sinh cây UIO Input: M = và L. Output: cây UIO. Phương pháp: Thực hiện các bƣớc sau Bước 1: Đặt ψ là một tập các vec-tơ đƣờng dẫn trong cây UIO, ban đầu ψ chứa vec-tơ ban đầu và đƣợc gán là không kết thúc. Bước 2: Tìm một phần tử chƣa kết thúc ψ ∈ ψ mà chƣa đƣợc “tính toán”. Nếu không tồn tại phần tử nào nhƣ vậy thì thuật toán kết thúc. Bước 3: Tính toán ψ‟ = pert(ψ, ai/bi) và thêm ψ‟ vào ψ với ∀ai/bi ∈ L. Đánh dấu ψ đã đƣợc “tính toán” và cập nhật cây UIO. Bước 4: Nếu pert(ψ, ai/bi), đã tính toán ở Bước 3 thỏa mãn điều kiện cắt tỉa, thì đánh dấu ψ‟ là một nút kết thúc. Bước 5: Quay lại bƣớc 2. Ví dụ: Cho FSM G1 như sau: Hình 3.1: Đồ thị mô tả FSM G1 Cây UIO của FSM G1 đƣợc xây dựng nhƣ sau: Hình 3.2: Cây UIO của FSM G1 ở Hình 3.1. Từ cây UIO của G1 ta tìm đƣợc chuỗi UIO nhƣ bảng 3.1 dƣới đây: Bảng 3.1 Chuỗi UIO của FSM G1
Trạng thái Chuỗi vào Chuỗi ra A 010 000 B 010 001 C 1010 0000 D 11010 00000 B. 3.2. Chuỗi phân biệt (Distinguishing sequence) 1) 3.2.1. Một số khái niệm Cho FSM M = với |S| = n Chuỗi phân biệt (distinguishing sequence): Một chuỗi thông tin đầu vào x đƣợc gọi là chuỗi phân biệt nếu và chỉ nếu λ(si, x) = λ(sj, x) với ∀si, sj ∈ S và si = sj. 2) 3.2.2. Thuật toán sinh cây DS Input : M = . Output: Cây DS. Phương pháp: Thực hiện các bƣớc sau: Bước 1: Gọi ψ là một tập các khối trạng thái trong cây DS. Ban đầu, ψ chứa khối trạng thái ban đầu và đƣợc gán là không kết thúc. Bước 2: Tìm một thành phần ψ ∈ ψ mà vẫn chƣa đƣợc “tính toán”. Nếu không có thành phần nào nhƣ thế tồn tại thì thuật toán kết thúc. Bước 3: Tính toán ψ’ = dpert(ψ, a) và thêm ψ’ vào ψ với∀a ∈ I. Gán ψ đã đƣợc “tính toán” và cập nhật DS tree. Bước 4: Nếu dpert (ψ, a) đƣợc tính toán ở Bước 3 thỏa mãn điều kiện kết thúc D1, D2 hoặc D3 thì gán ψ’ là nút kết thúc. Bước 5: Quay lại Bước 2 Ví dụ cho FSM G2 nhƣ sau: Hình 3.2: Đồ thị mô tả FSM G2. Áp dụng thuật toán trên sinh cây DS cho FSM G2 nhƣ hình 3.3 dƣới đây:
Hình 3.3: Cây DS của FSM G2 ở Hình 3.2 Chuỗi „11‟ là chuỗi phân biệt của các trạng thái, đƣợc kiểm chứng tại bảng 3.3 bên dƣới. Bảng 3.3 Bảng chuỗi phân biệt của các trạng thái của FSM G2 Trạng thái Chuỗi vào Chuỗi ra A 11 00 B 11 11 C 11 10 D 11 01 C. 3.3. Chuỗi đặc trưng (Characterizing sequence) 1) 3.3.1. Một số khái niệm  W là một tập hữu hạn các chuỗi input mà phân biệt hành vi của bất kỳ một cặp trạng thái nào trong FSM M. Mỗi input trong W có độ dài hữu hạn.  Sự phân vùng tƣơng đƣơng mức k (k-equivalence partition) của tập trạng thái Q ký hiệu là Pk là một tập hợp hữu hạn n tập W1, W2, ..., Wn. Nghĩa là: Uni = 1Wi = Q Nếu trạng thái si thuộc Wi và sj thuộc Wj với i ≠ j thì si và sj là 2 trạng thái có thể phân biệt ở mức k. 2) 3.3.2. Phương pháp tìm W Bước 1: Xây dựng 1 chuỗi của phân vùng tƣơng đƣơng mức k của tập trạng thái Q, giả sử là P1, P2, …, Pm. Bước 2: Theo phân vùng tƣơng đƣơng mức k theo thứ tự ngƣợc lại để tìm chuỗi phân biệt cho mỗi cặp trạng thái. IV. CHƢƠNG 4. KIỂM THỬ DỰA TRÊN MÔ HÌNH FSM A. 4.1. Mối quan hệ mô phỏng của hai FSM ξ ⊆ S1× S2 là quan hệ mô phỏng từ FSM MS = thành FSM MI = nếu: 1. (s01, s02 ) ∈ ξ 2. (s1, s2 ) ∈ ξ =>
{∀i ∀o ∀s1‟ [(s1 s1‟) => [(s2s2‟) ∧ (s1‟, s2‟ ∈ ξ)]]} Nếu ξ nhƣ thế tồn tại thì MI mô phỏng MS. Trong quá trình cài đặt MI đã “làm mịn” MS, hay nói cách khác MI mô phỏng MS. Tuy nhiên việc cài đặt MI có thể có lỗi dẫn đến MI không mô phỏng MS, do đó phần tiếp theo sẽ trình bày phƣơng pháp kiểm thử để kiểm thử xem MI có mô phỏng MS hay không. B. 4.2. Kiểm thử dựa trên mô hình FSM Một hệ thống đƣợc đặc tả bởi FSM MS và đƣợc cài đặt bằng MI. Kiểm thử xem hệ thống MI có “hoạt động đúng” theo nhƣ đặc tả MS hay không bằng cách so sánh hành vi của hai máy trạng thái dựa trên sự quan sát hành vi input/output của MI gọi là kiểm tra sự phù hợp hay sự tìm lỗi [6]. Nhƣ thế nào là “hoạt động đúng”, nhƣ thế nào là “phù hợp”, nhƣ thế nào là “lỗi”? Căn cứ vào đâu để chúng ta có thể đƣa ra kết luận MI hoạt động đúng theo đặc tả MS? Trong luận văn này tôi xin đề xuất khái niệm mô phỏng nhƣ là một tiêu chí để đánh giá MI có “hoạt động đúng” nhƣ đặc tả hay không. Nhƣ vậy, bài toán ở đây là kiểm thử xem MI có mô phỏng MS hay không, nếu MI không mô phỏng MS thì có lỗi trong quá trình cài đặt. Phƣơng pháp kiểm thử với việc kiểm chứng trạng thái [5] là cách để giúp trả lời xem FSM MI có mô phỏng MS hay không. Ý tƣởng của phƣơng pháp đƣợc thể hiện trong mô hình 4.3 dƣới đây Hình 4.3: Mô hình khái niệm kiểm thử với việc kiểm chứng trạng thái C. 4.3. Một số lỗi thường gặp khi kiểm thử sự mô phỏng của 2 FSM Khi có bản đặc tả FSM MS = < S1, I, O, s01, δ1, λ1> và hệ thống cài đặt FSM MI = < S2, I, O, s02, δ2, λ2> , một câu hỏi đặt ra là FSM MI có mô phỏng FSM MS hay không? Bảng tổng hợp thông tin 4.1 sau là lời giải đáp cho câu hỏi này Bảng 4.1: Tổng hợp các trường hợp lỗi khi cài đặt MI ∃λ1(s01, x) = ∃λ1(s01, x) ≠ ∃[λ1(s1, a) ≠ ∃[λ1(s2, x) ≠ ∃[λ1(s2, x) = Kết luận λ2(s02, x) λ2(s02, x) λ2(s2, a)] λ2(s2‟, x)] λ2(s2‟, x)] - T - - - No T F T - - No T F F T - No T F F F T Yes
“No”: MI không mô phỏng MS “Yes” : MI có mô phỏng MS Nhƣ vậy qua bảng tổng hợp 4.1 ta có thể thấy một số lỗi thƣờng gặp khi kiểm thử sự mô phỏng của hai FSMs nhƣ sau: 1. Lỗi liên quan đến output: Output ứng với transition từ s2 s2‟ của MI không giống với output ứng với transition s1 s1‟ của MS. 2. Lỗi liên quan đến trạng thái: - Trạng thái ban đầu của MI không mô phỏng trạng thái ban đầu của MS - Trạng thái tiếp theo của một chuyển trạng thái của MI không mô phỏng trạng thái trạng thái tiếp theo ứng với chuyển trạng thái tƣơng ứng của MS. V. CHƢƠNG 5. KỸ THUẬT SINH CA KIỂM THỬ A. 5.1. Độ bao phủ mô hình máy hữu hạn trạng thái Để kiểm thử FSM MI thì cần thiết kế bao nhiêu ca kiểm thử? Căn cứ vào đâu để biết đƣợc số ca kiểm thử đã đủ hay chƣa? Dùng hai chỉ số để đo độ bao phủ là: Độ bao phủ trạng thái (state coverage) và độ bao phủ chuyển trạng thái (transition coverage). 1) 5.1.1. Độ bao phủ trạng thái (state coverage) Để đạt đƣợc độ bao phủ trạng thái ta lựa chọn chuỗi các chuyển đổi trạng thái sao cho mỗi trạng thái đƣợc thăm ít nhất một lần [5]. 2) 5.1.2. Độ bao phủ chuyển trạng thái (transition coverage) Để đạt đƣợc độ bao phủ chuyển trạng thái ta lựa chọn chuỗi các chuyển trạng thái sao cho mỗi chuyển trạng thái đƣợc thăm ít nhất một lần [5]. Bài toán này sẽ tƣơng đƣơng với việc tìm đƣờng đi qua tất cả các cạnh của một đồ thị có hƣớng sao cho mỗi cạnh đƣợc qua ít nhất một lần. Vì mỗi cạnh của đồ thị tƣơng đƣơng với một sự chuyển trạng thái mà các trạng thái là hữu hạn nên việc tìm đƣờng đi này là hoàn toàn có thể thực hiện đƣợc. Để tìm độ bao phủ chuyển trạng thái ta xây dựng cây kiểm thử từ mô hình FSM. Cây kiểm thử của một FSM là một cây có gốc là trạng thái ban đầu. Từ trạng thái ban đầu, nó chứa ít nhất một đƣờng đi từ trạng thái ban đầu tới các trạng thái còn lại của FSM [2]. Sau đây là cách xây dựng cây kiểm thử Bước 1: Gốc của cây kiểm thử là trạng thái ban đầu. Bước 2: Giả sử rằng cây kiểm thử đã đƣợc xây dựng đến mức k, mức thứ k+1 sẽ đƣợc xây dựng nhƣ sau: Chọn một node n tại mức k. Nếu n xuất hiện ở mức bất kỳ từ 1 đến k thì n là node lá và không xây dựng thêm nhánh này. Nếu n không phải là node lá thì tiếp tục xây dựng nhánh này bằng cách thêm một nhánh từ n tới node mới m nếu d(n, x) = m. Gán nhãn của nhánh này là x/y với y = λ(n, x). Lặp lại bƣớc này với tất cả các nút ở mức k
Tiếp theo ta tìm tập bao phủ trạng thái P từ cây kiểm thử. Tập bao phủ trạng thái P = {p1, p2, … pn} là một tập tất cả các chuỗi con pi thể hiện đƣờng dẫn con bắt đầu từ nút gốc trong cây kiểm thử, nối các nhãn theo các cạnh của đƣờng dẫn con ta đƣợc một chuỗi thuộc P. B. 5.3. Kỹ thuật sinh ca kiểm thử Ca kiểm thử tốt là ca kiểm thử có thể bao phủ toàn bộ mô hình FSM. Do vậy ta chọn độ bao phủ chuyển trạng thái, nếu độ bao phủ là 100% thì có thể phát hiện đƣợc tất cả các lỗi về output và các lỗi về trạng thái. 1) 5.1.3. Khuôn dạng ca kiểm thử Thông thƣờng khuôn dạng của một ca kiểm thử bao gồm thông tin sau: Bảng 5.1: Khuôn dạng ca kiểm thử Expected TC_ID Pre-Con Input Post-Con Output Thông tin tiền Thông tin Input Thông tin kết Thông tin hậu TC_1 điều kiện quả mong đợi điều kiện C. 5.2. Phương pháp sinh ca kiểm thử Từ mô hình đặc tả MS, ta sinh ca kiểm thử để kiểm thử MI theo các bƣớc nhƣ sau: 1. Sinh cây kiểm thử và tìm tập bao phủ chuyển trạng thái Với phƣơng pháp sinh cây kiểm thử và phƣơng pháp tìm tập bao phủ chuyển trạng thái đã trình bày tại mục 5.2.2, sau bƣớc này ta có tập bao phủ chuyển trạng thái P. 2. Tìm chuỗi kiểm chứng trạng thái Áp dụng một trong các phƣơng pháp đã trình bày tại chƣơng 3 để tìm chuỗi kiểm chứng. Giả sử chuỗi kiểm chứng tìm đƣợc là x. 3. Sinh ca kiểm thử Với mỗi phần tử của tập chuyển trạng thái hay với một đƣờng dẫn con trên cây kiểm thử kết hợp với việc kiểm chứng trạng thái đối với trạng trạng thái cuối cùng của đƣờng dẫn con sẽ sinh ra một ca kiểm thử. Ngoài ra, cần phải thiết kế thêm một ca kiểm thử để kiểm thử xem trạng thái đầu của MI có mô phỏng trạng thái đầu của MS hay không. Để kiểm thử trạng thái đầu của MI có mô phỏng MS hay không ta dùng chuỗi kiểm chứng để kiểm thử. Vì vậy đầu vào của ca kiểm thử này là chuỗi kiểm chứng, kết quả mong đợi là output sinh ra từ FSM MS. D. 5.3. Ví dụ Cho FSM MS đƣợc biểu diễn bởi đồ thị sau:
Hình 5.5: Đồ thị biểu diễn FSM MS Và FSM MI1 là bản cài đặt của FSM MS, giả sử đƣợc cài đặt nhƣ sau: Hình 5.6: Mô hình máy hữu hạn trạng thái MI1 Sau đây là phƣơng pháp sinh ca kiểm thử để kiểm thử xem MI1 có mô phỏng MS hay không 1. Tìm chuỗi kiểm chứng Áp dụng một trong các phƣơng pháp đã trình bày ở Chƣơng 4 để tìm chuỗi kiểm chứng trạng thái Mô hình máy hữu hạn trạng thái MS có chuỗi kiểm chứng trạng thái là 11 (áp dụng phƣơng pháp DS). 2. Xây dựng cây kiểm thử Xây dựng cây kiểm thử cho mô hình máy hữu hạn trạng thái MS Hình 5.7: Cây kiểm thử của mô hình máy hữu hạn trạng thái MS 3. Tìm tập bao phủ transition từ cây kiểm thử Sau khi xây dựng cây kiểm thử, bƣớc tiếp theo ta tiến hành tìm tập bao phủ transition từ cây kiểm thử. P = {0/0.B, 1/0.D, 0/0.0/0.A, 0/0.1/1.B, 1/0.0/1.D, 1/0.1/0.C, 1/0.1/0.0/1.D, 1/0.1/0.1/1.A} Sinh ca kiểm thử và kiểm thử Đối với mô hình cài đặt FSM MI1, ta có kết quả kiểm thử nhƣ bảng 5.6 dƣới đây.
Bảng 5.6: Kết quả kiểm thử của FSM MI1 TC_ID Pre-Con Input Expected Output Actual result Post-Con TC0-1 N/A 11 00 00 A TC1-11 Passed TC0- 011 011 011 A TC1-21 Passed TC0- 111 001 001 A TC2-11 Passed TC1- 0011 0000 0000 A TC2-21 Passed TC1- 0111 0111 0111 A TC2-31 Passed TC1- 1011 0101 0101 A TC2-41 Passed TC1- 1111 0010 0010 A TC3-11 Passed TC2- 11011 00101 00101 A TC3-21 Passed TC2- 10111 00100 00100 A Nhận xét: Theo kết quả kiểm thử trên thì mọi Actual result đều giống nhƣ Expected Output tại ca kiểm thử tƣơng ứng nên FSM MI1 mô phỏng FSM MS. VI. CHƢƠNG 6. KẾT LUẬN Kiểm thử phần mềm, một nội dung nghiên cứu đƣợc triển khai từ rất sớm và không phải là mới mẻ đối với thế giới, nhƣng luôn là vấn đề cấp thiết cho việc nâng cao chất lƣợng phần mềm. Trong luận văn này, tác giả đã trình bày tổng quan về mô hình máy hữu hạn trạng thái và đi sâu nghiên cứu về phƣơng pháp xác định chuỗi kiểm chứng trạng thái nhƣ: xác định Unique Input – Output sequence, Distingguishing sequence, Characterizing sequence. Luận văn cũng trình bày phƣơng pháp kiểm thử dựa trên mô hình máy hữu hạn trạng thái và dùng khái niệm mô phỏng nhƣ là một tiêu chí để đánh giá sự cài đặt đúng đắn của hệ thống so với đặc tả. Luận văn đi sâu nghiên cứu về độ bao phủ của mô hình máy hữu hạn trạng thái, và từ đó đƣa ra phƣơng pháp sinh ca kiểm thử để kiểm thử xem hệ thống cài đặt có mô phỏng bản đặc tả phần mềm dựa trên mô hình máy hữu hạn trạng thái hay không. Hƣớng phát triển tiếp theo của luận văn là tìm cách cải tiến phƣơng pháp sinh ca kiểm thử sao cho số ca kiểm thử là ít nhất nhƣng độ bao phủ là lớn nhất có thể. Đồng thời, tác giả sẽ xây dựng một chƣơng trình sinh ca kiểm thử tự động dựa trên phƣơng pháp đã đƣợc cải tiến.
References. Tiếng việt 1. Ngô Thùy Linh (2010), Nghiên cứu kiểm thử bao phủ phần mềm và ứng dụng, Luận văn Thạc sĩ, Trƣờng Đại học Công Nghệ, Đại học Quốc Gia Hà Nội, tr.43-53. Tiếng anh 2. Aditya P. Mathur (2008), Foundations of Software Testing, Dorling Kindersley (India) Pvt. Ltd., pp.221-234. 3. Boris Beizer (1990), Software Testing Techniques, Second Edition, Van Nostrand Reinhold. 4. Jeff Tian (2005), Software Quality Engineering, John Wiley & Sons, Inc. 5. Kshirasagar Naik, Priyadarshi Tripathy (2008), Software Testing and Quality Assurance, John Wiley & Sons, Inc., pp.265-318. 6. K. Derderian, R. M. Hirons, M. Harman, Q. Guo (2006), “Automated Unique Input Output sequence generation for conformance testing of FSMs”, The Computer Journal, 00, 0. 7. Ngozi I. Ihemelandu, Carl J. Mueller (2011), “The Intractability of Finite State Machine Test Sequences”, Computer Science Technical Reports, (TXSTATE-CS-TR-2011-26), pp.6-12. 8. Timothy Kam (1997), Synthesis of Finite State Machine, Kluwer Acad. Publ., pp.200. 9. www.cs.odu.edu~toidanerzic390techedregularfafa-applications.html