BỘ KHOA HỌC VÀ CÔNG NGHỆ ĐẠI HỌC ĐÀ NẴNG
NHIỆM VỤ HỢP TÁC QUỐC TẾ
KHOA HỌC VÀ CÔNG NGHỆ THEO NGHỊ ĐỊNH THƯ
BÁO CÁO TỔNG HỢP
KẾT QUẢ KHOA HỌC CÔNG NGHỆ ĐỀ TÀI
NGHIÊN CỨU KỸ THUẬT PHÂN TÍCH KHẢ NĂNG
KIỂM THỬ PHẦN MỀM VÀ MỞ RỘNG TÍNH NĂNG
CỦA CÔNG CỤ SATAN, THỬ NGHIỆM ỨNG DỤNG TRONG
MÔI TRƯỜNG SCICOS VÀ SIMULINK

Cơ quan chủ trì đề tài: Đại học Đà Nẵng
Chủ nhiệm đề tài: TS. Nguyễn Thanh Bình Đà Nẵng - 2012

i

ĐẠI HỌC ĐÀ NẴNG
__________________
CỘNG HOÀ XÃ HỘI CHỦ NGHĨA VIỆT NAM
Độc lập - Tự do - Hạnh phúc

Đà Nẵng, ngày 26 tháng 12 năm 2011BÁO CÁO THỐNG KÊ
KẾT QUẢ THỰC HIỆN ĐỀ TÀI

I. THÔNG TIN CHUNG
1. Tên đề tài:
Nghiên cứu kỹ thuật phân tích khả năng kiểm thử phần mềm và
mở rộng tính năng của công cụ SATAN, thử nghiệm ứng dụng trong môi trường
Scicos và Simulink

2. Chủ nhiệm đề tài/dự án:
Họ và tên: Nguyễn Thanh Bình
Ngày, tháng, năm sinh: 16/06/1975 Nam/ Nữ: Nam
Học hàm, học vị: Tiến sỹ
Chức danh khoa học: Giảng viên Chức vụ: Trưởng Khoa

TT

Theo kế hoạch Thực tế đạt được Ghi chú
(Số đề nghị
quyết toán)
Thời gian
(Tháng, năm)
Kinh phí
(Tr.đ)
Thời gian
(Tháng, năm)
Kinh phí
(Tr.đ)
1 01/2010 700 05/2010 700 700
2 01/2011 250 11/2011 250 250

c) Kết quả sử dụng kinh phí theo các khoản chi:
Đối với đề tài:
Đơn vị tính: Triệu đồng
Số
TT

Nội dung
các khoản chi
Theo kế hoạch Thực tế đạt được
Tổng SNK
H
Nguồn
khác
Tổng SNKH Nguồn
68,2

68,24 Đoàn ra
140 140 129,045 129,045
5 Đoàn vào
92 92 92 92
6 Chi khác
166 166 170,755 170,755

Tổng cộng 950 950 950 950
- Lý do thay đổi (nếu có):
1. Thiết bị máy móc: Do giá thực tế khi mua cao hơn so với giá lúc dự toán.

iii
2. Đoàn ra: Thay đổi số lượng người tham gia đoàn ra.

3. Các văn bản hành chính trong quá trình thực hiện đề tài/dự án:
(Liệt kê các quyết định, văn bản của cơ quan quản lý từ công đoạn xác định nhiệm vụ, xét chọn,
phê duyệt kinh phí, hợp đồng, điều chỉnh (thời gian, nội dung, kinh phí thực hiện nếu có); văn
bản của tổ chức chủ trì đề tài, dự án (đơn, kiến nghị điều chỉnh nếu có)
Số
TT

Số, thời gian ban
hành văn bản

chủ yếu
đạt được
Ghi
chú*
1 Khoa Công
nghệ Thông
tin, Trường
Đại học Bách
Khoa, Đại
học Đà Nẵng
Khoa Công
nghệ Thông
tin, Trường Đại
học Bách
Khoa, Đại học
Đà Nẵng
Tham gia
nghiên cứu
đề tài và
phát triển
phần mềm
Báo cáo,
bài báo,
đào tạo,
phần mềm

2 Khoa Công
nghệ Thông
tin, Trường
Đại học Công

Viện Đại học
Bách khoa
Grenoble
Phòng nghiên
cứu LCIS,
Viện Đại học
Bách khoa
Grenoble
Cung cấp
công cụ, hỗ
trợ cùng
nghiên cứu
và phát triển
phần mềm
Bài báo,
đào tạo,
phần mềm 5. Cá nhân tham gia thực hiện đề tài, dự án:
(Người tham gia thực hiện đề tài thuộc tổ chức chủ trì và cơ quan phối hợp, không quá 10
người kể cả chủ nhiệm)
Số
TT
Tên cá nhân
đăng ký theo
Thuyết minh

Tên cá nhân
đã tham gia

3 TS. Đặng Văn
Hưng
TS. Đặng Văn
Hưng
Tham gia
nghiên cứu
Báo cáo
4 ThS. Nguyễn
Văn Khang
ThS. Nguyễn
Văn Khang
Tham gia
nghiên cứu
Báo cáo
5 ThS. Trịnh
Công Duy
ThS. Trịnh
Công Duy
Tham gia
nghiên cứu,
viết phần
mềm
Phần mềm

6. Tình hình hợp tác quốc tế:
Số
TT
Theo kế hoạch
(Nội dung, thời gian, kinh phí, địa
điểm, tên tổ chức hợp tác, số

01/2012, Kinh phí
93,439,000đ, Phòng thí
nghiệm LCIS, Valence,
Pháp, 01 đoàn ra, 02 người.
3 Trao đổi về triển khai đề tài,
Kinh phí 62,000,000đ,
09/2010, Phòng thí nghiệm
DATIC, Đà Nẵng, 01 đoàn
vào, 02 người.
Trao đổi về triển khai đề tài,
Kinh phí 64,56,000đ,
12/2010, Phòng thí nghiệm
DATIC, Đà Nẵng, 01 đoàn
vào, 03 người.

4 Tư vấn kết quả thực hiện đề
tài, Kinh phí 30,000,000đ,
12/2011, Phòng thí nghiệm
DATIC, Đà Nẵng, 01 đoàn
vào, 02 người.
Tư vấn kết quả thực hiện đề
tài, Kinh phí 30,000,000đ,
12/2011, Phòng thí nghiệm
DATIC, Đà Nẵng, 01 đoàn
vào, 01 người. 7. Tình hình tổ chức hội thảo, hội nghị:
Số
TT

Thời gian
(Bắt đầu, kết thúc
- tháng … năm)
Người,
cơ quan
thực hiện
Theo kế
hoạch
Thực tế
đạt được
1
Nghiên cứu và đánh giá
tổng quan về các kỹ thuật
phân tích khả năng kiểm
thử hiện có.

1/1/2010 -
30/03/2010

1/1/2010 -
30/03/2010

Đặng Văn Hưng, Khoa
Công nghệ Thông tin,
Trường Đại học Công
nghệ, Đại học Quốc gia
Hà Nội
Nguyễn Thanh Bình,
Phòng thí nghiệm
DATIC.


01/06/2010
-
30/06/2010

01/06/2010
-
30/06/2010

Trịnh Công Duy,
Đặng Thiên Bình,
Nguyễn Thanh Bình,
Phòng thí nghiệm
DATIC.
Michel Delaunay,
Phòng thí nghiệm LCIS.

4
Tìm hiểu các môi trường
hỗ trợ phát triển phần
mềm: Simulink và Scicos.

01/07/2010
-
31/08/2010

01/07/2010
-
31/08/2010


công cụ SATAN để phân
tích khả năng kiểm thử của
các phần mềm phát triển
trên môi trường mã nguồn
mở Simulink.

01/03/2011
-
30/10/2011

01/03/2011
-
30/09/2011

Đặng Thiên Bình,
Nguyễn Thanh Bình,
Phòng thí nghiệm
DATIC.
Michel Delaunay,
Chantal Robach, Phòng
thí nghiệm LCIS.

7
Thử nghiệm ứng dụng
phân tích khả năng kiểm
thử tại phòng thí nghiệm
sản xuất tự động, Trường
Đại học Bách khoa Đà
Nẵng.
01/09/2011

Thực tế
đạt được
1 Công cụ SATAN

Toàn bộ mã
nguồn công cụ
SATAN.
Mã nguồn biên
dịch và thực thi
được.
Tài liệu kỹ thuật
về công cụ
SATAN.

Toàn bộ mã
nguồn công cụ
SATAN.
Mã nguồn biên
dịch và thực thi
được.
Tài liệu kỹ thuật
về công cụ
SATAN.2 Chương trình mở rộng
tính năng công cụ
SATAN phân tích khả
năng kiểm thử các thiết
kế trong môi trường

SATAN phân tích khả
năng kiểm thử các thiết
kế trong môi trường
Simulink.
Thiết kế rõ ràng,
chặt chẽ.
Mã nguồn dễ
bảo trì.
Được kiểm thử
đầy đủ.
Có tài liệu
hướng dẫn sử
dụng và hướng
dẫn cài đặt.
Tích hợp vào
SATAN.

Thiết kế rõ ràng,
chặt chẽ.
Mã nguồn dễ
bảo trì.
Được kiểm thử
đầy đủ.
Có tài liệu
hướng dẫn sử
dụng và hướng
dẫn cài đặt.
Tích hợp vào
SATAN.


trên t
ạp chí hoặc
kỷ yếu hội thảo
khoa học quốc
gia.
thảo khoa học
quốc tế.
01 bài báo đăng
trên tạp chí
khoa học và
công nghệ (6
trường Đại học
Kỹ thuật).

b) Kết quả đào tạo:
Số
TT
Cấp đào tạo, Chuyên
ngành đào tạo
Số lượng
Ghi chú
(Thời gian kết
thúc)
Theo kế
hoạch
Thực tế đạt
được
1 Thạc sỹ 02 04 2010, 2011
2 Tiến sỹ 01 01 2013


Kết quả phân
tích khả năng
kiểm thử
tương ứng với
khó khăn khi
kiểm thử.
3 Thử nghiệm phân
tích khả năng kiểm
thử
2011 Công ty LogiGear,
Việt Nam
Ứng dụng
công cụ
SATAN. 2. Đánh giá về hiệu quả do đề tài, dự án mang lại:
a) Hiệu quả về khoa học và công nghệ:
Nhóm nghiên cứu DATIC phối hợp với nhóm nghiên cứu CTSYS của phòng
thí nghiệm LCIS đã nắm rỏ được tình hình nghiên cứu về lĩnh vực khả năng

