Tiến Sĩ Nghiên cứu khả năng chuyển đổi giữa các đặc tả hình thức và ứng dụng trong kiểm chứng phần mềm

Giới thiệu
Trong ngành công nghiệp phần mềm, việc đảm bảo chất lượng phần mềm là
một vấn đề quan trọng nhằm đảm bảo tính đúng đắn, giảm tỉ lệ lỗi, tìm khiếm
khuyết, v.v. của phần mềm trước khi đưa vào sử dụng [1]. Vấn đề này không chỉ
là yếu tố quyết định thành công của các công ty phần mềm trong việc nâng cao
uy tín và giảm chi phí bảo trì mà nó còn góp phần quan trọng tới sự thành công
của khách hàng. Vấn đề này càng cấp thiết hơn khi phát triển các phần mềm
nhúng/điều khiển. Lỗi trong phần mềm có thể gây ra thiệt hại không mong
muốn cho người sử dụng phần mềm hoặc có thể ảnh hưởng nghiêm trọng tới
tình hình kinh tế, chính trị, an ninh của quốc gia. Ví dụ, sự cố Therac-25 vào
khoảng giữa tháng 6 năm 1985 và tháng giêng năm 1987. Nguyên nhân của sự
cố này được xác định là do tương tác giữa các thành phần của hệ thống và lỗi
chương trình song song khi thực hiện một chức năng quan trọng của chương
trình [2, 3]. Sự cố này được xem như là tai nạn bức xạ tồi tệ nhất trong lịch sử
35 năm phát triển của ngành y học kể từ năm 1985 [2, 3]. Hơn nữa, trong tương
lai các tiện ích phục vụ cho con người đang dần được thay thế bởi các hệ thống
nhúng/điều khiển. Nên các hệ thống này sẽ trở nên phổ biến.
Để đảm bảo chất lượng phần mềm, hầu hết các công ty hiện nay sử dụng
các kỹ thuật kiểm thử trong đó chủ yếu là kỹ thuật kiểm thử hộp đen [1]. Tuy
nhiên, các kỹ thuật kiểm thử chỉ có thể phát hiện ra lỗi/khiếm khuyết chứ không
chỉ ra được phần mềm không còn lỗi. Một số dự án phần mềm hiện nay yêu cầu
phải chứng minh được tính đúng đắn của chương trình (đảm bảo rằng chương
trình không còn lỗi) trước khi đưa vào sử dụng. Điều này có nghĩa là chỉ áp
dụng phương pháp kiểm thử là chưa đủ để đảm bảo chất lượng phần mềm,
đặc biệt đối với những phần mềm yêu cầu tính đúng đắn và chất lượng cao
như: hệ thống điều khiển máy bay/tên lửa, hệ thống giám sát hạt nhân, v.v.
Một trong những phương pháp nhằm chứng minh tính đúng đắn của chương
trình đang được quan tâm nghiên cứu và áp dụng vào thực tế là kiểm chứng mô
1Chương 1. Giới thiệu
hình (model checking) [4]. Ý tưởng của phương pháp này là xây dựng mô hình
của hệ thống và các thuộc tính cần kiểm tra bằng các công cụ toán học và chứng
minh tự động tính đúng đắn của nó dựa trên mô hình này. Tuy nhiên, một trong
những hạn chế lớn nhất của phương pháp này là vấn đề "bùng nổ không gian
trạng thái" khi áp dụng vào các hệ thống có kích thước lớn [4]. Phương pháp
kiểm chứng giả định-đảm bảo (Assume-Guarantee Verification) [5] được xem là
giải pháp tiềm năng để giải quyết vấn đề trên cho các hệ thống dựa trên thành
phần. Phương pháp này được xây dựng dựa trên phương pháp kiểm chứng mô
hình kết hợp với kỹ thuật chia để trị nhằm mục đích chia nhỏ công việc kiểm
chứng cả hệ thống thành các bài toán con để kiểm chứng các thành phần riêng
biệt. Bằng cách tiếp cận này, bài toán bùng nổ không gian trạng thái hứa hẹn
sẽ được giải quyết. Để áp dụng phương pháp này, chúng ta cần cài đặt công cụ
hỗ trợ nhằm mục tiêu ứng dụng nó trong thực tế. Mặc dù phương pháp này
được đề xuất bởi Dimitra Giannakopoulou [5] và đã có công cụ hỗ trợ [6] nhưng
công cụ này không được công bố. Một công cụ hỗ trợ phương pháp này có tên
là AGTool 1 đã được cài đặt bởi nhóm nghiên cứu [7]. AGTool cho phép người
dùng sinh ra một giả thiết kiểm chứng để kiểm tra một thành phần và cả hệ
thống có thỏa mãn một thuộc tính hay không.
Các thành phần đầu vào của AGTool được biểu diễn dưới dạng một loại
máy hữu hạn trạng thái (LTS) và được truyền vào AGTool bằng cách liệt kê các
hàm chuyển trạng thái (trong luận văn này được gọi là dạng biểu diễn liệt kê (LF)).
Cách biểu diễn này yêu cầu phải chuẩn bị các thành phần đầu vào một cách chi
tiết, tốn nhiều thời gian và dễ gây ra lỗi. Bên cạnh đó, dạng biểu diễn liệt kê
không được ứng dụng rộng rãi như một số ngôn ngữ mô hình hóa khác, ví dụ
như FSP. Vì vậy, AGTool gặp khó khăn trong việc tương tác và sử dụng lại đặc
tả của các chương trình kiểm chứng phần mềm khác như LTSA 2 [8]. Để giải
quyết những vấn đề này, AGTool đã được nâng cấp lên phiên bản mới có tên gọi
là GUI-AGTool 3 bởi [9, 10]. GUI-AGTool cung cấp giao diện người dùng hỗ trợ
nhập liệu trực quan và dễ dàng. Bên cạnh đó, GUI-AGTool cũng có khả năng
tương tác với các kiểu dữ liệu LF, FSP đơn giản. Những cải tiến này là một bước
tiến quan trọng trong quá trình đưa AGTool tiếp cận với thực tế và mở ra một
tiềm năng ứng dụng mới. Tuy nhiên, GUI-AGTool vẫn còn tồn tại nhiều vấn đề
cần được cải tiến. GUI-AGTool cần có khả năng sử dụng được kiểu dữ liệu FSP
hoàn chỉnh. Kết quả của quá trình chuyển đổi từ LF sang FSP cần được tối ưu
nhiều hơn.
Mục tiêu của luận văn này là đưa GUI-AGTool trở thành một công cụ làm
việc được với ngôn ngữ FSP hoàn chỉnh. Ý tưởng cơ bản của luận văn là nghiên
1
http://uet.vnu.edu.vn/~hungpn/AGTools/
2
http://www.doc.ic.ac.uk/ltsa/
3
http://uet.vnu.edu.vn/~hungpn/GUI-AGTool/
2Chương 1. Giới thiệu
cứu đặc tả hoàn chỉnh của FSP và tích hợp GUI-AGTool với công cụ LTSA.
Những cải tiến này sẽ biến GUI-AGTool trở thành một công cụ hiệu quả và có
tính tương tác rộng rãi hơn trong thực tế.
Cấu trúc của luận văn được chia thành sáu phần. Chương đầu tiên giới
thiệu về vai trò của kiểm chứng phần mềm, công cụ hỗ trợ và bài toán cần giải
quyết trong luận văn này. Tiếp theo, chương 2 trình bày các khái niệm cơ bản
nhằm phục vụ luận văn. Chương này bao gồm các khái niệm về máy hữu hạn
trạng thái, dẫn xuất, ghép nối song song, thuộc tính an toàn, đặc tả của ngôn ngữ
FSP, ngôn ngữ lập trình hàm OCaml, Ocamllex và Ocamlyacc. Công cụ kiểm
chứng phần mềm dựa thành phần AGTool được mô tả ở chương 3. Những vấn
đề còn tồn tại của công cụ kiểm chứng AGTool được nêu ra trong chương này.
Các phương pháp chuyển đổi giữa các dạng biểu diễn của LTS được trình bày
trong chương 4. Trong chương này đưa ra hai phương pháp chuyển đổi qua lại
giữa hai cách biểu diễn của LTS là FSP và LF. Kết quả sau khi làm thực nghiệm
bằng công cụ GUI-AGTool được trình bày ở chương 5. Cuối cùng, chương 6 tóm
tắt kết quả đạt được sau khi hoàn thành luận văn, những vấn đề cần khắc phục
và hướng phát triển trong tương lai.






Mục lục
1 Giới thiệu 1
2 Kiến thức cơ bản 4
2.1 Labeled Transition System (LTS) . 4
2.2 Các phương pháp biểu diễn LTS . 5
2.2.1 Phương pháp liệt kê 6
2.2.2 FSP 6
2.3 Dẫn xuất . 7
2.4 Ghép nối song song . 7
2.5 LTS an toàn và thuộc tính an toàn . 8
2.6 Tính thỏa mãn 9
2.7 Đặc tả ngôn ngữ FSP 9
2.7.1 Định nghĩa FSP . 10
2.7.2 Các định danh 10
2.7.3 Nhãn hành động 11
2.7.4 Const, Range, Set 12
2.7.5 Định nghĩa tiến trình 12
2.7.6 Tiến trình kết hợp 13
2.7.7 Tham số . 14
2.7.8 Phép gán lại nhãn và phép ẩn . 15
2.7.9 Property, Progress và Menu 16
2.7.10 Biểu thức . 16
viiMỤC LỤC
2.8 Ngôn ngữ lập trình hàm OCaml . 17
2.8.1 Đặc trưng của OCaml . 17
2.8.2 Cú pháp và ngữ nghĩa . 18
2.9 OCamllex và OCamlyacc 23
2.9.1 OCamllex 23
2.9.2 OCamlyacc . 23
3 AGTool 25
3.1 Giới thiệu AGTool 25
3.2 Hạn chế của AGTool 27
4 Chuyển đổi giữa các dạng biểu diễn của LTS 28
4.1 Chuyển đổi FSP sang LF 29
4.1.1 Ý tưởng . 29
4.1.2 Thiết kế . 32
4.1.3 Phân tích đánh giá . 32
4.2 Chuyển đổi LF sang FSP 33
4.2.1 Ý tưởng . 33
4.2.2 Phân tích đánh giá . 36
5 Thực nghiệm 37
5.1 Cài đặt chương trình 37
5.2 Giới thiệu về chương trình . 37
5.3 Thực nghiệm . 39
5.4 Đánh giá thực nghiệm . 43
6 Kết luận 44
Tài liệu tham khảo 46
viiiDanh sách hình vẽ
2.1 Ví dụ của LTS . 5
2.2 Phương pháp biểu diễn liệt kê của LTS 6
2.3 Ví dụ của LF 6
2.4 Ví dụ của FSP . 7
2.5 Ghép nối song song giữa INPUT và OUTPUT 8
2.6 Biểu diễn LTS của thuộc tính an toàn Safety Property 9
2.7 Ví dụ định nghĩa hằng số 9
2.8 Ví dụ định nghĩa danh sách đối số . 10
2.9 Định nghĩa FSP 10
2.10 Định nghĩa các định danh 11
2.11 Định nghĩa các chữ hoa, thường 11
2.12 Định nghĩa nhãn hành động 11
2.13 Định nghĩa tập các nhãn hành động 12
2.14 Định nghĩa Const, Range, Set 12
2.15 Định nghĩa tiến trình . 13
2.16 Định nghĩa tiến trình địa phương . 14
2.17 Định nghĩa thành phần tuần tự . 15
2.18 Định nghĩa thành phần tuần tự . 15
2.19 Định nghĩa tham số . 16
2.20 Định nghĩa phép gán lại nhãn . 16
2.21 Định nghĩa phép ẩn . 17
2.22 Định nghĩa Property . 17
2.23 Định nghĩa Progress . 18
ixDANH SÁCH HÌNH VẼ
2.24 Định nghĩa Menu . 18
2.25 Định nghĩa biểu thức . 19
2.26 Định nghĩa biểu thức (tiếp) . 20
2.27 Định nghĩa biểu thức (tiếp) . 21
2.28 Ví dụ khai báo hàm 21
2.29 Ví dụ gọi hàm . 21
2.30 Ví dụ hàm mức cao 22
2.31 Ví dụ hàm nặc danh . 22
2.32 Ví dụ hàm đệ quy . 22
2.33 Cấu trúc lệnh của so sánh mẫu . 22
2.34 Ví dụ so sánh mẫu 22
2.35 Cấu trúc tập tin đặc tả từ vựng . 23
2.36 Ví dụ tập tin đặc tả từ vựng . 24
2.37 Cấu trúc tập tin đặc tả cú pháp . 24
3.1 Mô hình công cụ kiểm chứng AGTool . 25
3.2 Thành phần đầu vào của AGTool 26
3.3 Kết quả được sinh ra bởi AGTool 26
4.1 Kiến trúc của GUI-AGTool 28
4.2 Cấu trúc thành phần chuyển đổi từ FSP sang LF . 29
4.3 FSP M . 29
4.4 Mô hình FSP Compiler 32
4.5 Cấu trúc thành phần chuyển đổi từ LF sang FSP . 33
5.1 Giao diện chính của GUI-AGTool 38
5.2 Giao diện thể hiện giả định sinh ra bởi GUI-AGTool . 39
5.3 Ví dụ FSP đầu vào của AGTool . 40
5.4 LTS của thành phần M1 . 41
5.5 LTS của thành phần M2 . 41
5.6 LTS của thành phần P 41
x