- Nghiên cứu phương pháp sinh dữ liệu kiểm thử phần mềm dựa trên kỹ thuật kiểm chứng. - ngành: Công nghệ phần mềm. - Trình bày cơ sở lý luận về kiểm định phần mềm và các nhóm kiểm định phần mềm. - Giới thiêu về JPF, kiến trúc của JPF, cách mở rộng, phát triển trên JPF.. - Ngoài ra giới thiệu về thực thi tượng trưng để sinh dữ liệu kiểm thử cho chương trình trong JPF cũng như cho phép sinh tự động dữ liệu kiểm thử chương trình Java.. - Công nghệ phần mềm. - Dữ liệu. - Kiểm chứng mô hình. - Phần mềm. - 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ử, kiểm chứng 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.. - 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 chứng và kiểm thử phần mềm. - 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ử. - Vì vậy tác giả đặt ra vấn đề: Liệu có thể sử dụng Z3 để kiểm chứng 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 chương trình 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. - Sau đó bước đầu tích hợp thành công Z3 và JPF để 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. - Nội dung: Giới thiêu JPF là gì? Kiến trúc của JPF, cách mở rộng, phát triển trên JPF.. - Ngoài ra còn một phần rất quan trọng đó là giới thiệu về thực thi tượng trưng để sinh dữ liệu kiểm thử cho chương trình trong JPF. - Mở rộng này sẽ cho phép sinh tự động dữ liệu kiểm thử chương trình Java.. - Kết luận và hướng phát triển của luận văn