Luận Văn Thạc Sĩ Mở Rộng Javapathfinder Với Z3 Để Sinh Tự Động Dữ Liệu Kiếm Thử Chương Trình Java

Mở Rộng Javapathfinder Với Z3 Để Sinh Tự Động Dữ Liệu Kiếm Thử Chương Trình Java​

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 phương thức để 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).

• Luận văn thạc sĩ Công nghệ thông tin
• Chuyên ngành Công nghệ Phần mềm
• Người hướng dẫn khoa học: TS. Trương Anh Hoàng
• Tác giả: Phùng Thanh Sơn
• Số trang: 55
• Kiểu file: PDF
• Ngôn ngữ: Tiếng Việt
• Đại học Quốc gia Hà Nội 2010

Link Download
http://dlib.vnu.edu.vn/iii/cpro/DigitalItemViewPage.external?lang=vie&sp=1056523
https://drive.google.com/drive/folders/1yLBzZ1rSQoNjmWeJTM6cEZ3WGQHg04L1