Tài liệu 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

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ ĐOÀN THỊ THÙY LINH NGHIÊN CỨU PHƯƠNG PHÁP SNH CA KIỂM THỬ TỪ MÔ HÌNH MÁY HỮU HẠN TRẠNG THÁI Ngành: Công nghệ thông tin Chuyên ngành: Công nghệ phần mềm Mã số: 60 48 10 TÓM TẮT LUẬN VĂN THẠC SĨ Hà nội, 2012 3 MỤC LỤC DANH SÁCH BẢNG ................................................................................. 5 DANH SÁCH HÌNH VẼ ........................................................................... 6 DANH MỤC CÁC CHỮ VIẾT TẮT ......................................................... 7 Chương 1. GIỚI THIỆU ........................................................................... 8 1.1. Đặt vấn đề ......................................................................................... 8 1.2. Nội dung nghiên cứu ........................................................................ 8 1.3. Cấu trúc luận văn .............................................................................. 8 Chương 2. MÁY HỮU HẠN TRẠNG THÁI (FSM) .............................. 10 2.1. Định nghĩa FSM ............................................................................. 10 2.2. Biểu diễn FSM ................................................................................ 11 2.2.1. Biểu diễn kiểu liệt kê ................................................................ 11 2.2.2. Biểu diễn bằng đồ thị ................................................................ 12 2.2.3. Biểu diễn bằng dạng bảng ........................................................ 12 2.3. Một số tính chất của FSM............................................................... 13 2.3.1. Được đặc tả đầy đủ (Completely specified) ............................. 13 2.3.2. Đơn định (Deterministic).......................................................... 14 2.3.3. Liên thông mạnh (Strongly connected) .................................... 15 2.3.4. Tối giản (Reduced) ................................................................... 16 Chương 3. MỘT SỐ PHƯƠNG PHÁP XÁC ĐỊNH CHUỖI KIỂM CHỨNG TRẠNG THÁI ..................................................................................... 18 3.1. Chuỗi vào – ra duy nhất (Unique Input - Output sequence) [5] ..... 18 3.1.1. Một số khái niệm ...................................................................... 19 3.1.2. Thuật toán sinh cây UIO........................................................... 20 3.2. Chuỗi phân biệt (Distinguishing sequence) [5] .............................. 25 3.2.1. Một số khái niệm ...................................................................... 25 3.2.2. Thuật toán sinh cây DS............................................................. 27 3.3. Chuỗi đặc trưng (Characterizing sequence) [2] .............................. 29 3.3.1. Một số khái niệm ...................................................................... 29 3.3.2. Phương pháp tìm W .................................................................. 29 Chương 4. KIỂM THỬ DỰA TRÊN MÔ HÌNH FSM.......................... 34 4 4.1. Mối quan hệ mô phỏng của hai FSM ............................................. 34 4.2. Kiểm thử dựa trên mô hình FSM .................................................... 35 4.3. Một số lỗi thường gặp khi cài đặt FSM .......................................... 37 Chương 5. KỸ THUẬT SINH CA KIỂM THỬ ...................................... 40 5.1. Độ bao phủ mô hình máy hữu hạn trạng thái ................................. 40 5.1.1. Độ bao phủ trạng thái (state coverage) ..................................... 40 5.1.2. Độ bao phủ chuyển trạng thái (transition coverage) ................ 42 5.2. Kỹ thuật sinh ca kiểm thử ............................................................... 44 5.2.1. Khuôn dạng ca kiểm thử........................................................... 44 5.2.2. Phương pháp sinh ca kiểm thử ................................................. 45 5.3. Ví dụ ............................................................................................... 51 Chương 6. KẾT LUẬN ............................................................................ 57 TÀI LIỆU THAM KHẢO ........................................................................ 58 5 DANH SÁCH BẢNG ảng 2.1: Minh họa việc biểu diễn FSM bằng dạng bảng ........................ 13 Bảng 3.1: Chuỗi UIO của FSM G1 ........................................................... 24 Bảng 3.2: Ví dụ khối trạng thái................................................................. 26 Bảng 3.3: Bảng chuỗi phân biệt của các trạng thái của FSM G2.............. 29 Bảng 3.4: Bảng mô tả FSM G3 ................................................................. 30 Bảng 3.5: Bảng phân vùng tương đương mức 1 của FSM G3 .................. 31 Bảng 3.6: Bảng P1 phân vùng tương đương mức 2 của FSM G3 ............. 31 Bảng 3.7: Bảng P2 phân vùng tương đương mức 3 của FSM G3 ............. 32 Bảng 3.8: Bảng P3 phân vùng tương đương mức 4 của FSM G3 ............. 32 Bảng 3.9: Bảng P4 phân vùng tương đương mức 5 của FSM G3 ............. 32 Bảng 4.1: Bảng tổng hợp các lỗi khi cài đặt FSM MI .............................. 38 Bảng 5.1: Khuôn dạng ca kiểm thử .......................................................... 45 Bảng 5.2: Ca kiểm thử trạng thái ban đầu của FSM MS........................... 46 Bảng 5.3: Nhóm ca kiểm thử TC1 của FSM MS ...................................... 50 Bảng 5.4: Nhóm ca kiểm thử TC2- của FSM MS ..................................... 50 Bảng 5.5: Nhóm ca kiểm thử TCk- của FSM MS ..................................... 50 Bảng 5.6: Ca kiểm thử của FSM MS......................................................... 54 Bảng 5.7: Kết quả kiểm thử của FSM MI1 ................................................ 55 Bảng 5.8: Kết quả kiểm thử của FSM MI2 ................................................ 55 Bảng 5.9: Kết quả kiểm thử của FSM MI3 ................................................ 56 6 DANH SÁCH HÌNH VẼ Hình 2.1: Minh họa việc biểu diễn FSM bằng đồ thị ............................... 12 Hình 2.2: Ví dụ về FSM M1 được đặc tả đầy đủ....................................... 13 Hình 2.3: Ví dụ về FSM M2 không được đặc tả không đầy đủ. ............... 14 Hình 2.4: Ví dụ về FSM M3 có tính chất đơn định................................... 14 Hình 2.5: Ví dụ về FSM M4 có tính chất không đơn định........................ 15 Hình 2.6: Ví dụ về FSM M5 có tính liên thông mạnh. ............................. 15 Hình 2.7: Ví dụ về FSM M6 có tính liên thông yếu.................................. 16 Hình 2.8: Ví dụ về FSM M7 không được tối giản. ................................... 16 Hình 2.9: Ví dụ về FSM M8 được tối giản. .............................................. 17 Hình 3.1: Đồ thị mô tả FSM G1. ............................................................... 19 Hình 3.2: Cây UIO của FSM G1 ở hình 3.1 .............................................. 22 Hình 3.3: Xác định chuỗi UIO trên cây UIO ở hình 3.2 .......................... 23 Hình 3.4: Đồ thị mô tả FSM G2 ................................................................ 25 Hình 3.5: Cây DS của FSM G2 ở Hình 3.4 ............................................... 28 Hình 3.6: Mô hình FSM G3 ...................................................................... 30 Hình 4.1: Mô hình FSM đặc tả hàm y = |x| .............................................. 34 Hình 4.2: Mô hình FSM thể hiện cài đặt hàm y = |x| ............................... 34 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 [5]. .................................................................................................................... 36 Hình 5.1: Mô hình máy hữu hạn trạng thái C1.......................................... 41 Hình 5.2: Một đường đi bao phủ tất cả các trạng thái của FSM C1.......... 41 Hình 5.3: Cây kiểm thử của FSM C1. ....................................................... 43 Hình 5.4: Đồ thị biểu diễn FSM MS [5]. ................................................... 51 Hình 5.5: Mô hình máy hữu hạn trạng thái MI1 ........................................ 51 Hình 5.6: Mô hình máy hữu hạn trạng thái MI2. ....................................... 52 Hình 5.7: Mô hình máy hữu hạn trạng thái MI3. ....................................... 52 Hình 5.8: Cây kiểm thử từ mô hình FSM MS. .......................................... 53 7 DANH MỤC CÁC CHỮ VIẾT TẮT Từ viết tắt DS Ý nghĩa Giải thích tiếng Việt Distinguishing sequence Chuỗi phân biệt FSM Finite state machine Máy hữu hạn trạng thái UIO Unique Input - Output sequence Chuỗi vào – ra duy nhất VER State verification sequence Chuỗi kiểm chứng trạng thái W Characterizing sequence Chuỗi đặc trưng 8 Chương 1. GIỚI THIỆU. Đặt vấn đề Hiện nay có rất nhiều hệ thống được đặc tả hoặc mô hình như là một máy hữu hạn trạng thái, đó là các hệ thống reactive (là hệ thống thay đổi hành động, kết quả đầu ra và các điều kiện/ trạng thái tương ứng với các kích thích từ bên trong hoặc bên ngoài nó) [9] 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 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 [5]. Trong luận văn này chúng 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. 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. 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). 9 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. 10 Chương 2. MÁY HỮU HẠN TRẠNG THÁI (FSM) 2.1. Định nghĩa FSM Máy hữu hạn trạng thái (FSM) [7] là một mô hình hành vi sử dụng các trạng thái và chuyển trạng thái. Nó là một mô hình được sử dụng rộng rãi trong mọi lĩnh vực của công nghiệp phần mềm và đặc biệt phổ biến trong thiết kế hệ thống viễn thông, giao thức truyền thông, hệ thống nhúng, và hệ thống điều khiển. Có hai loại máy hữu hạn trạng thái là máy Mealy và máy Moore. Máy Mealy tạo ra output trên chuyển trạng thái và input nhận được còn máy Moore tạo ra output dựa trên chuyển trạng thái (không phụ thuộc vào input nhận được). FSM thường được mô hình hóa như máy Mealy. Máy hữu hạn trạng thái (Mealy machine) [5, 7] là một bộ M = . Trong đó:       S là một 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. Hay nói một cách khác, [4] FSM là mô hình bao gồm: Những yếu tố tĩnh: bao gồm trạng thái (state) và sự chuyển tiếp trạng thái (state transition). Số lượng của những trạng thái là hữu hạn. Sự chuyển tiếp trực tiếp từ trạng thái sang trạng thái ch có thể theo một đường link duy nhất là - . Số lượng các đường link cũng là giới hạn.  Những yếu tố động: bao gồm đầu vào (input) được cung cấp cho FSM và đầu ra (output) được lấy ra từ FSM ở những sự thực hiện động. Cả hai số lượng đầu vào và đầu ra đều là hữu hạn.  Nguồn gốc FSM [7] từ máy tự động hữu hạn (Finite Automata), gồm 5 thành phần (Q, ∑, δ, q0, F). Trong đó: Q là một tập hữu hạn các trạng thái,  ∑ là một tập các ký hiệu được gọi là tập chữ cái ngõ nhập (input alphabet),  δ: Q x ∑ → Q là hàm chuyển trạng thái,  11 q0 ∈ Q là trạng thái ban đầu,  F ⊆ Q là một tập trạng thái kết thúc.  Máy tự động hữu hạn được sử dụng chủ yếu trong phân tích cú pháp cho các ngôn ngữ được đoán nhận. Tại thời điểm ban đầu, nó được giả thiết ở trạng thái khởi đầu q0, với cơ cấu nhập (đầu đọc) của nó đang ở trên ký hiệu đầu tiên bên trái của chuỗi nhập. Trong suốt mỗi lần di chuyển, cơ cấu nhập tiến về phía phải một ký hiệu, như vậy mỗi lần di chuyển sẽ lấy một ký hiệu ngõ nhập.Khi gặp ký hiệu kết thúc chuỗi, chuỗi là được chấp nhận (accepted) nếu máy tự động hữu hạn đang ở trạng thái kết thúc của nó. Ngược lại thì có nghĩa là chuỗi bị từ chối. So sánh mô hình của máy hữu hạn trạng thái và máy tự động hữu hạn ta thấy rằng: FSM có đầu ra (output) còn automata thì không có. Trong luận văn này, các thuật toán áp dụng cho FSM được mô hình theo máy Mealy. 2.2. Biểu diễn FSM 2.2.1. Biểu diễn kiểu liệt kê Cho FSM M = .      Trạng thái ban đầu s0 Tập trạng thái S = {s1, s2..., sn} Tập Inputs I = {i1, i2, ..., in} Tập chuyển trạng thái {δ(ii,sj) = st} với ∀ ii  I và sj, st  S Tập Outputs O = {λ(si,ik) = ot} với si  S; ∀ ik  I; ∀ot  O Ví dụ: FSM M = , trong đó:        S = {A, B, C, D} là tập các trạng thái. I = {0, 1} là tập thông tin đầu vào (inputs). O = {0, 1} là tập thông tin đầu ra (outputs). A là trạng thái ban đầu. δ : S × I → S là hàm chuyển trạng thái. λ : S × I → O là hàm thông tin đầu ra. Tập các nhãn chuyển đổi L = {0/0, 0/1, 1/0} và được mô tả bởi đồ thị sau: 19 Hình 3.1: Đồ thị mô tả FSM G1. 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. Ví dụ: X t chuỗi input 010 cho trạng thái A của FSM G1: λ(A,010) = λ(λ(λ(A,0),1),0) = 000 Với mọi trạng thái khác của FSM G1 thì: λ( ,010) = λ(λ(λ(B,0),1),0) = 001 λ(D,010) = λ(λ(λ(D,0),1),0) = 100 λ(C,010) => Không chấp nhận chuỗi 010 Như vậy: 010 là chuỗi UIO của trạng thái của FSM G1. Vec-tơ đường dẫn (Path Vector), ký hiệu là PV, là một tập hợp các cặp trạng thái của một chuỗi chuyển trạng thái (s1/s1’, ..., si/si’, ..., sk/sk’), với si là trạng thái đầu và sj là trạng thái cuối của một chuyển trạng thái.  Vec-tơ ban đầu (Inital Vectơ), ký hiệu là IV, là một tập các trạng thái đầu của PV, có nghĩa là IV(PV) = (s1, ..., si, ..., sk).  Vec-tơ hiện thời (Current Vector), ký hiệu là CV, là một tập các trạng thái cuối của vec-tơ đường dẫn. Có nghĩa là CV(PV) = (s1’, ..., si’, ..., sk’).  Một vec-tơ đường dẫn được gọi là vec-tơ đơn nhất (Singleton Vector) nếu nó chứa đúng một cặp trạng thái.  Ví dụ: PV = (B/D), vì PV ch có một cặp trạng thái nên PV là một vec-tơ đơn nhất. 20  Một vec-tơ đường dẫn được gọi là vec-tơ đồng nhất (Homogeneous Vector) nếu tất cả các phần tử của vec-tơ hiện thời là như nhau. Ví dụ: PV = (A/B, C/B) ⟹ CV(PV) = (B, B), vì tất cả các phần tử của CV(PV) là giống nhau nên PV là vec-tơ đồng nhất.  Từ một vec-tơ đường dẫn PV, input-output được gán nhãn là a b của một chuyển trạng thái, gọi PV’ là một vec-tơ đường dẫn mới được “tính toán” từ PV và a b: PV’ = pert(PV,a b), được định nghĩa là: PV’ = {si/si”| si” = δ(si’,a) ∧ λ(si’,a) = b ∧ si / si’∈ PV} Hay nói một cách khác, ta có thể tưởng tượng hàm tính PV’ = pert (PV, a b) như là một cạnh từ nút PV tới một nút mới PV’ với nhãn của cạnh là a b. Thêm vào đó, đưa vào PV và một tập các nhãn chuyển đổi L, ta có thể sắp xếp các nút mới L{pert (PV, a/b), ∀a/b ∈ L} trên cùng một cấp. Điều đó có nghĩa là: tất cả các đường dẫn vec-tơ của FSM M có thể được sắp xếp dưới dạng một cây với các cấp 1, 2, 3, ..., ∞. Một cây như vậy được gọi là cây UIO. Tuy nhiên, ta cần cắt t a cây dựa trên một vài điều kiện gọi là điều kiện cắt t a. Sau mỗi lần tính PV’ = pert (PV, a/b) ta kiểm tra các điều kiện bên dưới:  C1: CV(PV’) là một vec-tơ đồng nhất hoặc vec-tơ đơn nhất.  C2: Trên một đường dẫn (path) từ vec-tơ đầu tới PV, tồn tại PV” sao cho PV’⊆ PV”. Trong khi xây dựng cây UIO, nếu một trong 2 điều kiện cắt t a trên thỏa mãn thì PV’ là một vec-tơ đường dẫn kết thúc. Mỗi trạng thái si của FSM có chuỗi UIO nếu và ch nếu cây UIO của FSM M có một vec-tơ đường dẫn đơn nhất. 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. 21 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 D1 hoặc D2 hoặc D3, thì đánh dấu ψ’ là một nút kết thúc. Bước 5: Quay lại bước 2. Ví dụ: Cây UIO của FSM G1 được xây dựng như sau: Ψ=( , , C C, D D) và được “tính toán” bởi việc sử dụng tất cả các thành phần của L như sau: (A/B, B/A) = pert(Ψ, 0/0) (C/D, D/D) = pert(Ψ, 0/1) (A/D, B/B, C/A, D/C) = pert(Ψ, 1 0) Cây UIO có thể được thể hiện dưới dạng đồ họa như sau: gốc là vec-tơ đường dẫn ban đầu, Ψ = (A/A, B/B, C/C, D/D). Từ gốc vẽ 3 cạnh tới các đường dẫn vec-tơ (A/B, B/A), (C/D, D/D), (A/D, B/B, C/A, D/C) với nhãn là các thành phần tương ứng của L là 0 0, 0 1 và 1 0, thể hiện trong Hình 3.2 dưới đây: