ĐẠ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:
- Xem thêm -