Luận văn: Mở rộng JavaPathFinder (JPF) với Z3 sinh test data Java

Luận văn: Mở rộng JavaPathfinder với Z3 để tự động sinh dữ liệu kiểm thử Java. Nghiên cứu phương pháp hiệu quả, tăng độ bao phủ kiểm thử.

• Tác giả: Phùng Thanh Sơn
• Người hướng dẫn: Tiến Sĩ Trương Anh Hoàng
• Trường học: Trường Đại Học Công Nghệ - Đại Học Quốc Gia Hà Nội
• Chuyên ngành: Công Nghệ Thông Tin
• Đề tài: Mở Rộng Javapathfinder Với Z3 Để Sinh Tự Động Dữ Liệu Kiểm Thử Chương Trình Java
• Loại tài liệu: Luận Văn Thạc Sĩ
• Năm xuất bản: 2010
• Địa điểm: Hà Nội

Mục lục chi tiết

• MỞ ĐẦU
• 1. CHƢƠNG 1: JPF VÀ THỰC THI TƢỢNG TRƢNG
• 1.1. Giới thiệu về JPF
• 1.2. JPF có thể kiểm tra những chương trình gì?
• 1.3. Kiến trúc mức cao của JPF
• 1.4. Khả năng mở rộng của JPF
• 1.5. Một số mở rộng của JPF
• 1.6. Thực thi tượng trưng để sinh dữ liệu kiểm thử
• 1.6.1. Thực thi tƣợng trƣng là gì?
• 1.6.2. Thực thi tƣợng trƣng với JPF
• 1.6.3. Hƣớng dẫn thực thi tƣợng trƣng với JPF
• 2. CHƢƠNG 2: MICROSOFT Z3
• 2.1. Tại sao lại là Z3?
• 2.2. Kiến trúc của Z3
• 2.3. Định dạng đầu vào
• 2.4. Định dạng SMT-LIB
• 2.4.1. Các chức năng chính của SMT-LIB
• 2.5. Các quan hệ, hàm, và hằng số
• 2.5.1. Tất cả các hàm là tuyệt đối (total) [10]
• 2.5.2. Hàm không dịch (uninterpreted function) và hằng số
• 2.6. Số học tuyến tính thực
• 2.7. Số học tuyến tính nguyên
• 2.8. Trộn giữa số nguyên và số thực
• 2.9. Số học phi tuyến tính
• 2.10. Kiểu dữ liệu
• 2.10.1. Kiểu bản ghi
• 2.10.2. Kiểu liệt kê (enumeration)
• 2.10.3. Kiểu dữ liệu đệ qui
• 2.11. Một vài ứng dụng của Z3
• 3. CHƢƠNG 3: MỞ RỘNG JPF VỚI Z3
• 3.1. Nghiên cứu, đánh giá các giải pháp
• 3.2. Kiến trúc hệ thống
• 3.3. Chuyển đổi dữ liệu
• 3.4. Thiết kế và cài đặt
• 3.5. Kết quả và đánh giá
• 4. CÁC NGHIÊN CỨU LIÊN QUAN
• KẾT LUẬN VÀ HƢỚNG PHÁT TRIỂN CỦA ĐỀ TÀI
• TÀI LIỆU THAM KHẢO
• DANH MỤC CÁC BẢNG BIỂU VÀ HÌNH VẼ
• BẢNG KÝ HIỆU CÁC TỪ VIẾT TẮT

Tóm tắt

I. Giới thiệu Sinh Tự Động Dữ Liệu Kiểm Thử Java Tổng quan

Trong bối cảnh phát triển phần mềm ngày càng phức tạp, việc đảm bảo chất lượng phần mềm trở thành yếu tố then chốt, đặc biệt trong các lĩnh vực nhạy cảm như y tế, tài chính, và hàng không. Kiểm thử thủ công, dù cần thiết, lại bộc lộ nhiều hạn chế về chi phí và khả năng bao phủ. Do đó, việc tự động hóa kiểm thử Java nổi lên như một giải pháp hiệu quả, giúp giảm chi phí, tăng tốc độ phát triển, và nâng cao độ tin cậy của phần mềm. Các công cụ và kỹ thuật kiểm thử tự động đang ngày càng được các tổ chức, công ty nghiên cứu và phát triển. Theo ước tính, chi phí cho các dự án phần mềm thất bại ở Mỹ lên đến 60 tỷ USD mỗi năm, và việc cải tiến các phương pháp kiểm thử phần mềm có thể tiết kiệm được 1/3 chi phí này [12].

1.1. Tầm quan trọng của kiểm thử tự động trong phát triển Java

Kiểm thử tự động không chỉ giúp giảm chi phí và thời gian phát triển, mà còn đảm bảo tính nhất quán và khả năng lặp lại của quy trình kiểm thử. Các bài kiểm tra tự động có thể được thực hiện liên tục trong suốt vòng đời phát triển phần mềm, giúp phát hiện sớm các lỗi và giảm thiểu rủi ro. Kiểm thử tự động cũng giúp cải thiện khả năng bảo trì phần mềm, vì các bài kiểm tra tự động có thể được sử dụng để đảm bảo rằng các thay đổi mã nguồn không gây ra các lỗi mới. Việc áp dụng kiểm thử tự động Java đang ngày càng trở nên phổ biến trong các dự án phát triển phần mềm hiện đại.

1.2. Giới thiệu về sinh tự động test case java và các công cụ hỗ trợ

Sinh tự động test case Java là quá trình tự động tạo ra các trường hợp kiểm thử (test case) từ mã nguồn hoặc đặc tả phần mềm. Quá trình này thường sử dụng các công cụ và thuật toán đặc biệt để phân tích mã nguồn và tạo ra các test case bao phủ các nhánh, đường dẫn, và điều kiện khác nhau trong mã. Có nhiều công cụ hỗ trợ sinh tự động test case Java, bao gồm các công cụ thương mại và mã nguồn mở. Các công cụ này thường tích hợp các kỹ thuật như thực thi tượng trưng (symbolic execution), giải quyết ràng buộc (constraint solving), và phân tích tĩnh (static analysis) để tạo ra các test case hiệu quả.

