cuongtribal
New Member
Link tải luận văn miễn phí cho ae Kết Nối
CHƢƠNG 1- JPF VÀ THỰC THI TƢỢNG TRƢNG ...................................3
1.1 Giới thiệu về JPF......................................................................................3
1.1.1 JPF có thể kiểm tra những chương trình gì? .......................................4
1.1.2 Kiến trúc mức cao của JPF.................................................................5
1.1.3 Khả năng mở rộng của JPF ................................................................6
1.1.4 Một số mở rộng của JPF ....................................................................8
1.2 Thực thi tượng trưng để sinh dữ liệu kiểm thử ..........................................9
1.2.1 Thực thi tượng trưng là gì? ................................................................9
1.2.2 Thực thi tượng trưng với JPF ...........................................................10
1.2.3 Hướng dẫn thực thi tượng trưng với JPF..........................................11
1.2.4 Hạn chế............................................................................................19
CHƢƠNG 2- MICROSOFT Z3 ....................................................................21
2.1 SMT là gì................................................................................................21
2.2 Z3 là gì ...................................................................................................21
2.3 Tại sao lại là Z3?....................................................................................22
2.4 Kiến trúc của Z3.....................................................................................22
2.5 Định dạng đầu vào .................................................................................24
2.6 Định dạng SMT-LIB ...............................................................................24
2.6.1 Các chức năng chính của SMT-LIB. ................................................24
2.7 Các quan hệ, hàm, và hằng số. ...............................................................25
2.7.1 Tất cả các hàm là tuyệt đối (total) [10].............................................25
2.7.2 Hàm không dịch (uninterpreted function) và hằng số.......................26
2.7.3 Hàm đệ quy......................................................................................27
2.8 Số học.....................................................................................................27
2.8.1 Số học tuyến tính thực .....................................................................27
2.8.2 Số học tuyến tính nguyên.................................................................27
2.8.3 Trộn giữa số nguyên và số thực. ......................................................28
2.8.4 Số học phi tuyến tính .......................................................................28
2.9 Kiểu dữ liệu ............................................................................................29
2.9.1 Kiểu bản ghi ....................................................................................29
2.9.2 Kiểu liệt kê (enumeration) ...............................................................29
2.9.3 Kiểu dữ liệu đệ qui...........................................................................29
2.10 Ví dụ về Z3 ..........................................................................................30
2.11 Một vài ứng dụng của Z3 ....................................................................30
CHƢƠNG 3- MỞ RỘNG JPF VỚI Z3 .........................................................32
3.1 Nghiên cứu, đánh giá các giải pháp .......................................................32
3.2 Kiến trúc hệ thống ..................................................................................32
3.3 Chuyển đổi dữ liệu..................................................................................33
3.4 Thiết kế và cài đặt ..................................................................................37
3.5 Kết quả và đánh giá................................................................................39
CÁC NGHIÊN CỨU LIÊN QUAN...................................................................44
ĐẶT VẤN ĐỀ
Trong những năm gần đây, 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 bả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 khoa, ngân hàng, hàng không… Việc kiểm
thử phần mềm một cách thủ công chỉ đảm bả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ụ để kiểm chứng, kiểm thử phần mềm một cách tự động.
Kiểm thử tự động không chỉ giúp giảm chi phí phát triển phần mềm mà còn làm
tăng tính linh động của các phần mềm hiện đại. Người ta ước lượng rằng chi phí
cho các dự án phần mềm thất bại ở Mỹ là khoảng 60 tỉ USD hàng năm, và việc cải
tiến các cách để kiểm thử phần mềm có thể tiết kiệm được 1/3 chi phí trên
[12].
Xuất phát từ nhu cầu thực tế trên, tác giả đã nghiên cứu một số lý thuyết,
công cụ trong việc kiểm thử phần mềm. Một lý thuyết nền tảng rất quan trọng đó
là lý thuyết về tính thỏa được, viết tắt là SMT (Satisfiability Modulo Theories). Lý
thuyết về tính thỏa được đã được ứng dụng để giải quyết nhiều bài toán trong công
nghệ phần mềm như:
Kiểm chứng chương trình
Khám phá chương trình
Mô hình hóa phần mềm
Sinh các ca kiểm thử
Hiện nay Microsoft Z3 là một công cụ tìm lời giải cho SMT đang được áp
dụng trong nhiều dự án của Microsoft như: Pex, Spec#, SLAM/SDV, Yogi. Z3
được đánh giá là một trong những công cụ tìm lời giải phát triển nhất hiện nay. Tuy
nhiên Z3 chỉ được áp dụng cho các ngôn ngữ của Microsoft. Vì vậy tác giả đặt ra
vấn đề: Liệu có thể sử dụng Z3 để kiểm thử cho các chương trình viết bằng ngôn
ngữ khác như Java?
Trong quá trình nghiên cứu về kiểm chứng, kiểm thử phần mềm tác giả
cũng có tìm hiểu về JavaPathFinder (JPF). JPF là một dự án mã nguồn mở được
phát triển trên ngôn ngữ Java. Hiện nay có một mở rộng của JPF trong việc sinh tự
động dữ liệu đầu vào để kiểm thử chương trình. Tuy nhiên còn rất nhiều hạn chế,
vì vậy tác giả đã nghĩ đến việc làm sao để tích hợp được Z3 với JPF để có thể sinh
tự động dữ liệu kiểm thử chương trình. Nếu việc tích hợp thành công thì sẽ dẫn tới
việc giải quyết được lớp bài toán rộng hơn. Điều này là rất có ý nghĩa đối với thực
tế.
MỤC TIÊU CỦA ĐỀ TÀI
Mục tiêu của đề tài là nghiên cứu nắm bắt rõ về Z3 và JPF. Sau đó bước đầu
tích hợp thành công Z3 vào JPF (mở rộng JPF với Z3) để có thể sinh tự động dữ
liệu kiểm thử chương trình Java cho các bài toán mà hiện nay JPF không thể thực
hiện được. (ví dụ: sinh tự động dữ liệu cho số học phi tuyến tính).
CẤU TRÚC CỦA LUẬN VĂN
Luận văn bao gồm các phần sau:
Mở đầu: Giới thiệu về đề tài, tính cấp thiết cũng như mục tiêu của đề tài
Chƣơng 1: JPF và Thực thi tượng trưng
Nội dung: Trong chương này tác giả sẽ trình bày những hiểu biết về JPF và thực
thi tượng trưng, JPF sẽ thực thi tượng trưng để sinh dữ liệu kiểm thử ra sao. Ngoài
ra tác giả cũng giới thiệu một số mở rộng của JPF đang được phát triển hiện nay.
Chƣơng 2: Microsoft Z3
Nội dung: Giới thiệu về dự án của Microsoft đang được quan tâm hiện nay đó là
Z3. Trong phần này tác giả sẽ trình bày các chức năng chính và một số ứng dụng
của Z3, cũng như các API mà Z3 hỗ trợ để từ đó có thể tích hợp với JPF.
Chƣơng 3: Mở rộng JPF với Z3
Nội dung: Dựa trên kết quả của chương 1 và 2, trong phần này tác giả sẽ đánh giá
và đưa ra các giải pháp để mở rộng JPF với Z3. Sau khi đã có giải pháp sẽ tiến
hành thiết kế kiến trúc hệ thống, sau đó chi tiết hóa sang mức gói, mức lớp cuối
cùng là cài đặt và đánh giá kết quả.
Các nghiên cứu liên quan
Phần này tác giả sẽ trình bày một số nghiên cứu khác liên quan đến luận văn, đó là
các công cụ Pex, AgitarOne, Cute trong việc tự động kiểm thử chương trình.
Kết luận và hƣớng phát triển của luận văn
Trình bày kết quả sau khi nghiên cứu, những hạn chế và hướng phát triển tiếp
theo.
CHƢƠNG 3- MỞ RỘNG JPF VỚI Z3
Chương 1 và 2 đã trình bày về Z3 và JPF. Chúng ta có thể thấy rằng: khả
năng giải quyết các vấn đề cho thực thi tượng trưng của JPF vẫn còn hạn chế, vì
vậy chương này của luận văn sẽ trình bày về tích hợp Z3 vào JPF trong việc sinh
dữ liệu để kiểm thử chương trình Java.
3.1 Nghiên cứu, đánh giá các giải pháp
Hiện nay Z3 hỗ trợ một số kiểu định dạng đầu vào đó là: Z3 native, SMTLIB, simplify, DIMACS. Qua quá trình tìm hiểu tác giả thấy:
Định dạng SMT-LIB được sử dụng trong rất nhiều công cụ tìm lời giải cho
SMT.
Đầy đủ và dễ hiểu trong việc biểu diễn các biểu thức.
Vì vậy chương trình sẽ sử dụng định dạng SMT-LIB để tích hợp giữa Z3 và JPF.
Tích hợp thành công giữa Z3 và JPF thông qua SMT – LIB sẽ giúp cho việc tích
hợp các công cụ tìm lời giải khác trở nên dễ dàng.
Sau khi chọn định dạng SMT-LIB làm định dạng chung để trao đổi giữa Z3
và JPF. Ta có thể thực hiện giao tiếp bằng các cách sau:
Cách 1: Thực hiện thông qua socket
Cách 2: Thực hiện trực tiếp thông qua thực thi bằng dòng lệnh (command
line).
Cách 1 có ưu điểm là chương trình có thể chạy phân tán tuy nhiên mất nhiều
thời gian cho việc phát triển hơn. Cách 2 có nhược điểm là Z3 và JPF phải chạy
trên cùng một máy tuy nhiên ưu điểm là cài đặt tốn ít thời gian hơn.
Cả 2 cách đều phải giải quyết một vấn đề đó là chuyển đổi các ràng buộc
hiện thời của JPF sang SMT – LIB sau đó sử dụng Z3 để lấy kết quả về.
Trong luận văn này sẽ sử dụng cách 2 để cài đặt chương trình.
3.2 Kiến trúc hệ thống
Như ta đã biết JPF hiện nay đang sử dụng một số các công cụ tìm lời giải
viết bằng Java như là: Choco, IAsolver. Vì vậy ý tưởng của việc thiết kế hệ thống
là ta sẽ xây dựng một wrapper, wrapper này là giao diện để liên kết giữa JPF và
Z3. Wrapper sẽ tương tác với Z3 tương tư như Choco hay IAsolver.
Kiến trúc hệ thống được mô tả như hình 3-1 bên dưới:
Do Drive thay đổi chính sách, nên một số link cũ yêu cầu duyệt download. các bạn chỉ cần làm theo hướng dẫn.
Password giải nén nếu cần: ket-noi.com | Bấm trực tiếp vào Link để tải:
CHƢƠNG 1- JPF VÀ THỰC THI TƢỢNG TRƢNG ...................................3
1.1 Giới thiệu về JPF......................................................................................3
1.1.1 JPF có thể kiểm tra những chương trình gì? .......................................4
1.1.2 Kiến trúc mức cao của JPF.................................................................5
1.1.3 Khả năng mở rộng của JPF ................................................................6
1.1.4 Một số mở rộng của JPF ....................................................................8
1.2 Thực thi tượng trưng để sinh dữ liệu kiểm thử ..........................................9
1.2.1 Thực thi tượng trưng là gì? ................................................................9
1.2.2 Thực thi tượng trưng với JPF ...........................................................10
1.2.3 Hướng dẫn thực thi tượng trưng với JPF..........................................11
1.2.4 Hạn chế............................................................................................19
CHƢƠNG 2- MICROSOFT Z3 ....................................................................21
2.1 SMT là gì................................................................................................21
2.2 Z3 là gì ...................................................................................................21
2.3 Tại sao lại là Z3?....................................................................................22
2.4 Kiến trúc của Z3.....................................................................................22
2.5 Định dạng đầu vào .................................................................................24
2.6 Định dạng SMT-LIB ...............................................................................24
2.6.1 Các chức năng chính của SMT-LIB. ................................................24
2.7 Các quan hệ, hàm, và hằng số. ...............................................................25
2.7.1 Tất cả các hàm là tuyệt đối (total) [10].............................................25
2.7.2 Hàm không dịch (uninterpreted function) và hằng số.......................26
2.7.3 Hàm đệ quy......................................................................................27
2.8 Số học.....................................................................................................27
2.8.1 Số học tuyến tính thực .....................................................................27
2.8.2 Số học tuyến tính nguyên.................................................................27
2.8.3 Trộn giữa số nguyên và số thực. ......................................................28
2.8.4 Số học phi tuyến tính .......................................................................28
2.9 Kiểu dữ liệu ............................................................................................29
2.9.1 Kiểu bản ghi ....................................................................................29
2.9.2 Kiểu liệt kê (enumeration) ...............................................................29
2.9.3 Kiểu dữ liệu đệ qui...........................................................................29
2.10 Ví dụ về Z3 ..........................................................................................30
2.11 Một vài ứng dụng của Z3 ....................................................................30
CHƢƠNG 3- MỞ RỘNG JPF VỚI Z3 .........................................................32
3.1 Nghiên cứu, đánh giá các giải pháp .......................................................32
3.2 Kiến trúc hệ thống ..................................................................................32
3.3 Chuyển đổi dữ liệu..................................................................................33
3.4 Thiết kế và cài đặt ..................................................................................37
3.5 Kết quả và đánh giá................................................................................39
CÁC NGHIÊN CỨU LIÊN QUAN...................................................................44
ĐẶT VẤN ĐỀ
Trong những năm gần đây, 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 bả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 khoa, ngân hàng, hàng không… Việc kiểm
thử phần mềm một cách thủ công chỉ đảm bả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ụ để kiểm chứng, kiểm thử phần mềm một cách tự động.
Kiểm thử tự động không chỉ giúp giảm chi phí phát triển phần mềm mà còn làm
tăng tính linh động của các phần mềm hiện đại. Người ta ước lượng rằng chi phí
cho các dự án phần mềm thất bại ở Mỹ là khoảng 60 tỉ USD hàng năm, và việc cải
tiến các cách để kiểm thử phần mềm có thể tiết kiệm được 1/3 chi phí trên
[12].
Xuất phát từ nhu cầu thực tế trên, tác giả đã nghiên cứu một số lý thuyết,
công cụ trong việc kiểm thử phần mềm. Một lý thuyết nền tảng rất quan trọng đó
là lý thuyết về tính thỏa được, viết tắt là SMT (Satisfiability Modulo Theories). Lý
thuyết về tính thỏa được đã được ứng dụng để giải quyết nhiều bài toán trong công
nghệ phần mềm như:
Kiểm chứng chương trình
Khám phá chương trình
Mô hình hóa phần mềm
Sinh các ca kiểm thử
Hiện nay Microsoft Z3 là một công cụ tìm lời giải cho SMT đang được áp
dụng trong nhiều dự án của Microsoft như: Pex, Spec#, SLAM/SDV, Yogi. Z3
được đánh giá là một trong những công cụ tìm lời giải phát triển nhất hiện nay. Tuy
nhiên Z3 chỉ được áp dụng cho các ngôn ngữ của Microsoft. Vì vậy tác giả đặt ra
vấn đề: Liệu có thể sử dụng Z3 để kiểm thử cho các chương trình viết bằng ngôn
ngữ khác như Java?
Trong quá trình nghiên cứu về kiểm chứng, kiểm thử phần mềm tác giả
cũng có tìm hiểu về JavaPathFinder (JPF). JPF là một dự án mã nguồn mở được
phát triển trên ngôn ngữ Java. Hiện nay có một mở rộng của JPF trong việc sinh tự
động dữ liệu đầu vào để kiểm thử chương trình. Tuy nhiên còn rất nhiều hạn chế,
vì vậy tác giả đã nghĩ đến việc làm sao để tích hợp được Z3 với JPF để có thể sinh
tự động dữ liệu kiểm thử chương trình. Nếu việc tích hợp thành công thì sẽ dẫn tới
việc giải quyết được lớp bài toán rộng hơn. Điều này là rất có ý nghĩa đối với thực
tế.
MỤC TIÊU CỦA ĐỀ TÀI
Mục tiêu của đề tài là nghiên cứu nắm bắt rõ về Z3 và JPF. Sau đó bước đầu
tích hợp thành công Z3 vào JPF (mở rộng JPF với Z3) để có thể sinh tự động dữ
liệu kiểm thử chương trình Java cho các bài toán mà hiện nay JPF không thể thực
hiện được. (ví dụ: sinh tự động dữ liệu cho số học phi tuyến tính).
CẤU TRÚC CỦA LUẬN VĂN
Luận văn bao gồm các phần sau:
Mở đầu: Giới thiệu về đề tài, tính cấp thiết cũng như mục tiêu của đề tài
Chƣơng 1: JPF và Thực thi tượng trưng
Nội dung: Trong chương này tác giả sẽ trình bày những hiểu biết về JPF và thực
thi tượng trưng, JPF sẽ thực thi tượng trưng để sinh dữ liệu kiểm thử ra sao. Ngoài
ra tác giả cũng giới thiệu một số mở rộng của JPF đang được phát triển hiện nay.
Chƣơng 2: Microsoft Z3
Nội dung: Giới thiệu về dự án của Microsoft đang được quan tâm hiện nay đó là
Z3. Trong phần này tác giả sẽ trình bày các chức năng chính và một số ứng dụng
của Z3, cũng như các API mà Z3 hỗ trợ để từ đó có thể tích hợp với JPF.
Chƣơng 3: Mở rộng JPF với Z3
Nội dung: Dựa trên kết quả của chương 1 và 2, trong phần này tác giả sẽ đánh giá
và đưa ra các giải pháp để mở rộng JPF với Z3. Sau khi đã có giải pháp sẽ tiến
hành thiết kế kiến trúc hệ thống, sau đó chi tiết hóa sang mức gói, mức lớp cuối
cùng là cài đặt và đánh giá kết quả.
Các nghiên cứu liên quan
Phần này tác giả sẽ trình bày một số nghiên cứu khác liên quan đến luận văn, đó là
các công cụ Pex, AgitarOne, Cute trong việc tự động kiểm thử chương trình.
Kết luận và hƣớng phát triển của luận văn
Trình bày kết quả sau khi nghiên cứu, những hạn chế và hướng phát triển tiếp
theo.
CHƢƠNG 3- MỞ RỘNG JPF VỚI Z3
Chương 1 và 2 đã trình bày về Z3 và JPF. Chúng ta có thể thấy rằng: khả
năng giải quyết các vấn đề cho thực thi tượng trưng của JPF vẫn còn hạn chế, vì
vậy chương này của luận văn sẽ trình bày về tích hợp Z3 vào JPF trong việc sinh
dữ liệu để kiểm thử chương trình Java.
3.1 Nghiên cứu, đánh giá các giải pháp
Hiện nay Z3 hỗ trợ một số kiểu định dạng đầu vào đó là: Z3 native, SMTLIB, simplify, DIMACS. Qua quá trình tìm hiểu tác giả thấy:
Định dạng SMT-LIB được sử dụng trong rất nhiều công cụ tìm lời giải cho
SMT.
Đầy đủ và dễ hiểu trong việc biểu diễn các biểu thức.
Vì vậy chương trình sẽ sử dụng định dạng SMT-LIB để tích hợp giữa Z3 và JPF.
Tích hợp thành công giữa Z3 và JPF thông qua SMT – LIB sẽ giúp cho việc tích
hợp các công cụ tìm lời giải khác trở nên dễ dàng.
Sau khi chọn định dạng SMT-LIB làm định dạng chung để trao đổi giữa Z3
và JPF. Ta có thể thực hiện giao tiếp bằng các cách sau:
Cách 1: Thực hiện thông qua socket
Cách 2: Thực hiện trực tiếp thông qua thực thi bằng dòng lệnh (command
line).
Cách 1 có ưu điểm là chương trình có thể chạy phân tán tuy nhiên mất nhiều
thời gian cho việc phát triển hơn. Cách 2 có nhược điểm là Z3 và JPF phải chạy
trên cùng một máy tuy nhiên ưu điểm là cài đặt tốn ít thời gian hơn.
Cả 2 cách đều phải giải quyết một vấn đề đó là chuyển đổi các ràng buộc
hiện thời của JPF sang SMT – LIB sau đó sử dụng Z3 để lấy kết quả về.
Trong luận văn này sẽ sử dụng cách 2 để cài đặt chương trình.
3.2 Kiến trúc hệ thống
Như ta đã biết JPF hiện nay đang sử dụng một số các công cụ tìm lời giải
viết bằng Java như là: Choco, IAsolver. Vì vậy ý tưởng của việc thiết kế hệ thống
là ta sẽ xây dựng một wrapper, wrapper này là giao diện để liên kết giữa JPF và
Z3. Wrapper sẽ tương tác với Z3 tương tư như Choco hay IAsolver.
Kiến trúc hệ thống được mô tả như hình 3-1 bên dưới:
Do Drive thay đổi chính sách, nên một số link cũ yêu cầu duyệt download. các bạn chỉ cần làm theo hướng dẫn.
Password giải nén nếu cần: ket-noi.com | Bấm trực tiếp vào Link để tải:
You must be registered for see links
Last edited by a moderator: