Mở rộng JavaPathFinder với Z3 để sinh tự động dữ liệu kiểm thử chương trình Java

DSpace/Manakin Repository

Mở rộng JavaPathFinder với Z3 để sinh tự động dữ liệu kiểm thử chương trình Java

Show full item record


Title: Mở rộng JavaPathFinder với Z3 để sinh tự động dữ liệu kiểm thử chương trình Java
Author: Phùng Thanh, Sơn
Abstract: Nghiên cứu và nắm bắt được cách phát triển để mở rộng JavaPathFinder (JPF). Nắm bắt được thực thi tượng trưng để sinh tự động dữ liệu kiểm thử. Nghiên cứu lý thuyết tính thỏa mãn (SMT). Lý thuyết này đã được sử dụng để giải quyết nhiều bài toán trong công nghệ phần mềm: • Kiểm chứng chương trình (Program Verification) • Khám phá chương trình (Program Exploration) • Mô hình hóa phần mềm (Software Modeling) • Sinh các ca kiểm thử (Test Case Generation) Nắm bắt được SMT – Lib một thư viện chuẩn cho các công cụ tìm lời giải cho SMT, từ đó sử dụng SMT-Lib như là một định dạng dữ liệu chuẩn để trao đổi giữa Z3 và JPF. Tìm hiểu Z3, biết cách sử dụng cũng như ưu điểm, nhược điểm để từ đó tích hợp với JPF. Kết quả mới: Mở rộng JPF với Z3 để sinh dữ liệu kiểm thử chương trình Java. Điều này sẽ giúp cho JPF sinh được dữ liệu kiểm thử cho nhiều chương trình Java hơn. Công cụ mới sẽ giải được chương trình với đại số phi tuyến ở mức độ giới hạn, vì còn phụ thuộc vào độ phức tạp của điều kiện đường đi.
Description: Nghiên cứu và nắm bắt được cách phát triển để mở rộng JavaPathFinder (JPF). Nắm bắt được thực thi tượng trưng để sinh tự động dữ liệu kiểm thử. Nghiên cứu lý thuyết tính thỏa mãn (SMT). Lý thuyết này đã được sử dụng để giải quyết nhiều bài toán trong công nghệ phần mềm: • Kiểm chứng chương trình (Program Verification) • Khám phá chương trình (Program Exploration) • Mô hình hóa phần mềm (Software Modeling) • Sinh các ca kiểm thử (Test Case Generation) Nắm bắt được SMT – Lib một thư viện chuẩn cho các công cụ tìm lời giải cho SMT, từ đó sử dụng SMT-Lib như là một định dạng dữ liệu chuẩn để trao đổi giữa Z3 và JPF. Tìm hiểu Z3, biết cách sử dụng cũng như ưu điểm, nhược điểm để từ đó tích hợp với JPF. Kết quả mới: Mở rộng JPF với Z3 để sinh dữ liệu kiểm thử chương trình Java. Điều này sẽ giúp cho JPF sinh được dữ liệu kiểm thử cho nhiều chương trình Java hơn. Công cụ mới sẽ giải được chương trình với đại số phi tuyến ở mức độ giới hạn, vì còn phụ thuộc vào độ phức tạp của điều kiện đường đi.
URI: http://hdl.handle.net/123456789/2810
Date: 2010

Files in this item

Files Size Format View
Phung_Thanh_Son_Thong_tin_luan_van_thac_si.pdf 142.4Kb PDF View/Open

This item appears in the following Collection(s)

Show full item record

Search DSpace


Advanced Search

Browse

My Account