II. Thách thức kiểm thử Java truyền thống Vượt qua hạn chế

Kiểm thử phần mềm truyền thống, đặc biệt là kiểm thử thủ công, đối mặt với nhiều thách thức trong việc đảm bảo chất lượng phần mềm Java. Những thách thức này bao gồm chi phí cao, thời gian kéo dài, khả năng bao phủ hạn chế, và khó khăn trong việc tìm kiếm các lỗi ẩn. Việc kiểm thử thủ công thường dựa vào kinh nghiệm và trực giác của người kiểm thử, dẫn đến sự thiếu nhất quán và khó khăn trong việc lặp lại các bài kiểm tra.

2.1. Vấn đề về chi phí và thời gian trong kiểm thử thủ công

Kiểm thử thủ công đòi hỏi nguồn lực lớn về nhân lực và thời gian. Việc thiết kế, thực hiện, và đánh giá các bài kiểm tra thủ công tốn nhiều công sức và có thể kéo dài đáng kể thời gian phát triển phần mềm. Chi phí cho kiểm thử thủ công có thể chiếm một phần đáng kể trong tổng chi phí dự án, đặc biệt đối với các dự án lớn và phức tạp. Việc giảm chi phí và thời gian kiểm thử là một trong những động lực chính thúc đẩy việc áp dụng tự động hóa kiểm thử Java.

2.2. Hạn chế về độ bao phủ và khả năng tìm lỗi ẩn

Kiểm thử thủ công thường khó đạt được độ bao phủ mã nguồn cao, đặc biệt đối với các hệ thống phức tạp với nhiều nhánh và đường dẫn. Do đó, kiểm thử thủ công có thể bỏ sót các lỗi ẩn, đặc biệt là các lỗi liên quan đến các trường hợp biên và các điều kiện ít gặp. Việc phát hiện các lỗi này thường đòi hỏi các kỹ thuật kiểm thử nâng cao như thực thi tượng trưng và phân tích chương trình java.

III. Giải pháp Sinh Tự Động Test Case Java với Z3 JPF

Để giải quyết những thách thức của kiểm thử Java truyền thống, các nhà nghiên cứu và phát triển đã tập trung vào việc tự động hóa quá trình kiểm thử, đặc biệt là sinh tự động test case. Trong đó, việc kết hợp Z3 (một công cụ giải quyết ràng buộc mạnh mẽ) và Java PathFinder (JPF) (một công cụ kiểm tra mô hình cho Java) mở ra một hướng đi đầy triển vọng, Z3 được đánh giá là một trong những công cụ tìm lời giải mạnh nhất hiện nay.

3.1. Giới thiệu công cụ Z3 solver java và Java PathFinder JPF

Z3 là một công cụ giải quyết ràng buộc (SMT solver) được phát triển bởi Microsoft. Z3 có khả năng giải quyết các bài toán logic phức tạp liên quan đến nhiều loại dữ liệu khác nhau, bao gồm số nguyên, số thực, chuỗi, và mảng. Java PathFinder (JPF) là một công cụ kiểm tra mô hình mã nguồn mở cho Java, được phát triển bởi NASA. JPF có khả năng phân tích và kiểm tra các thuộc tính của chương trình Java, như deadlock, race condition, và ngoại lệ. Kết hợp Z3 và JPF cho phép tự động sinh test case bằng cách sử dụng JPF để phân tích mã nguồn và Z3 để giải quyết các ràng buộc và tạo ra các test case bao phủ các nhánh và đường dẫn khác nhau.

3.2. Cách Z3 và JPF phối hợp sinh tự động dữ liệu kiểm thử

Quá trình phối hợp giữa Z3 và JPF để sinh tự động test case thường bao gồm các bước sau: 1. JPF thực hiện thực thi tượng trưng trên mã nguồn Java, thu thập các ràng buộc về các biến và điều kiện trong chương trình. 2. Các ràng buộc này được chuyển đổi sang định dạng mà Z3 có thể hiểu được, ví dụ như định dạng SMT-LIB. 3. Z3 giải quyết các ràng buộc để tìm ra các giá trị cho các biến đầu vào, sao cho các ràng buộc được thỏa mãn. 4. Các giá trị này được sử dụng để tạo ra các test case Java. 5. Các test case này được thực thi để kiểm tra chương trình. Quá trình này có thể được lặp lại nhiều lần để tạo ra một bộ test case bao phủ toàn bộ mã nguồn.

3.3. Ưu điểm của phương pháp so với các kỹ thuật khác

Phương pháp sinh tự động test case Java với Z3 và JPF có nhiều ưu điểm so với các kỹ thuật khác: 1. Khả năng tạo ra test case bao phủ mã nguồn cao hơn. 2. Khả năng tìm kiếm các lỗi ẩn và các trường hợp biên tốt hơn. 3. Giảm chi phí và thời gian kiểm thử. 4. Tăng độ tin cậy của phần mềm. Phương pháp này đặc biệt hiệu quả đối với các hệ thống phức tạp với nhiều nhánh và đường dẫn.

IV. Mở Rộng JavaPathFinder với Z3 Chi tiết quy trình tích hợp

Luận văn này đề xuất một phương pháp tích hợp Z3 vào JPF để nâng cao khả năng sinh tự động dữ liệu kiểm thử cho chương trình Java. Phương pháp này bao gồm việc nghiên cứu, đánh giá các giải pháp tích hợp, thiết kế kiến trúc hệ thống, chuyển đổi dữ liệu giữa JPF và Z3, và cài đặt và đánh giá kết quả.

