Tóm tắt Luận văn Xây dựng công cụ sinh dữ liệu thử tự động cho chương trình Java
1
MỞ ĐẦU
1. Lý do chọn đề tài
Phần mềm hiện nay được sử dụng rộng rãi trong đời sống, công
việc, nhiều lĩnh vực khoa học, kinh tế và xã hội. Vì vậy, việc đảm
bảo rằng phần mềm đáp ứng mong muốn của người sử dụng là rất
quan trọng. Kiểm thử phần mềm là một trong những hoạt động cơ
bản nhằm đảm bảo chất lượng phần mềm.
Việc phát triển phần mềm ngày càng được chuy n nghiệp h a
Các phần mềm được phát triển ngày càng c quy mô lớn Y u cầu
đảm ảo chất lượng phần mềm là một trong những mục ti u quan
trong nhất, đ c biệt trong một số lĩnh vực như y hoa, ng n hàng,
hàng hông Việc iểm thử, iểm chứng phần mềm một cách thủ
công ch đảm ảo được phần nào chất lượng của phần mềm Vì vậy
rất nhiều các t chức, công ty đã nghi n cứu và phát triển các l
thuyết c ng như công cụ để iểm chứng, iểm thử phần mềm một
cách tự động.
Một số lợi ích có thể kể đến của kiểm thử tự động như: cải thiện
hiệu quả công việc, cải thiện tính chính xác, cải thiện chất lượng
kiểm thử và chất lượng của phần mềm. Tại các doanh nghiệp tư nhân
hiện tại, công việc kiểm thử phần mềm đơn vị (unit test) thường
được các lập trình viên thực hiện ngay trong quá trình viết mã nguồn
của chương trình Vì vậy dẫn đến một số vấn đề như sau:
-
-
Không đảm bảo được tính khách quan.
Các lập trình vi n thường khó sử dụng các kỹ thuật kiểm thử
hộp trắng vì hông đủ chi phí thời gian.
Hiện tại trong các dự án mà tôi đang tham gia, ngôn ngữ lập trình
chủ yếu được sử dụng là Java. Ngoài ra,trong các ngôn ngữ lập trình
2
hiện đại ngày nay, Java là ngôn ngữ lập trình ph biến trong suốt 13
năm qua [1]
Vì những l do tr n, tôi đề xuất chọn đề tài luận văn cao học: “X y
dựng công cụ sinh dữ liệu thử tự động cho chương trình Java”
2. Mục đích và ý nghĩa đề tài
a. Mục đích
-
Xây dựng công cụ sinh dữ liệu kiểm thử tự động cho chương
trình nguồn Java. Nhằm mục đích thực hiện việc kiểm thử
hộp trắng cho kiểm thử đơn vị một cách tự động và khoa
học Hướng đến mục tiêu giảm chi phí về thời gian và tài
chính khi thực hiện công việc kiểm thử cho các lập trình
viên/kiểm thử viên.
-
Tìm hiểu về các thách thức g p phải trong quá trình sinh dữ
liệu thử tự động, từ đ đề xuất và cài đ t giải pháp để giải
quyết các thách thức này.
b. Ý nghĩa khoa học
-
-
-
Nghiên cứu về các kỹ thuật kiểm thử hộp trắng.
Nghiên cứu về lý thuyết về tính thoả được.
Xây dựng công cụ tự động sinh dữ liệu cho chương trình
Java đảm bảo tiêu chí bao phủ lộ trình và tối ưu thời gian
thực thi.
c. Ý nghĩa thực tiễn
-
-
-
Giảm thời gian và chi phí cho việc kiểm thử hộp trắng của
các lập trình viên khi thực hiện kiểm thử đơn vị.
Dữ liệu thử tự động mang tính hách quan hơn, hông ị
phụ thuộc vào góc nhìn và kinh nghiệm của người lập trình.
Kiểm tra được các lỗi tiềm ẩn trong mã nguồn.
3
3. Mục tiêu và nhiệm vụ
a. Mục tiêu
Xây dựng công cụ sinh dữ liệu tự động cho chương trình Java
đảm bảo tiêu chí bao phủ lộ trình.. Các mục tiêu cụ thể như sau:
-
-
-
Nghiên cứu về các phương pháp iểm thử hộp trắng.
Nghiên cứu về phương pháp giải các ràng buộc (SMT [2]).
Nghiên cứu về các giải pháp sinh dữ liệu thử tự động cho
chương trình Java và những thách thức hiện nay.
-
Xây dựng công cụ sinh dữ liệu thử cho chương trình Java
b. Nhiệm vụ
Để đạt được những mục tiêu trên, nhiệm vụ đ t ra của đề tài là:
-
Nghiên cứu lý thuyết kiểm thử hộp trắng, tập trung vào các
lý thuyết xây dựng tập dữ liệu kiểm thử.
Nghiên cứu về lý thuyết về tính thoả được.
Nghiên cứu và áp dụng kỹ thuật tối ưu h a để tối ưu thời
gian thực thi.
-
-
4. Đối tƣợng và phạm vi nghiên cứu
Luận văn tập trung vào nghiên cứu các đối tượng và phạm vi
sau:
-
-
Cấu trúc chương trình Java
Lý thuyết về tính thoả được của các bộ SMT và cách áp
dụng để giải các ràng buộc.
-
Phân tích, thiết kế và cài đ t ứng dụng sinh dữ liệu thử cho
chương trình Java
5. Phƣơng pháp nghiên cứu
a. Phương pháp lý thuyết
Tiến hành thu thập và nghiên cứu các tài liệu có liên quan
đến đề tài.
4
Nghiên cứu lý thuyết về thực thi ký hiệu và lý thuyết về tính
thỏa được.
Nghiên cứu về kiểm thử đơn vị và cách thực hiện.
Nghiên cứu các phương pháp tối ưu h a các đường thực thi.
b. Phương pháp thực nghiệm
Nghiên cứu về phương pháp thực thi ký hiệu và các công cụ
hỗ trợ thực thi ký hiệu hiện nay.
Nghiên cứu đề xuất giải pháp tối ưu các đường thực thi trong
quá trình thực hiện thực thi ký hiệu.
5. Kết luận
a. Kết quả của đề tài
Thứ nhất, tìm hiểu về cách xây dựng và hoạt động của và
phương pháp sinh dữ liệu kiểm thử tự động cho ngôn ngữ
Java c ng như nghi n cứu về các thách thức hiện nay.
Thứ hai, đề xuất và cài đ t giải pháp tối ưu trong việc sinh
dữ liệu thử tự động nhằm tối ưu hóa thời gian nhưng vẫn
đảm bảo tính đúng đắn, toàn vẹn và khả năng ao phủ của bộ
dữ liệu thử tự động.
b. Hướng phát triển của đề tài
Trong quá trình nghiên cứu, bộ SMT Choco không cho kết
quả tốt như các ộ SMT hác như Z3 hay CVC3 Vì vậy, trong thời
gian tới chúng tôi sẽ tiếp tục nghiên cứu và triển khai tích hợp các bộ
SMT mới và có khả năng hỗ trợ nâng cấp tốt hơn vào trong chương
trình sinh dữ liệu kiểm thử
5
CHƢƠNG 1
CƠ SỞ LÝ THUYẾT
1.1. Tổng quan về kiểm thữ phần mềm
1.1.1. Các bước kiểm thử
1.1.2. Các mức kiểm thử
1.1.3. Các kỹ thuật kiểm thử phần mềm
1.2. Lý thuyết về tính thỏa đƣợc
Tính thỏa mãn là một trong những vấn đề quan trọng nhất
của ngành khoa học máy tính. Các vấn đề cần tính thỏa mãn được
ứng dụng trong cả phát triển phần cứng c ng như phần mềm, đ c
biệt là kiểm định phần cứng, kiểm thử, lập lịch, đồ thị.
Trong các lĩnh vực nói trên, nhiều các ứng dụng được xây
dựng dựa trên việc tạo ra các công thức tiền tố và việc chứng minh
tính hợp lệ của chúng. Cho dù hai thập niên gần đ y, việc chứng
minh tính hợp lệ của các định lý, biểu thức tiền tố có những tiến bộ
đáng ể, tuy nhiên, không phải công thức nào c ng c thể chứng
minh một cách tự động được. Lý do của vấn đề này là bởi lẽ nhiều
công thức hông quan t m đến tính khả thi trong trường hợp t ng
quát mà ch được quan tâm trong một lý thuyết nền tảng. Việc
nghiên cứu tính khả thi của các công thức trong một lý thuyết nền
tảng được gọi là các lý thuyết module về tính thỏa được
(Satisfiability Modulo Theories hay SMT) và các công cụ để chứng
minh một cách tự động các tính khả thi của những vẫn đề SMT được
gọi là bộ giải SMT (SMT solver).
Trên thực tế, việc xây dựng và sử dụng các bộ giải SMT
được phát triển khá sớm, từ đầu những năm 1980 [9] Tại thời điểm
đ , một số bộ giải được xây dựng bởi Greg Nelson và Derek Oppent
tại trường đại học Stanford , Robert Shostak tại SRI, và Robert
6
Boyer và J Moore tại trường đại học ở Texas Đến cuối những năm
1990, việc nghiên cứu SMT hiện đại dựa trên lợi thế của công nghệ
SAT đã x y dựng nhiều bộ giải SMT tiến bộ hơn
Như đã đề cập ở trên, trong khuôn kh đồ án, việc đánh giá
về tính đúng đắn, các nghiên cứu về thuật giải của từng bộ giải sẽ
hông được đề cập đến. Vấn đề được đ t ra ở đ y là ết quả của bộ
giải nào sẽ được đưa ra sớm nhất. Hiện nay, có rất nhiều các bộ giải
như A solver, Boolector, CVC3, OpenSMT, Yices, Z3… Do yêu
cầu của hệ thống là phải đưa ra được giá trị thỏa mãn (nếu bài toán
SMT đ c thỏa mãn) nên bộ giải hệ thống sử dụng phải hỗ trợ chức
năng này Ngoài ra hệ thống sử dụng đầu vào theo chuẩn của SMT-
Lib và ngắt thời gian giải một bài toán (trong trường hợp bài toán
cần thời gian giải quá lớn), do đ , ộ giải cần phải có hỗ trợ những
chức năng này hi hoạt động. Từ những yêu cầu đ , hai ộ giải là
Yices của SRI International và Choco thuần Java đã được lựa chọn
trong JPF. Hai bộ giải này tuy có cấu trúc hác nhau nhưng cùng
được dựa trên thuật giải DPLL (Davis-Putnam-Logemann-
Loveland).
1.3. Thực thi ký hiệu
Trong hoạt động kiểm thử phần mềm, các ca kiểm thử
thường được tạo ra một cách thủ công, gây tốn kém về chi phí c ng
như thời gian để hoàn thành công đoạn này. Thực thi ký hiệu
(Sym olic execution) được biết đến là một kỹ thuật n i tiếng với khả
năng tự động sinh những bộ ca kiểm thử c độ bao phủ cao với các
tiêu chí kiểm thử nhằm phát hiện những lỗi sâu trong các hệ thống
phần mềm phức tạp. Trong mục này sẽ trình bày các vấn đề t ng
quan và một số kết quả của các nghiên cứu gần đ y về kỹ thuật thực
thi ký hiệu, đưa ra những thách thức cần giải quyết trong lĩnh vực
7
này như: sự bùng n đường thực thi của chương trình, hả năng giải
các ràng buộc, mô hình hóa bộ nhớ, các vấn đề về tương tranh, đồng
thời c ng tập trung vào ph n tích và đề xuất giải pháp để sinh ra dữ
liệu kiểm thử cho chương trình Java một cách tự động.
Hiện nay c rất nhiều công cụ nền tảng phục vụ cho hoạt
động iểm thử phần mềm như JUnit cho ngôn ngữ Java, NUnit,
VSUnit cho NET để thực thi các ca iểm thử mức đơn vị Tuy
nhi n, các công cụ iểm thử này hông hỗ trợ việc sinh tự động các
ca iểm thử đơn vị Viết các ca iểm thử là một công việc n ng nhọc
và tốn nhiều công sức C nhiều phương pháp hác nhau hỗ trợ việc
sinh tự động các ca iểm thử giúp giảm chi phí và thời gian thực hiện
đã được nghi n cứu và đưa ra như: Dựa tr n iểm chứng mô hình
(Model Chec ing), ểm thử ngẫu nhi n (Random Testing) Nhưng
hạn chế của n là iểm tra c ng một hành vi thực thi của chương
trình nhiều lần với những đầu vào hác nhau và ch c thể iểm tra
được một số trường hợp thực thi của chương trình Th m vào đ ,
iểm thử ngẫu nhi n h xác định được hi nào việc iểm thử n n
được dừng lại và n hông iết tại điểm nào hông gian trạng thái đã
được thám hiểm hết Để xác định hi nào việc iểm thử dừng lại thì
hệ thống iểm thử ngẫu nhi n được ết hợp với các ti u chuẩn an
toàn Để hắc phục những hạn chế của iểm thử ngẫu nhi n, phương
pháp thực thi tương trưng x y dựng các ràng uộc tr n các giá trị
hiệu và giải các ràng uộc đ để sinh ra các giá trị đầu vào cho
chương trình mà c thể ao phủ tất các d ng lệnh c ng như các
nhánh thực thi của chương trình
tưởng của thực thi hiệu đã được đề xuất ởi, nhưng
việc hiện thực tưởng mới ch được thực hiện trong những năm gần
đ y qua tiến ộ đáng ể trong l thuyết giải các ràng uộc và các tiếp
8
cận mở rộng thực thi hiệu động , một ỹ thuật ết hợp giữa các
giá trị cụ thể và giá trị hiệu cho các giá trị đầu vào
1.4. Các kỹ thuật thực thi ký hiệu
a. Concolic testing
Thực thi hiệu động chính là sự ết hợp giữa thực thi cụ thể và
thực thi hiệu Trong thực thi hiệu động, chương trình được
thực thi nhiều lần với những giá trị hác nhau của tham số đầu vào
Bắt đầu ằng việc chọn những giá trị t y cho các tham số đầu
vào và thực thi chương trình với những giá trị cụ thể đ chương trình
sẽ được thực thi theo một đường đi xác định DART thực thi chương
trình với các giá trị cụ thể của tham số đầu vào và thu gom các ràng
buộc trong quá trình thực thi theo đường đi mà sự thực thi cụ thể này
đi theo, đồng thời suy ra các ràng uộc mới từ những ràng uộc đã
thu gom được
Tại các c u lệnh rẽ nhánh, iểu thức điều iện rẽ nhánh sẽ được
đánh giá theo các giá trị cụ thể của các tham số đầu vào Nếu iểu
thức điều iện rẽ nhánh nhận giá trị là True thì iểu thức của điều
kiện rẽ nhánh sẽ được thu gom vào ràng uộc của ràng uộc lộ trình
và được ghi nhớ, đồng thời phủ định của điều iện rẽ nhánh sẽ được
sinh ra và được th m vào một ràng buộc lộ trình tương ứng với
nhánh c n lại mà sự thực thi cụ thể đ hông đi theo Một bộ xử l
ràng buộc sẽ được sử dụng để giải quyết các ràng uộc mới sinh ra
này để sinh ra các giá trị cụ thể của tham số đầu vào Trong trường
hợp ngược lại iểu thức phủ định của điều iện rẽ nhánh sẽ được thu
gom vào ràng buộc của ràng uộc lộ trình tương ứng với nhánh mà
sự thực thi hiện thời đang đi theo và được ghi nhớ Đồng thời điều
kiện rẽ nhánh sẽ được sinh ra và th m vào PC tương ứng với nhánh
c n lại mà sự thực thi hiện thời hông đi theo Các giá trị mới được
9
sinh ra của các tham số đầu vào sẽ tiếp tục được thực thi và quá trình
này sẽ được l p lại cho tới hi chương trình được thực thi theo tất cả
các đường đi Do các chương trình được thực thi với những giá trị cụ
thể n n c thể thấy rằng tất cả các đường đi ph n tích được trong quá
trình thực thi hiệu động đều là các đường đi hả thi
b. Excution generated testing
EGT trộn lẫn giá trị cụ thể và thực thi hiệu ằng cách iểm tra
động trước mọi toán hạng Nếu các giá trị li n quan đ hoàn toàn là
các giá trị cụ thể thì toán hạng đ sẽ thực thi như chương trình gốc
C n nếu c ít nhất một giá trị là hiệu thì toán hạng sẽ thực hiện
thực thi hiệu và cập nhật điều iện ràng buộc đường đi cho đường
thực thi hiện thời
1.5. Các thách thức và giải pháp
a. Bùng nổ đường đi
Một trong những thách thức quan trọng của thực thi hiệu là
n sẽ sinh ra một số lượng lớn các đường thực thi m c d chương
trình là nhỏ và thường là hàm m trong số các c u lệnh rẽ nhánh tĩnh
của mã nguồn Kết quả là trong một hoảng thời gian định trước n
sẽ quyết định hám phá con đường đầu ti n sao cho ph hợp nhất
Trước hết, lưu rằng thực thi hiệu đã ngầm lọc ra tất cả
các đường thực thi hông phụ thuộc vào các iến hiệu đầu vào và
những đường dẫn hông hả thi (Infeasi lle path) trong quá trình
giải các ràng uộc M c d như vậy, sự ng n đường dẫn vẫn là
một trong những thách thức lớn nhất đối với thực thi hiệu Hiện
nay c 2 cách tiếp cận chính để giải quyết vấn đề này là ưu ti n tìm
iếm inh nghiệm (Heuristic search) và sử dụng ỹ thuật ph n tích
tính đúng đắn của chương trình.
10
b. Giải các ràng buộc
M c d đã c những tiến ộ đáng ể trong ỹ thuật thực hiện
giải các ràng uộc trong những năm gần đ y, giúp cho thực thi
hiệu trở n n thực tế hơn, nhưng việc giải các ràng uộc vẫn là cản trở
đáng ể của thực thi ký hiệu N thường chiếm nhiều thời gian trong
quá trình thực hiện và là một trong những l do chính hiến thực thi
tương trưng hông mở rộng được với một số loại chương trình mà
mã nguồn của n sinh ra với y u cầu rất lớn trong việc giải các ràng
buộc.
c. Mô hình hóa bộ nhớ
Độ chính xác của các c u lệnh của chương trình hi chuyển sang
các ràng buộc ký hiệu c ảnh hưởng đáng ể đến độ ao phủ hi thực
hiện thực thi hiệu Ví dụ hi sử dụng mô hình hóa bộ nhớ mà xấp
x để thiết lập độ rộng cho tham iến iểu Interger c thể c hiệu quả
hơn trong thực tế nhưng m t hác ết quả lại thiếu chính xác trong
ph n tích mã nguồn N phụ thuộc vào hoảng lựa chọn giá trị tương
ứng như lỗi tràn ộ nhớ toán học, c ng c thể g y ra thiếu đường dẫn
trong thực thi hiệu, ho c khai phá những đường đi hông hả thi
vv..
11
CHƢƠNG 2
GIẢI PHÁP SINH DỮ LIỆU THỬ
CHO CHƢƠNG TRÌNH JAVA
2.1. Giải pháp sinh dữ liệu thử cho chƣơng trình JAVA
a. Tổng quan về giải pháp
Mô hình t ng thể của giải pháp sinh dữ liệu thử cho chương trình
Java được mi u tả như trong hình 2 1 dưới đ y:
Hình 2.1. Mô hình triển khai
Tham số đầu vào của phương pháp là tệp nguồn Java cần
phân tích, số vòng l p tối đa (của các lệnh l p for, while ...), và các
tiêu chuẩn phủ. Mã nguồn Java được ph n rã thành các phương thức
và mức độ ưu ti n xử lý của chúng được tính toán, những phương
thức ít phụ thuộc vào các phương thức hác hơn sẽ c độ ưu ti n xử
l cao hơn, như vậy những phương thức không có lời gọi hàm sẽ
được xử l đầu tiên. Cuối cùng chúng ta có một danh sách các
12
phương thức được xếp theo mức ưu ti n giảm dần, và chúng lần lượt
được xử lý theo thứ tự đ
Với mỗi phương thức, đầu ti n đồ thị luồng điều khiển được
xây dựng, duyệt đồ thị luồng điều khiển sẽ cho ra các lộ trình thực
thi của phương thức, tiếp đến c được tập ràng buộc tương ứng nhờ
áp dụng phương pháp thực thi ký hiệu. Quá trình này được l p lại
cho đến khi tất cả các phương thức được phân tích hết.
Các lộ trình thực thi đã tìm được ở ước trên sẽ được đưa lần
lượt vào SMT-Solver để kiểm tra tính thoả được và sinh ra dữ liệu
kiểm thử tự động đảm bảo bao phủ được lộ trình đã đưa vào SMT-
Solver
b. Phương pháp thực hiện
Bƣớc 1: Phân tích danh sách các phương thức
Ta dựa vào 2 định nghĩa sau:
Định nghĩa 2.1: Đồ thị luồng với tập nút N, tập cạnh E, là
một đồ thị c hướng liên thông, luôn luôn có duy nhất một điểm đầu
vào, và ít nhất một điểm kết thúc [7].
Định nghĩa 2.2: Trong chương trình, đồ thị luồng biễu diễn
cho những luồng điều khiển khả thi của n , trong đ mỗi nút tương
ứng cho các điểm chương trình (tập lệnh) và các cạnh thể hiện cho
luồng điều khiển giữa các điểm đ [7]
Dựa vào cấu trúc một phương thức ta phân tách thành các
khối độc lập Sau đ lại gọi đệ quy để phân tích thành các khối cấu
trúc con của n Trong ước này, có thể sử dụng công cụ JDT cho
phép duyệt qua toàn bộ phương thức và nhận dạng các thành phần
cấu tạo nên một câu lệnh như If, For, While ; từ đ dễ dàng xây
dựng các đ c tả của một nút và giúp tập trung vào thuật toán xây
dựng đồ thị.
13
Bƣớc 2: Sinh ra các lộ trình thực thi
Tập hợp các lộ trình thực thi của một hàm có thể lấy được
bằng cách duyệt đồ thị luồng điều khiển tương ứng với nó. Với
những phương thức có lời gọi hàm con, mỗi nút của đồ thị ho c là
các câu lệnh ( ho c tập các câu lệnh ) xác định, ho c sẽ là lời gọi đến
các hàm con đ
Cần lưu rằng thay vì chèn ràng buộc lộ trình của hàm con,
có thể thay thế nó bằng lộ trình thực thi tương ứng. Tuy nhiên kết
quả của một hàm ch phụ thuộc vào đối số của nó, nói cách khác các
biến hác được tạo ra và sử dụng n trong hàm con được gọi không
ảnh hưởng đến lộ trình thực thi hiện tại. Do vậy việc sử dụng lộ trình
ràng buộc sẽ là tối ưu hi mà các iến số n trong n đã được xử lý
bằng thực thi ký hiệu.
Bƣớc 3: Sinh ra tập các ràng buộc
Định nghĩa 2.3: Ràng buộc lộ trình[7] là một tập hợp các
biểu thức luận lý:
trong đ n là số nút điều kiện của đường thực thi, c biểu diễn ràng
buộc tương ứng với mỗi điều kiện đ
Tập lộ trình thực thi của các phương thức được xử l để cho
ra tập lộ trình ràng buộc bằng cách sử dụng phương pháp Thực thi ký
hiệu. Mỗi ước thực hiện trên lộ trình thực thi được mô tả bởi trạng
thái bởi các biến đầu vào (input) và các biến n trong phương thức
Bƣớc 4 : Sinh ra các dữ liệu kiểm thử từ bộ SMT solver
Để làm việc với SMT ta thực hiện công việc chuẩn hóa các
đầu vào theo định dạng SMT – LIB. Mỗi nút của đường ràng buộc sẽ
được chuyển từ dạng trung tố sang dạng tiền tố, từ hoá assert được
sử dụng để thêm các ràng buộc vào SMT
14
2.2. Vấn đề tối ƣu các ràng buộc
Một trong những nhược điểm chính của sinh dữ liệu thử tự
động là cần phải tối thiểu các ràng buộc nhằm đảm bảo tốc độ thực
thi và hao tốn về tài nguy n như đã trình ày trong mục 1.5, vì vậy
thuật toán tối ưu h a các ràng uộc đã được cài đ t tích hợp thêm
vào trong công cụ có sẵn và đảm bảo các điểm sau:
-
Hạn chế số lượng các ràng buộc được đưa vào SMT để giảm
tiêu tốn về tài nguyên.
-
Đảm bảo tính đúng đắn, không làm sai lệch kết quả đầu ra
của chương trình sau hi áp dụng thuật toán.
Vì vậy, ài toán đ t ra là phải cài đ t thuật toán tối ưu h a
vào trong chương trình mã nguồn mở có sẵn để tăng tốc độ thực thi
nhưng vẫn đảm bảo tính đúng đắn của chương trình
2.3. Giải quyết các ràng buộc
Trong quá trình thực hiện việc tối ưu hoá các ràng uộc,
chúng tôi sử dụng công cụ mã nguồn mở JPF trong việc hỗ trợ thực
thi ký hiệu và ch tập trung vào việc cài đ t và thử nghiệm thuật toán
để tối ưu hoá các ràng uộc. Mô hình thực hiện được biểu diễn: Với
sự hỗ trợ từ công cụ mã nguồn mở JPF, có thể triển khai quá trình
thực hiện như trong thuật toán được trình bày cụ thể trong mục 2.5
2.4. Ứng dụng JAVA PATH FINDER
a. Giới thiệu về JPF
JPF là một máy ảo cho Java ytecode, c nghĩa là n là một
chương trình nhận đầu vào là một chương trình Java để thực thi. Nó
được sử dụng để tìm lỗi trong các chương trình này, vì vậy ta c ng
cần phải cung cấp cho nó các thuộc tính để kiểm tra như đầu vào
[10].
15
JPF sẽ cho ra một báo cáo đã được tạo ra bởi JPF để phân
tích Cơ chế của JPF được thực hiện như hình minh họa sau:
Hình 2.3. Cấu trúc của JPF
b. Giới thiệu về bộ mở rộng JPF-SYMBC
JPF-SYMBC là một gói mở rộng của JPF nhằm mục tiêu hỗ trợ
người lập trình trong việc thực hiện thực thi ký hiệu.
JPF-SYMBC ết hợp thực thi hiệu và iểm chứng mô hình
và thực hiện giải các ràng uộc để sinh các dữ liệu test, hỗ trợ thực
thi ký hiệu động và thực thi trên các tệp ytecode và c thể áp dụng
đối với mô hình cho các ngôn ngữ mô hình h a SPF c thể thực hiện
tr n các iểu dữ liệu nguy n, iểu thực, con trỏ, mảng, một số toán
tử tr n iểu x u (đang phát triển và hoàn thiện) và sử dụng ết hợp
một số ộ giải ràng uộc như: Choco, IASolve, CVC3 thực hiện giải
các ràng buộc tuyến tính, phi tuyến tính tr n các iểu số nguy n, số
thực, iểu tham chiếu (con trỏ) và iểu x u
c. Tối ưu hoá các ràng buộc lộ trình để phục vụ cho quá trình thực
thi ký hiệu
Việc giải các ràng buộc(Constraint solving) là một phần
không thể thiếu của việc thực thi ký hiệu, việc giải quyết các
constraint là phần tốt nhiều tài nguyên nhất trong quá trình thực thi
ký hiệu. Trong thực tế, hiệu suất của các chế giải quyết được sử dụng
bởi một kỹ thuật thực thi ký hiệu có thể ảnh hưởng đáng ể đến hiệu
16
suất t ng thể của nó. Không may, giải quyết hạn chế này chủ yếu
được sử dụng trong thực thi ký hiệu không tận dụng bất kỳ ngữ cảnh
và thông tin tên miền có sẵn Để giải quyết vấn đề này, đề tài đã sử
dụng một chiến lược tối ưu h a mới, sử dụng miền và các thông tin
theo ngữ cảnh để tối ưu h a hiệu suất của giải quyết các ràng buộc
trong quá trình thực thi ký hiệu.
Quá trình thực thi ký hiệu thực thi một chương trình với đầu là
quá trình kiếm tra tất cả các lộ trình có thể trong chương trình Đối
với mỗi lộ trình, quá trình thực thi ký hiệu cập nhật các trạng thái
mang tính biểu tượng của chương trình theo ngữ nghĩa Ở phần cuối
của quá trình thực thi ký hiệu, rang buộc lộ trình được đưa váo các
bộ solver và thông qua các SMT để tìm ra kết quả
Phương án tối ưu sau đ y được gọi là phương pháp rút gọn miền,
với 2 ràng buộc Ca và Cb trong 1 tập ràng buộc C được gọi là phụ
thuộc nếu ít nhất thỏa mãn :
-
Phụ thuộc trực tiếp: Ca và Cb cùng tồn tại trong một ràng
buộc.
-
Phụ thuộc không trực tiếp: Ca và Cb có phụ thuộc trực tiếp
tới một biến Cc.
Giải pháp chứa ràng buộc không có sự phụ thuộc với các biến
ràng buộc mục tiêu thì không ảnh hưởng đến kết quả.vì vậy ta có thể
loại bỏ ràng buộc này khỏi ràng buộc lộ trình và đưa vào trở lại sau
quá trình thực thi Đối với các ràng buộc thực tế hơn, đơn giản hóa
này có thể dẫn đến tiết kiệm đáng ể về số lượng hạn chế mà bộ giải
SMT phải xử lý.
Cách tiếp cận tối ưu dựa trên việc giảm các ràng buộc trên
miền dữ liệu được thực hiện như sau
17
-
Bước 1: Chia các biến mục ti u thành các nh m theo độ
phụ thuộc.
-
-
Bước 2: Tìm 2 biến c độ phụ thuộc lớn nhất và bé nhất.
Bước 3: Thay thế lần lượt các biến mục tiêu với giá trị
đầu vào với từng nhóm và thực hiện ước lược bỏ các
phụ thuôc như đã trình ày ở trên.
2.5. Cài đặt tối ƣu các ràng buộc với JPF
a. Kiến trúc của JPF và mở rộng JPF-SYMBC
b. Các thiết lập của JPF
c. Cài đặt tối ưu ràng buộc
d. Thuật toán tối ưu
Thuật toán tối ưu các ràng uộc được trình ày trong chương 2
được triển hai như sau:
Input: Ràng buộc lộ trình, giá trị các biến mục tiêu và biến cố
định, bộ giải SMT.
Output: kết quả sau khi giải bằng SMT (sat, usat ho c
unknown).
Constraint cur = getTargetConstraint(index, pc)
List targetsymlist = getSymVars(cur)
result = unknown
for i = 1 to length(targetsymlist) do
groups[] = formGroupsofX(i, targetsymlist)
List dependencies = []
for a = 0 to length(groups) do
dependencies[a] = getDependencies(groups[a], pc)
end
int selectDep[0] = findSmallestDepIndex(dependencies)
int selectDep[1] = findLargestDepIndex(dependencies)
for b = 0 to length(selectedDep) do
List grpDep = dependencies[(selectDep[b])]
List
symbolicVars
=
join(groups(selectDep[b]),
grpDep)
18
newPC = modifyPC(symbolicVars,concreteValuesMapping,pc)
output = callSolver(solver,newPC)
if output = “sat” then
return output
end
else if output = “unsat” then
result = output
end
end
end
Trong thuật toán tối ưu hoá ràng uộc, chúng tôi có một số
phương thức quan trọng:
findSmallestDepIndex(): nhận đầu vào là một tập các
phụ thuộc, và trả về giá trị của phụ thuộc có ít sự phụ
thuộc nhất.
findLargestDepIndex(): nhận đầu vào là một tập các phụ
thuộc, và trả về giá trị của phụ thuộc có ít sự phụ thuộc
nhất.
modifyPC(): Thay thế các giá trị ký hiệu của biến mục
tiêu bằng các giá trị hiện thời của lộ trình.
Tải về để xem bản đầy đủ
25 trang
19720
Free
Bạn đang xem 20 trang mẫu của tài liệu "Tóm tắt Luận văn Xây dựng công cụ sinh dữ liệu thử tự động cho chương trình Java", để tải tài liệu gốc về máy hãy click vào nút Download ở trên
File đính kèm:
- tom_tat_luan_van_xay_dung_cong_cu_sinh_du_lieu_thu_tu_dong_c.pdf
