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 |