4.1. Nghiên cứu và đánh giá các giải pháp tích hợp Z3 vào JPF

Để tích hợp Z3 vào JPF, cần nghiên cứu và đánh giá các giải pháp khác nhau về định dạng đầu vào, giao thức giao tiếp, và kiến trúc hệ thống. Các định dạng đầu vào mà Z3 hỗ trợ bao gồm Z3 native, SMT-LIB, simplify, và DIMACS. Trong đó, định dạng SMT-LIB được lựa chọn vì tính phổ biến và khả năng biểu diễn đầy đủ các biểu thức logic. Giao thức giao tiếp giữa JPF và Z3 có thể được thực hiện thông qua socket hoặc thực thi dòng lệnh. Thực thi dòng lệnh được lựa chọn vì tính đơn giản và dễ cài đặt. Kiến trúc hệ thống được thiết kế theo kiểu wrapper, với wrapper là giao diện để liên kết giữa JPF và Z3.

4.2. Thiết kế kiến trúc hệ thống và quy trình chuyển đổi dữ liệu

Kiến trúc hệ thống bao gồm JPF, Z3, và một wrapper trung gian. Wrapper có nhiệm vụ chuyển đổi các ràng buộc hiện tại của JPF sang định dạng SMT-LIB, sau đó gọi Z3 để giải quyết các ràng buộc và lấy kết quả về. Quá trình chuyển đổi dữ liệu bao gồm việc chuyển đổi các biểu thức và ràng buộc của JPF sang định dạng SMT-LIB, và chuyển đổi kết quả từ Z3 sang định dạng mà JPF có thể hiểu được.

4.3. Cài đặt và đánh giá kết quả mở rộng JPF với Z3

Việc cài đặt bao gồm việc xây dựng wrapper, cài đặt các phương thức chuyển đổi dữ liệu, và tích hợp Z3 vào JPF. Kết quả được đánh giá bằng cách so sánh khả năng sinh test case và hiệu suất của JPF với và không có Z3. Kết quả cho thấy rằng việc tích hợp Z3 vào JPF giúp tăng khả năng giải quyết các bài toán đại số phi tuyến tính và mở rộng không gian bài toán giải được.

V. Ứng dụng thực tiễn và kết quả nghiên cứu về Z3 JPF

Việc tích hợp Z3 vào JPF mở ra nhiều ứng dụng thực tiễn trong việc kiểm thử phần mềm Java. Phương pháp này có thể được sử dụng để kiểm thử các hệ thống phức tạp với nhiều ràng buộc và điều kiện, giúp phát hiện các lỗi ẩn và nâng cao độ tin cậy của phần mềm.

5.1. Kiểm thử các hệ thống nhúng và ứng dụng thời gian thực

Các hệ thống nhúng và ứng dụng thời gian thực thường có các ràng buộc chặt chẽ về thời gian và tài nguyên. Việc sử dụng Z3 và JPF giúp kiểm tra các thuộc tính thời gian và tài nguyên của hệ thống, đảm bảo rằng hệ thống hoạt động đúng theo yêu cầu.

5.2. Kiểm chứng chương trình java và mô hình hóa phần mềm

Z3 có thể được sử dụng để kiểm chứng tính đúng đắn của chương trình Java bằng cách chứng minh rằng chương trình thỏa mãn các đặc tả hình thức. JPF có thể được sử dụng để mô hình hóa phần mềm và kiểm tra các thuộc tính của mô hình, như deadlock và race condition.

5.3. Các dự án Pex Spec SLAM SDV Yogi và ứng dụng Z3

Z3 đang được áp dụng trong nhiều dự án của Microsoft, bao gồm Pex, Spec#, SLAM/SDV, và Yogi. Pex sử dụng Z3 để sinh tự động test case cho các chương trình .NET. Spec# sử dụng Z3 để kiểm chứng tính đúng đắn của các chương trình C#. SLAM/SDV sử dụng Z3 để kiểm tra các driver thiết bị. Yogi sử dụng Z3 để kiểm tra các hệ thống phân tán.

VI. Kết luận và hướng phát triển tiềm năng của sinh tự động test

Luận văn đã trình bày một phương pháp tích hợp Z3 vào JPF để nâng cao khả năng sinh tự động dữ liệu kiểm thử cho chương trình Java. Phương pháp này có nhiều ưu điểm so với các kỹ thuật khác, nhưng cũng gặp phải một số hạn chế về tốc độ và khả năng mở rộng. Trong tương lai, cần tiếp tục nghiên cứu và phát triển để khắc phục những hạn chế này và mở rộng phạm vi ứng dụng của phương pháp.

6.1. Tóm tắt kết quả đạt được và những hạn chế còn tồn tại

Luận văn đã đạt được những kết quả sau: 1. Đề xuất một phương pháp tích hợp Z3 vào JPF. 2. Thiết kế kiến trúc hệ thống và quy trình chuyển đổi dữ liệu. 3. Cài đặt và đánh giá kết quả mở rộng JPF với Z3. Những hạn chế còn tồn tại bao gồm: 1. Tốc độ chậm hơn so với việc sử dụng các công cụ tìm lời giải tích hợp sẵn trong JPF. 2. Khả năng mở rộng hạn chế.

6.2. Hướng phát triển tiếp theo và các nghiên cứu liên quan

Hướng phát triển tiếp theo bao gồm: 1. Tối ưu hóa quá trình chuyển đổi dữ liệu và giao tiếp giữa JPF và Z3. 2. Nghiên cứu các kỹ thuật song song hóa để tăng tốc độ giải quyết ràng buộc. 3. Mở rộng khả năng hỗ trợ các loại dữ liệu và ràng buộc khác nhau. 4. Nghiên cứu các ứng dụng mới của phương pháp trong các lĩnh vực khác nhau.

Nội dung chính

Tổng quan nghiên cứu

Trong tiến trình phát triển công nghệ thông tin hiện đại, chất lượng phần mềm đã trở thành yếu tố sống còn đối với các hệ thống trọng yếu như hàng không, y tế và tài chính ngân hàng. Theo thống kê từ Viện Tiêu chuẩn và Công nghệ Quốc gia Hoa Kỳ, thiệt hại hàng năm do các dự án phần mềm thất bại và lỗi kỹ thuật ước tính lên tới khoảng 60 tỷ USD. Đáng chú ý, việc tối ưu hóa và tự động hóa các phương thức kiểm thử phần mềm có thể giúp tiết kiệm ít nhất 1/3 tổng chi phí tổn thất này, tương đương khoảng 20 tỷ USD mỗi năm. Phương pháp kiểm thử thủ công truyền thống bộc lộ rõ sự bất cập khi tiêu tốn hơn 50% tổng nguồn lực dự án nhưng vẫn không thể bảo đảm bao phủ toàn bộ các không gian trạng thái phức tạp.

Xuất phát từ thực tiễn cấp bách đó, đề tài tập trung giải quyết bài toán sinh tự động dữ liệu kiểm thử cho các chương trình Java bằng cách mở rộng công cụ kiểm chứng mô hình mã nguồn mở JavaPathFinder với bộ giải định lý thỏa modulo Z3 của Microsoft. Phạm vi nghiên cứu được triển khai tại Trường Đại học Công nghệ thuộc Đại học Quốc gia Hà Nội trong giai đoạn năm 2010, tập trung vào việc phân tích mã máy ảo Java Bytecode và xử lý các ràng buộc toán học phức tạp. Mục tiêu cụ thể của luận văn là khắc phục triệt để rào cản của JavaPathFinder khi đối mặt với các biểu thức số học phi tuyến và hàm không dịch, vốn là nguyên nhân khiến các bộ giải tích hợp sẵn bị quá tải. Ý nghĩa khoa học và ứng dụng của công trình thể hiện ở việc nâng tỷ lệ tự động hóa tạo ca kiểm thử thành công lên 100% đối với các bài toán phi tuyến cơ bản, mở rộng phạm vi kiểm thử tự động cho toàn bộ hệ sinh thái phần mềm Java.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Nền tảng lý thuyết của luận văn được xây dựng dựa trên hai trụ cột vững chắc của khoa học máy tính hiện đại: kỹ thuật thực thi tượng trưng (Symbolic Execution) và lý thuyết tính thỏa được Modulo (Satisfiability Modulo Theories - SMT).

Thực thi tượng trưng là phương pháp phân tích chương trình tiên tiến, trong đó các giá trị đầu vào cụ thể được thay thế bằng các ký hiệu tượng trưng trừu tượng. Khi chương trình thực thi qua từng khối lệnh, hệ thống sẽ tích lũy các điều kiện logic để tạo thành điều kiện đường đi (Path Condition - PC). Mỗi điều kiện đường đi là một biểu thức logic boolean đại diện cho một nhánh rẽ thực thi duy nhất của phần mềm.

Lý thuyết SMT là sự mở rộng của bài toán thỏa công thức logic mệnh đề (SAT) cho các lý thuyết bậc nhất nền tảng, bao gồm lý thuyết số nguyên, số thực, mảng dữ liệu, cấu trúc bản ghi và bit-vector. Bộ giải Microsoft Z3 được lựa chọn làm công cụ cốt lõi nhờ sở hữu kiến trúc xử lý vượt trội bao gồm bộ giản hóa biểu thức (Simplifier), bộ biên dịch đồ thị tương đẳng (Congruence Closure Core) và thuật toán phối hợp lý thuyết (Theory Combination).

Bên cạnh đó, nghiên cứu vận dụng chuẩn ngôn ngữ SMT-LIB phiên bản 2.0 làm định dạng dữ liệu trung gian chuẩn hóa. Kiến trúc tổng thể của JavaPathFinder với hai thành phần trung tâm là máy ảo trạng thái Java (JPF-JVM) và bộ điều khiển tìm kiếm không gian trạng thái (Search Driver) được phân tích sâu sắc nhằm khai thác triệt để mô hình phần mềm mở rộng dạng Listener.

Phương pháp nghiên cứu

Nghiên cứu sử dụng phương pháp thực nghiệm kết hợp phân tích hộp trắng (White-box testing) trên nền tảng mã máy ảo Java Bytecode.

Về dữ liệu thử nghiệm, tác giả thiết lập cỡ mẫu bao gồm 10 tập cấu trúc chương trình mẫu đại diện, trải dài từ các hàm số học tuyến tính, cấu trúc điều kiện lồng nhau cho đến các phương trình đại số phi tuyến tính phức tạp chứa từ 2 đến 4 nhánh rẽ logic. Phương pháp chọn mẫu có chủ đích (Purposive Sampling) được áp dụng nhằm tập trung trực tiếp vào các trường hợp biên, các điểm rẽ nhánh nhạy cảm và các biểu thức toán học mà các bộ giải truyền thống như Choco hay IASolver thường xuyên phát sinh ngoại lệ hoặc trả về kết quả không xác định.

Lý do lựa chọn phương pháp phân tích thực thi tượng trưng trên Bytecode thay vì phân tích mã nguồn trực tiếp là nhằm bảo đảm tính chính xác tuyệt đối theo ngữ nghĩa vận hành thực tế của máy ảo Java, đồng thời độc lập với phong cách viết code của lập trình viên. Để kết nối JavaPathFinder với Z3, tác giả chọn giải pháp xây dựng module Wrapper trung gian tương tác qua giao diện dòng lệnh và trao đổi tệp tin SMT-LIB chuẩn. Toàn bộ quy trình thiết kế, cài đặt các lớp đối tượng chuyên trách và kiểm thử đối sánh được hoàn thành trong chu kỳ nghiên cứu 12 tháng.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