ix
kiểm thử trên thế giới, làm chủ và áp dụng được công cụ phân tích khả năng
kiểm thử SATAN, mở rộng công cụ SATAN áp dụng cho các môi trường
Simlink và Scicos. Xây dựng được nhóm nghiên cứu chuyên sâu ở DATIC về
khả năng kiểm thử phần mềm.
b) Hiệu quả về kinh tế xã hội:
Kết quả nghiên cứu của đề tài có thể triển khai để đánh giá khả năng kiểm thử
của các phần mềm được phát triển trong môi trường Simulink hay Scicos tại
các doanh nghiệp.
Thủ trưởng tổ chức chủ trì
(Họ tên, chữ ký và đóng dấu)

TS. Nguyễn Thanh Bình
1

MỤC LỤC
MỤC LỤC 1

DANH MỤC CÁC BẢNG 5

DANH MỤC CÁC HÌNH VẼ 7

MỞ ĐẦU 9

CHƯƠNG 1.

KIỂM THỬ PHẦN MỀM VÀ PHÂN TÍCH TÍNH KHẢ KIỂM
THỬ PHẦN MỀM 13

1.1.

Giới thiệu 13

1.1.1.

Kiểm chứng và hợp thức hóa 14



Các phương pháp phân tích tính khả kiểm thử phần mềm 22

1.4.1.

Phương pháp phân tích tính khả kiểm thử truyền thống 23

1.4.2.

Phương pháp phân tích tính khả kiểm thử hướng đối tượng 35

1.5.

Tổng kết chương 1 43

CHƯƠNG 2.

PHÂN TÍCH TÍNH KHẢ KIỂM THỬ VỚI SATAN 44

2.1.

Giới thiệu 44

2.2.

Đồ thị truyền tin 45

2

2.3.


2.6.2.

Mô-đun In-Mac 62

2.6.3.

Mô-đun lõi SATAN 63

2.6.4.

Thư viện In-Mac 65

2.7.

Tổng kết chương 2 68

CHƯƠNG 3.

MÔI TRƯỜNG SCICOS VÀ MÔI TRƯỜNG SIMULINK 69

3.1.

Giới thiệu 69

3.2.

Môi trường SCICOS 69

3.2.1.


CHƯƠNG 4.

MỞ RỘNG CÔNG CỤ SATAN CHO CÁC MÔI TRƯỜNG
SIMULINK VÀ SCICOS 78

4.1.

Giới thiệu 78

4.2.

Thiết kế mô-đun Simulink/Scicos2mac 79

4.2.1.

Thiết kế tổng thể 79

4.2.2.

Thiết kế chi tiết 80

4.2.3.

Cài đặt 86

3

4.3.


4.5.2.

Phân tích tính khả kiểm thử của các mô hình SIMULINK 100

4.6.

Tổng kết chương 4 110

CHƯƠNG 5.

PHÂN TÍCH TÍNH KHẢ KIỂM THỬ CÁC MÔ HÌNH MÁY
TRẠNG THÁI HỮU HẠN 111

5.1.

Giới thiệu 111

5.2.

Ngữ cảnh 112

5.2.1.

Hệ thống phản ứng 112

5.2.2.

Hệ thống phản ứng đồng bộ 114

5.2.3.


5.4.1.

Định nghĩa 123

5.4.2.

Thảo luận 124

5.5.

Độ đo tính khả kiểm thử dựa trên máy trạng thái hữu hạn 125

5.5.1.

Chuỗi Markov 125

5.5.2.

Độ đo tính khả kiểm thử 127

5.6.

Thử nghiệm 130

4

5.6.1.

Tính khả kiểm thử của B01_AUTOMATON 131
5

DANH MỤC CÁC BẢNG
Bảng 1.1 Phân loại các định nghĩa tính khả kiểm thử 21
Bảng 1.2. Các luật tính khả năng điều khiển các phép gán 27
Bảng 4.1. Sự tương quan giữa SIMULINK/SCICOS và SATAN 80
Bảng 4.2. Các API được sử dụng 86
Bảng 4.3. Danh sách các kiểu SATAN được xây dựng 88
Bảng 4.4. Các tệp tin chứa kết quả phân tích tính khả kiểm thử 92
Bảng 4.5. Kết quả tính khả kiểm thử của hệ thống Pil-dem 98
Bảng 4.6. Kết quả tính khả kiểm thử của hệ thống GRS 99
Bảng 4.7. Thông tin về hệ thống re_gy_2sw_anno 101
Bảng 4.8. Kết quả phân tích trong lớp 1 (luồng 1) 102
Bảng 4.9. Kết quả phân tích trong lớp 2 (luồng 2) 102
Bảng 4.10. Kết quả phân tích trong lớp 2 (luồng 4) 102
Bảng 4.11. Kết quả phân tích trong lớp 3 (luồng 3) 102
Bảng 4.12. Hệ thống S_TEST_QUATERNION_SIGN 103
Bảng 4.13 Kết quả phân tích trong lớp 1 (luồng 1) 103
Bảng 4.14 Kết quả phân tích trong lớp 2 (luồng 2) 104
Bảng 4.15. Kết quả phân tích tính khả kiểm thử theo Multi-Clue 104
Bảng 4.16. Hệ thống B23_NAVIGATION_PROPAGATION 105
Bảng 4.17. Kết quả phân tích trong lớp 1 (luồng 8) 106
Bảng 4.18. Kết quả phân tích trong lớp 2 (luồng 7) 106
Bảng 4.19. Kết quả phân tích trong lớp 3 (luồng 5) 106
Bảng 4.20. Kết quả phân tích trong lớp 3 (luồng 2) 107
Bảng 4.21. Kết quả phân tích trong lớp 4 (luồng 1) 107
Bảng 4.22. Kết quả phân tích trong lớp 5 (luồng 9) 107
6

Hình 4.4. Thuật toán system2dot 84
Hình 4.5. Thuật toán blocks_to_dot_nodes 85
Hình 4.6. Thuật toán lines_to_dot_egdes 85
Hình 4.7. ITG của phép toán AND_2 90
Hình 4.8. Mô hình mô-đun Out-Mac 93
Hình 4.9. Thuật toán xử lý kết quả tính khả kiểm thử theo Start-Small 94
8

Hình 4.10. Minh họa kết quả tính khả kiểm thử theo Start-Small 95
Hình 4.11. Thuật toán xử lý kết quả tính khả kiểm thử theo Multi-Clue 96
Hình 4.12. Minh họa kết quả tính khả kiểm thử theo Multi-Clue 97
Hình 4.13. Mô hình SCICOS của hệ thống Pil-dem 98
Hình 4.14. Mô hình SCICOS của hệ thống GRS 99
Hình 4.15. Mô hình Simulink của hệ thống re_gy_2sw_anno 101
Hình 4.16. Cây xác định lỗi theo chiến lược Multi-Clue 104
Hình 4.17. Cây xác định lỗi theo chiến lược Multi-Clue 109
Hình 5.1. Hệ thống phản ứng 113
Hình 5.2. Hệ thống tại thời điểm k 115
Hình 5.3. B01_AUTOMATON trong dự án MSU 131
Hình 5.4. B01_AUTOMATON được vẽ lại 132
Hình 5.5. B01_AUTOMATON với chuyển tiếp T10 134

9

MỞ ĐẦU
Các hệ thống phần mềm được phát triển ngày càng phức tạp. Sự phức
tạp này còn cao hơn đối với các hệ thống điều khiển và các hệ thống nhúng
trong các thiết bị công nghiệp, như máy bay, vệ tinh… Các hoạt động kiểm
thử đóng vai trò rất quan trọng nhằm đảm bảo chất lượng của các hệ thống
phần mềm. Các hoạt động này phải được tính đến trong suốt tiến trình phát

Nghiên cứu về tính khả kiểm thử phần mềm đã và đang được thực hiện
trong lĩnh vực phần cứng, cũng như phần mềm. Trong đó, công cụ SATAN
(System’s Automatic Testability ANalysis) đã được thiết kế và phát triển bởi
phòng thí nghiệm LCIS (Laboratoire de Conception et d’Intégration de
Systèmes), đã có nhiều ứng dụng trong phân tích tính khả kiểm thử phần mềm
của các hệ thống phần mềm luồng dữ liệu được phát triển trong các môi
trường như SCADE và GALA. Trong khuôn khổ hợp tác với nhóm nghiên
cứu của phòng thí nghiệm LCIS, chúng tôi nghiên cứu về công cụ SATAN và
đề xuất sự mở rộng ứng dụng của công cụ trong các môi trường phát triển
phần mềm SCICOS và SIMULINK. Phương pháp phân tích tính khả kiểm thử
này gồm bốn hoạt động cơ bản:
− Xây dựng mô hình tính khả kiểm thử, nhằm biểu diễn luồng thông
tin trong hệ thống phần mềm.
11

− Tính toán các luồng thông tin dựa trên mô hình tính khả kiểm thử.
− Áp dụng các chiến lược kiểm thử nhằm giảm số luồng thông tin.
− Tính toán các độ đo tính khả kiểm thử.
Hơn nữa, các hệ thống phần mềm có thể được thiết kế gồm hai phần:
phần tính toán và phần điều khiển. Phần tính toán thường được biểu diễn bởi
mô hình luồng dữ liệu. Phần điều khiển thường được biểu diễn bởi các mô
hình máy trạng thái hữu hạn, như STATEFLOW trong SIMULINK. Sự mở
rộng của công cụ SATAN chỉ cho phép phân tích tính khả kiểm thử của các
mô hình luồng dữ liệu trong các môi trường SCICOS và SIMULINK. Trong
nghiên cứu này, chúng tôi đề xuất phương pháp phân tích tính khả kiểm thử
của các mô hình máy trạng thái hữu hạn.
Báo cáo này được tổ chức gồm năm chương.
Trong chương 1, chúng tôi trình bày vai trò, mục đích và các khái niệm
cơ bản của kiểm thử phần mềm và phân tích tính khả kiểm thử phần mềm.
Trong chương này, chúng tôi cũng trình bày tổng quan về các nghiên cứu

tả…) và kỹ thuật kiểm thử. Việc phân tích thực thể phần mềm có thể được
dựa trên các mô tả khác nhau của phần mềm, như luồng điều khiển, luồng dữ
liệu, đặc tả chức năng và thậm chí là mã nguồn.
Các kỹ thuật kiểm thử được sử dụng phổ biến gồm kiểm thử cấu trúc và
kiểm thử chức năng. Phương pháp phân tích và đánh giá độ đo tính khả kiểm
thử gắn liền với kiểm thử cấu trúc dựa trên cấu trúc bên trong của phần mềm,
nó thường mang lại nhiều thông tin chi tiết hơn so với phương pháp phân tích
và đánh giá độ đo tính khả kiểm thử gắn liền với kiểm thử chức năng chỉ dựa
trên đặc tả chức năng.
14

Trong chương này, trước khi trình bày các phương pháp phân tích tính
khả kiểm thử, chúng tôi trình bày ngắn gọn về kiểm chứng, hợp thức hóa và
kiểm thử phần mềm. Sau đó, chúng tôi giới thiệu các định nghĩa khác nhau về
tính khả kiểm thử phần mềm cũng như các phương pháp phân tích và đánh
giá độ đo tính khả kiểm thử phần mềm.
1.1.1. Kiểm chứng và hợp thức hóa
Chất lượng phần mềm ảnh hưởng bởi tất cả các hoạt động của tiến trình
phát triển, tuy nhiên, nó đặc biệt liên quan đến hai hoạt động: kiểm chứng
(verification) và hợp thức hóa (validation) (Hình 1.1).
Hình 1.1. Kiểm chứng và hợp thức hóa trong mô hình phát triển V
− Kiểm chứng cho phép thiết lập sự tương quan giữa phần mềm và
đặc tả của nó. Trong tiến trình phát triển, kiểm chứng đảm bảo
rằng phần mềm sau mỗi giai đoạn phát triển đạt các điều kiện đặt
ra để chuyển sang giai đoạn tiếp theo.
Đặc tả
Thiết kế
tổng thể
Thiết kế
chi tiết