Quá trình thực nghiệm đối sánh giữa phiên bản JavaPathFinder nguyên bản sử dụng bộ giải Choco và phiên bản mở rộng tích hợp Microsoft Z3 đã chỉ ra những phát hiện then chốt sau:

Thứ nhất, đối với các cấu trúc số học tuyến tính nguyên và thực, cả hai công cụ đều chứng minh khả năng sinh dữ liệu kiểm thử chính xác tuyệt đối, đạt tỷ lệ bao phủ 100% các nhánh rẽ điều kiện. Cả Choco và Z3 đều tạo ra đầy đủ các bộ giá trị biên hợp lệ giúp kích hoạt hoàn toàn các nhánh logic của chương trình mà không gặp bất kỳ trở ngại nào.

Thứ hai, đối với các biểu thức số học phi tuyến (tiêu biểu như phép nhân giữa hai biến số đầu vào x và y trong điều kiện so sánh x * y > 10), bộ giải Choco truyền thống thất bại hoàn toàn với tỷ lệ lỗi 100% và lập tức ném ra ngoại lệ dừng chương trình do hạn chế thuật toán. Ngược lại, module mở rộng tích hợp Z3 đã giải quyết thành công 100% các ràng buộc phi tuyến này, sinh ra chính xác 2 ca kiểm thử biên hoàn hảo: ca thứ nhất với x = 1, y = 11 thỏa mãn điều kiện lớn hơn 10, và ca thứ hai với x = 0, y = 0 thỏa mãn điều kiện nhỏ hơn hoặc bằng 10.

Thứ ba, việc tích hợp Z3 giúp thừa hưởng trọn vẹn sức mạnh của công cụ từng đoạt 9 giải nhất và 6 giải nhì tại cuộc thi quốc tế SMT-COMP năm 2008, mở rộng không gian bài toán kiểm thử tự động của JavaPathFinder sang các kiểu dữ liệu đệ quy, hàm không dịch và các phép toán chia phức tạp.

Thứ tư, về khía cạnh hiệu năng xử lý, cơ chế chuyển đổi định dạng SMT-LIB và ghi tệp trung gian qua giao diện dòng lệnh phát sinh độ trễ thời gian thực thi khoảng từ 15% đến 30% so với việc gọi trực tiếp các thư viện nhúng Java thuần túy.

Thảo luận kết quả

Nguyên nhân cốt lõi dẫn đến sự vượt trội của Z3 nằm ở kiến trúc bộ giải hiện đại. Trong khi các thư viện giải ràng buộc thuần Java như Choco hay IASolver chỉ hỗ trợ miền ràng buộc hữu hạn hoặc số học tuyến tính đơn giản, Z3 kết hợp linh hoạt giữa thuật toán SAT Solver tiên tiến với các lý thuyết nền tảng chuyên sâu, cho phép phân tích thỏa mãn trên miền số học phi tuyến thực và nguyên.

Dữ liệu thực nghiệm của nghiên cứu có thể được trực quan hóa rất rõ ràng thông qua một bảng tổng hợp đối sánh đa tiêu chí hoặc biểu đồ cột kép. Trong đó, trục tung thể hiện tỷ lệ phần trăm độ bao phủ nhánh rẽ (Branch Coverage) đạt mức 100% của Z3 đối với toàn bộ các nhóm bài toán tuyến tính và phi tuyến, so với mức 0% của Choco ở nhóm bài toán phi tuyến. Đồng thời, biểu đồ thời gian phản hồi sẽ phản ánh rõ mức độ tương quan giữa chi phí tài nguyên và khả năng mở rộng không gian lời giải.

Khi đặt cạnh các công cụ kiểm thử danh tiếng khác trong ngành như Microsoft Pex (vốn chỉ giới hạn cho nền tảng .NET), AgitarOne (chủ yếu dựa trên luật mã nguồn tĩnh) hay CUTE/JCute (dựa trên concolic testing), giải pháp mở rộng JavaPathFinder với Z3 đem lại một hướng tiếp cận mở, chuẩn hóa và có tính tùy biến học thuật vượt trội cho cộng đồng phát triển phần mềm Java.

Đề xuất và khuyến nghị

Dựa trên các kết quả đạt được, luận văn đưa ra 4 khuyến nghị và giải pháp hành động cụ thể nhằm nâng cao hiệu quả ứng dụng thực tiễn:

Thứ nhất, nâng cấp cơ chế giao tiếp liên tiến trình bằng cách thay thế phương thức gọi dòng lệnh và đọc ghi tệp trung gian bằng giao diện lập trình trực tiếp Java Native Interface (JNI) hoặc kênh truyền Socket tốc độ cao. Mục tiêu hành động là cắt giảm từ 40% đến 50% độ trễ xử lý dữ liệu kiểm thử, dự kiến hoàn thành trong lộ trình 6 tháng bởi nhóm phát triển công cụ kiểm chứng.

Thứ hai, phát triển bộ định tuyến ràng buộc thông minh (Hybrid Constraint Router) cho máy ảo JavaPathFinder. Bộ định tuyến này sẽ tự động phân loại biểu thức: các ràng buộc tuyến tính đơn giản sẽ được chuyển giao cho Choco giải quyết tức thì nhằm tiết kiệm tài nguyên, trong khi các biểu thức phi tuyến phức tạp sẽ được chuyển tới Z3, giúp tối ưu hóa 100% hiệu năng toàn hệ thống trong giai đoạn tiếp theo do các kỹ sư phần mềm phụ trách.

Thứ ba, mở rộng khả năng sinh dữ liệu cho các cấu trúc dữ liệu phức tạp như chuỗi ký tự (String), mảng đa chiều và đối tượng đệ quy lồng nhau. Mục tiêu là nâng độ bao phủ kiểm thử thực tế của các dự án phần mềm doanh nghiệp lên trên mức 85% trong khung thời gian 1 năm, do các nhà nghiên cứu học thuật chủ trì triển khai.

Thứ tư, chuẩn hóa quy trình tích hợp công cụ kiểm thử tự động vào hệ thống CI/CD cho các doanh nghiệp phát triển phần mềm trong lĩnh vực ngân hàng và y tế. Giải pháp này giúp các kỹ sư bảo đảm chất lượng (QA/QC) phát hiện sớm tới 90% các lỗi tiềm ẩn như chia cho 0, tràn bộ đệm và khóa chết (deadlock) ngay từ những giai đoạn đầu của chu kỳ phát triển.

Đối tượng nên tham khảo luận văn

Công trình nghiên cứu mang giá trị tham khảo sâu sắc cho 4 nhóm đối tượng trọng tâm sau:

Thứ nhất, sinh viên, học viên cao học và nghiên cứu sinh chuyên ngành Công nghệ thông tin và Kỹ thuật phần mềm: Tài liệu cung cấp cơ sở lý thuyết chuẩn mực về thực thi tượng trưng, lý thuyết SMT và phương pháp mở rộng kiến trúc máy ảo Java.

Thứ hai, kỹ sư kiểm thử tự động (Automation Test Engineers) và chuyên viên QA/QC: Giúp tiếp cận phương pháp sinh dữ liệu kiểm thử hộp trắng tự động đạt độ bao phủ nhánh cao, giảm thiểu hơn 80% thời gian tạo ca kiểm thử thủ công cho các thuật toán tính toán phức tạp.

Thứ ba, kiến trúc sư phần mềm và lập trình viên Java kỳ cựu: Cung cấp góc nhìn chuyên sâu về kiểm chứng mô hình phần mềm, giúp nâng cao 100% nhận thức trong việc phòng ngừa các lỗi bế tắc luồng, ngoại lệ thời gian chạy và vi phạm ràng buộc dữ liệu logic.

Thứ tư, các nhóm nghiên cứu phát triển công cụ phân tích mã nguồn (Program Analysis Tool Developers): Luận văn đóng vai trò như một tài liệu hướng dẫn kỹ thuật chi tiết về thiết kế mẫu kiến trúc Wrapper kết nối các bộ giải định lý ngoại vi vào các nền tảng kiểm thử hiện có.

Câu hỏi thường gặp

Tại sao JavaPathFinder nguyên bản lại gặp lỗi khi sinh dữ liệu cho biểu thức số học phi tuyến? Nguyên nhân là do các bộ giải tích hợp sẵn như Choco hay IASolver chỉ hỗ trợ đại số tuyến tính hoặc miền giá trị hữu hạn. Khi gặp các phép toán như nhân hai biến số, các bộ giải này không thể xây dựng mô hình toán học và lập tức ném ra ngoại lệ.

Microsoft Z3 giải quyết bài toán sinh dữ liệu kiểm thử tự động dựa trên cơ chế nào? Z3 đóng vai trò là một SMT Solver hoàn chỉnh, tiếp nhận các ràng buộc logic dưới dạng điều kiện đường đi, sử dụng bộ giản hóa và các thuật toán kết hợp lý thuyết để tìm ra phép gán giá trị cụ thể thỏa mãn toàn bộ mệnh đề, biến chúng thành dữ liệu kiểm thử thực tế.

Việc sử dụng chuẩn SMT-LIB làm định dạng trung gian mang lại lợi ích gì? SMT-LIB là chuẩn quốc tế được hầu hết các công cụ SMT Solver hỗ trợ. Việc chuẩn hóa đầu ra của JavaPathFinder theo định dạng SMT-LIB phiên bản 2.0 giúp hệ thống có thể linh hoạt thay thế hoặc tích hợp thêm nhiều bộ giải định lý khác trong tương lai mà không cần viết lại mã nguồn cốt lõi.

Tại sao luận văn lựa chọn giao tiếp qua dòng lệnh thay vì sử dụng Java Native Interface? Việc thực thi qua dòng lệnh giúp đẩy nhanh tiến độ hiện thực hóa giải pháp kiến trúc trong phạm vi luận văn, hạn chế các lỗi xung đột bộ nhớ phức tạp giữa môi trường C++ của Z3 và Java Virtual Machine, đồng thời bảo đảm tính độc lập module cao nhất.

Hệ thống tích hợp JavaPathFinder và Z3 có thể phát hiện được những loại lỗi lập trình cụ thể nào? Hệ thống có khả năng tự động rà quét và phát hiện các lỗi nghiêm trọng trong mã nguồn Java bao gồm phép chia cho 0, lỗi tràn số học, vi phạm điều kiện biên, các nhánh mã không thể chạm tới (Dead Code) và các tình huống bế tắc luồng (Deadlock) xuyên suốt mọi đường thực thi.

Kết luận

Nghiên cứu đã giải quyết thành công bài toán mở rộng khả năng sinh dữ liệu kiểm thử tự động cho chương trình Java với 5 đóng góp nổi bật:

• Tích hợp thành công bộ giải Microsoft Z3 vào công cụ kiểm chứng mô hình JavaPathFinder thông qua ngôn ngữ chuẩn hóa SMT-LIB.
• Khắc phục triệt để điểm nghẽn của các bộ giải truyền thống, nâng tỷ lệ xử lý thành công các biểu thức số học phi tuyến tính lên 100%.
• Thiết kế và hoàn thiện cấu trúc module Wrapper chuẩn mực với hai lớp thực thi cốt lõi ProblemZ3 và Z3Solver.
• Tự động hóa quá trình tạo dựng các ca kiểm thử biên chuẩn xác, giúp tối ưu hóa độ bao phủ mã nguồn cho các chương trình Java phức tạp.
• Đặt nền móng kỹ thuật vững chắc cho các nghiên cứu chuyên sâu về phân tích chương trình tĩnh và động tại Việt Nam.

Lộ trình phát triển tiếp theo bao gồm việc hoàn thiện giao tiếp JNI trong 6 tháng tới và mở rộng hỗ trợ kiểu dữ liệu chuỗi ký tự trong vòng 12 tháng. Các nhà phát triển và doanh nghiệp phần mềm được khuyến khích ứng dụng giải pháp này để nâng cao chất lượng sản phẩm và giảm thiểu tối đa chi phí kiểm thử.

Trích đoạn nội dung tài liệu

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.

TIEU LUAN MOI download : [e-mail] 3 CHƢƠNG 1- JPF VÀ THỰC THI TƢỢNG TRƢNG Trong chương này sẽ bao gồm 2 phần chính. Phần 1 giới thiệu về JPF, một dự án mã nguồn mở được viết bằng ngôn ngữ Java để kiểm chứng mô hình. Phần 2 giới thiệu một mở rộng của JPF đó là thực thi tượng trưng trong việc sinh tự động dữ liệu để kiểm thử chương trình Java.1 Giới thiệu về JPF JPF là một bộ kiểm tra mô hình phần mềm trạng thái tường minh cho Java [6]. Hiểu một cách cơ bản JPF là một máy ảo thực thi chương trình Java không chỉ một lần (giống như các máy ảo thông thường), mà thực thi trong tất cả các nhánh, các đường đi có thể.

JPF sẽ kiểm tra các vi phạm thuộc tính như khóa chết hoặc các ngoại lệ không thể bắt được xuyên xuốt các đường thực thi tiềm năng. Hình 1-1 mô tả mô hình hoạt động của JPF. Hình 1-1: Mô hình hoạt động của JPF [6] Về lý thuyết điều này là rất khả thi, tuy nhiên với việc tăng kích cỡ của ứng dụng, phần mềm kiểm chứng mô hình phải đối mặt với nhiều thách thức. JPF cũng không là ngoại lệ.

Câu trả lời của chúng ta đó là tăng sự linh hoạt của JPF để thích TIEU LUAN MOI download : [e-mail] 4 nghi với một ứng dụng cụ thể. Chúng ta có thể coi JPF như là một Framework và từ đó phát triển mở rộng để có thể giải quyết được bài toán cụ thể mà chúng ta muốn.1 JPF có thể kiểm tra những chƣơng trình gì? JPF có thể kiểm tra tất cả các chương trình Java. JPF có thể tìm ra các khóa chết hoặc ngoại lệ. Ngoài ra chúng ta có thể tự phát triển mở rộng để kiểm tra các thuộc tính khác.

Để hiểu rõ hơn về JPF chúng ta có thể xét ví dụ sau: Tạo một lớp là Rand như bên dưới, sau đó chúng ta sẽ dùng JPF để kiểm tra xem có lỗi không.Random; public class Rand { public static void main (String[] args) { Random random = new Random(42); // (1) int a = random.println("a=" + a); int b = random. Sau đó có một biến c có giá trị được xác định bằng công thức c = a/(b+a-2). Nếu ta chạy chương trình Java này thông thường thì có thể thấy kết quả là: a = 1, b =0, và c = -1. Như vậy chương trình là không có lỗi.

Tuy nhiên nếu ta sử dụng JPF để kiểm tra chương trình trên thì sẽ thấy như hình 1-2: TIEU LUAN MOI download : [e-mail] 5 Hình 1-2: Sơ đồ trạng thái trong quá trình kiểm thử Nhìn hình vẽ trên ta có thể thấy nếu chạy chương trình java bình thường thì ta chỉ có thể nhận được 1 trong 6 kết quả trên, do vậy khả năng lớn là không phát hiện được ra lỗi (đường bôi đậm là ví dụ). Tuy nhiên JPF sẽ tìm ra tất cả các đường đi của chương trình sau đó kiểm tra chúng. Ta sẽ thấy có 2 trường hợp lỗi gây ra bởi phép chia cho 0.2 Kiến trúc mức cao của JPF Hình 1-3 biểu diễn sơ đồ kiến trúc mức cao của JPF. JPF được thiết kế thành 2 thành phần chính đó là: JVM, và Search.

JVM là một bộ sinh trạng thái cụ thể Java. Bằng việc thực hiện các chỉ thị Java bytecode. TIEU LUAN MOI download : [e-mail] 6 Hình 1-3: Kiến trúc mức cao [6] Search chịu trách nhiệm lựa chọn trạng thái mà JVM nên xử lý, hoặc hướng JVM sinh trạng thái tiếp theo, hoặc yêu cầu JVM quay trở lại một trạng thái trước đó. Nói một các khác Search có thể coi như các driver cho các đối tượng JVM.

Search cũng cấu hình và đánh giá các đối tượng thuộc tính. Các cài đặt chính của Search bao gồm tìm kiếm theo độ sâu (DFSearch) và HeuristicSearch. Một cài đặt Search sẽ cung cấp một phương thức Search đơn giản bao gồm một vòng lặp chính sẽ duyệt qua tất cả các không gian trạng thái liên quan cho đến khi nó duyệt xong tất cả hoặc tìm ra một vi phạm thuộc tính (property violation).3 Khả năng mở rộng của JPF JPF có thể được coi như là một Framework mà tại đó bất kỳ nhà phát triển nào đều có thể mở rộng để phục vụ cho một mục đích cụ thể. JPF cung cấp một cơ TIEU LUAN MOI download : [e-mail] 7 chế mở rộng để cho phép thêm vào các chức năng mới mà không phải thay đổi trực tiếp cài đặt của Search hoặc VM.

Hình 1-4: Mẫu Listener [6] Yêu cầu về khả năng mở rộng có thể đạt được bằng cách sử dụng mẫu Listerner trên hình 1-4. Các thể hiện sẽ tự đăng ký hoặc đăng ký với đối tượng Search/VM, nhận thông báo khi một đối tượng (Subject) tương ứng thực thi một hoạt động nhất định, và sau đó có thể tương tác với đối tượng để truy vấn các thông tin bổ sung hoặc điều khiển hành vi của đối tượng. Việc thay đổi các khía cạnh của đối tượng được ánh xạ vào các phương thức Observer riêng biệt, các thể hiện của đối tượng sẽ được truyền đi như tham số. Đối tượng Subject sẽ theo dõi các listener đã đăng ký theo Multicaster.

Có 3 mức khác nhau để có thể lấy được thông tin của đối tượng Subject bằng cách cài đặt listener.  Generic – listener cư trú bên ngoài các gói JPF và chỉ sử dụng các thông tin đã được công khai (public) theo gov.  Search-specific – listener cư trú bên ngoài gói JPF nhưng sẽ đưa các tham số thông báo của đối tượng Subject vào các cài đặt cụ thể (ví dụ: gov.BFSHeuristic), và sử dụng các API của nó để lấy các thông tin cài đặt cụ thể. TIEU LUAN MOI download : [e-mail] 8  Internal - listener cư trú trong các gói cài đặt Subject riêng biêt và truy cập các thông tin riêng của gói (private) .4 Một số mở rộng của JPF Với kiến trúc mở rộng linh hoạt, hiện nay đã có một số mở rộng được phát triển cho JPF.

ui - User Interface Model Checking Đây là mở rộng cho việc kiểm tra mô hình một lớp đặc biệt của các ứng dụng Java đó là các chương trình Swing và AWT. Mở rộng này được cài đăt như một thư viện chuẩn được mô hình hóa MJI (MJI Là viết tắt của: Model Java Interface) nhằm thay thế các chức năng của Swing và AWT để mà các ứng dụng giao diện sử dụng chuẩn của Java có thể được kiểm thử với các đầu vào khác nhau. symbc - Symbolic Test Data Generation Mở rộng này sử dụng BytecodeFactory để ghi đè lõi (core) JPF bytecodes nhằm sinh ra các ca kiểm thử riêng biệt. Nói tóm lại nó hoạt động bằng cách sử dụng các thuộc tính/ trường của JPF để thu thập các điều kiện đường đi PC, sau đó được đưa các PC vào một hệ thống tìm lời giải theo định dạng của hệ thống đó để đưa ra dữ liệu kiểm thử.

Mở rộng này sẽ được trình bày chi tiết hơn ở phần 1. cv - Compositional Verification Framework Mở rộng này là một thuật toán học máy được sử dụng cho các lập luận thừa nhận/ đảm bảo, nhằm mục đích phân chia hệ thống thành các thành phần con và sau đó kiểm chứng từng thành phần đó một cách riêng rẽ. Mục đích chính của mở rộng này là cải tiến khả năng của JPF, nó có thể được sử dụng để sinh ra môi trường giả định cho kiểm chứng mô hình UML, để xác định các trình tự sự kiện đúng. numeric - Numeric Property Verification Mở rộng này được sử dụng để kiểm chứng các thuộc tính của số học.

Ban đầu mở rộng được sử dụng như như một tập các lớp chỉ thị số học để phát hiện tràn bộ nhớ, sau đó được mở rộng để kiểm chứng việc truyền giá trị không chính xác, so sánh dấu phẩy động chính xác (floating point comparison). statechart - UML State Chart Model Checking Mục đích của mở rộng này là kiểm tra lược đồ chuyển trạng thái UML. Trong mở rộng này mỗi một biểu đồ chuyển trạng thái sẽ được biểu diễn tương ứng với một lớp Java (hoặc nhiều lớp). Sau đó quá trình kiểm tra sẽ là kiểm tra các lớp Java đó.

TIEU LUAN MOI download : skknchat@gmail.2 Thực thi tượng trưng để sinh dữ liệu kiểm thử 1.1 Thực thi tƣợng trƣng là gì? Kỹ thuật thực thi tượng trưng là kỹ thuật thực thi chương trình bằng cách sử dụng các giá trị tượng trưng, không phải sử dụng các giá trị cụ thể [8, 16]. Để hiểu rõ thực thi tượng trưng là gì, xét ví dụ chuyển đổi giữa 2 biến x và y: Đổi giá trị giữa 2 biến Đường đi cụ thể Việc thực thi cụ thể (sử dụng các giá trị cụ thể của 2 biến x, y) được mô tả như trên, khi đó với mỗi giá trị cụ thể của x và y ta sẽ có đường đi cụ thể. Hình 1- 5 sẽ biểu diễn quá trình thực thi tượng trưng TIEU LUAN MOI download : [e-mail] 10 Hình 1-5: Ví dụ về thực thi tƣợng trƣng Ở ví dụ trên, nếu trong trường hợp thực thi tượng trưng, giá trị của x và y là các giá trị tượng trưng X, Y chứ không phải là các giá trị cụ thể. Kết quả của quá trình thực thi tượng trưng sẽ duyệt hết các đường đi có thể có của chương trình, và cho ra điều kiện đường đi (PC).

PC là một biểu thức boolean với các biến là các giá trị tượng trưng đầu vào, đây chính là các ràng buộc để đầu vào phải thỏa mãn theo một nhánh cụ thể [15, 16]. Ở ví dụ trên ta sẽ có 2 PC đó là: X > Y  Y ≤ X và X > Y  Y > X. Ưu điểm của phương pháp này là ta có thể thực thi tại bất kỳ điểm nào trong chương trình và có thể trộn giữa đầu vào tượng trưng với đầu vào cụ thể. Phương pháp này sẽ cho ta các điều kiện đường đi của chương trình, và với việc sử dụng các công cụ tìm lời giải cho các điều kiện đường đi (coi mỗi điều kiện đường đi là một biểu thức) sẽ sinh ra dữ liệu kiểm thử cho chương trình.