Xây dựng công cụ sinh dữ liệu thử tự động cho chương trình Java

Xây dựng công cụ sinh dữ liệu thử tự động cho chương trình Java

MỞ ĐẦU

1. Lý do chọn đề tài

Phần mềm hiện nay được sử dụng rộng rãi trong đời sống, công việc, nhiều lĩnh vực khoa học, kinh tế và xã hội. Vì vậy, việc đảm bảo rằng phần mềm đáp ứng mong muốn của người sử dụng là rất quan trọng. Kiểm thử phần mềm là một trong những hoạt động cơ bản nhằm đảm bảo chất lượng phần mềm.

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.

Một số lợi ích có thể kể đến của kiểm thử tự động như: cải thiện hiệu quả công việc, cải thiện tính chính xác, cải thiện chất lượng kiểm thử và chất lượng của phần mềm. Tại các doanh nghiệp tư nhân hiện tại, công việc kiểm thử phần mềm đơn vị (unit test) thường được các lập trình viên thực hiện ngay trong quá trình viết mã nguồn của chương trình. Vì vậy dẫn đến một số vấn đề như sau:

• Không đảm bảo được tính khách quan.
• Các lập trình viên thường khó sử dụng các kỹ thuật kiểm thử hộp trắng vì không đủ chi phí thời gian.

Hiện tại trong các dự án mà tôi đang tham gia, ngôn ngữ lập trình chủ yếu được sử dụng là Java. Ngoài ra,trong các ngôn ngữ lập trình hiện đại ngày nay, Java là ngôn ngữ lập trình phổ biến trong suốt 13 năm qua [1].

Vì những lý do trên, tôi đề xuất chọn đề tài luận văn cao học: “Xây dựng công cụ sinh dữ liệu thử tự động cho chương trình Java”.

1. Mục đích và ý nghĩa đề tài

Mục đích

• Xây dựng công cụ sinh dữ liệu kiểm thử tự động cho chương trình nguồn Java. Nhằm mục đích thực hiện việc kiểm thử hộp trắng cho kiểm thử đơn vị một cách tự động và khoa học. Hướng đến mục tiêu giảm chi phí về thời gian và tài chính khi thực hiện công việc kiểm thử cho các lập trình viên/kiểm thử viên.
• Tìm hiểu về các thách thức gặp phải trong quá trình sinh dữ liệu thử tự động, từ đó đề xuất và cài đặt giải pháp để giải quyết các thách thức này.

Ý nghĩa khoa học

• Nghiên cứu về các kỹ thuật kiểm thử hộp trắng.
• Nghiên cứu về lý thuyết về tính thoả được.
• Xây dựng công cụ tự động sinh dữ liệu cho chương trình Java đảm bảo tiêu chí bao phủ lộ trình và tối ưu thời gian thực thi.

Ý nghĩa thực tiễn

• Giảm thời gian và chi phí cho việc kiểm thử hộp trắng của các lập trình viên khi thực hiện kiểm thử đơn vị.
• Dữ liệu thử tự động mang tính khách quan hơn, không bị phụ thuộc vào góc nhìn và kinh nghiệm của người lập trình.
• Kiểm tra được các lỗi tiềm ẩn trong mã nguồn.

1. Mục tiêu và nhiệm vụ

Mục tiêu

Xây dựng công cụ sinh dữ liệu tự động cho chương trình Java đảm bảo tiêu chí bao phủ lộ trình.. Các mục tiêu cụ thể như sau:

• Nghiên cứu về các phương pháp kiểm thử hộp trắng.
• Nghiên cứu về phương pháp giải các ràng buộc (SMT [2]).
• Nghiên cứu về các giải pháp sinh dữ liệu thử tự động cho chương trình Java và những thách thức hiện nay.
• Xây dựng công cụ sinh dữ liệu thử cho chương trình Java.

Nhiệm vụ

Để đạt được những mục tiêu trên, nhiệm vụ đặt ra của đề tài là:

• Nghiên cứu lý thuyết kiểm thử hộp trắng, tập trung vào các lý thuyết xây dựng tập dữ liệu kiểm thử.
• Nghiên cứu về lý thuyết về tính thoả được.
• Nghiên cứu và áp dụng kỹ thuật tối ưu hóa để tối ưu thời gian thực thi.

1. Đối tượng và phạm vi nghiên cứu

Luận văn tập trung vào nghiên cứu các đối tượng và phạm vi sau:

• Cấu trúc chương trình Java.
• Lý thuyết về tính thoả được của các bộ SMT và cách áp dụng để giải các ràng buộc.
• Phân tích, thiết kế và cài đặt ứng dụng sinh dữ liệu thử cho chương trình Java.

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

Phương pháp lý thuyết

• Tiến hành thu thập và nghiên cứu các tài liệu có liên quan đến đề tài.
• Nghiên cứu lý thuyết về thực thi ký hiệu và lý thuyết về tính thỏa được.
• Nghiên cứu về kiểm thử đơn vị và cách thực hiện.
• Nghiên cứu các phương pháp tối ưu hóa các đường thực thi.

Phương pháp thực nghiệm

• Nghiên cứu về phương pháp thực thi ký hiệu và các công cụ hỗ trợ thực thi ký hiệu hiện nay.
• Nghiên cứu đề xuất giải pháp tối ưu các đường thực thi trong quá trình thực hiện thực thi ký hiệu.

5. Kết luận

a. Kết quả của đề tài

• Thứ nhất, tìm hiểu về cách xây dựng và hoạt động của và phương pháp sinh dữ liệu kiểm thử tự động cho ngôn ngữ Java cũng như nghiên cứu về các thách thức hiện nay.
• Thứ hai, đề xuất và cài đặt giải pháp tối ưu trong việc sinh dữ liệu thử tự động nhằm tối ưu hóa thời gian nhưng vẫn đảm bảo tính đúng đắn, toàn vẹn và khả năng bao phủ của bộ dữ liệu thử tự động.

b. Hướng phát triển của đề tài

Trong quá trình nghiên cứu, bộ SMT Choco không cho kết quả tốt như các bộ SMT khác như Z3 hay CVC3. Vì vậy, trong thời gian tới chúng tôi sẽ tiếp tục nghiên cứu và triển khai tích hợp các bộ SMT mới và có khả năng hỗ trợ nâng cấp tốt hơn vào trong chương trình sinh dữ liệu kiểm thử

Chương 1: Cơ sở lý Thuyết

1.1. Tổng quan VỀ KIỂM THỮ PHẦN MỀM

1.1.1. Các bước kiểm thử

1.1.2. Các mức kiểm thử

1.1.3. Các kỹ thuật kiểm thử phần mềm

1.2. LÝ THUYẾT VỀ TÍNH THỎA ĐƯỢC

Tính thỏa mãn là một trong những vấn đề quan trọng nhất của ngành khoa học máy tính. Các vấn đề cần tính thỏa mãn được ứng dụng trong cả phát triển phần cứng cũng như phần mềm, đặc biệt là kiểm định phần cứng, kiểm thử, lập lịch, đồ thị.

Trong các lĩnh vực nói trên, nhiều các ứng dụng được xây dựng dựa trên việc tạo ra các công thức tiền tố và việc chứng minh tính hợp lệ của chúng. Cho dù hai thập niên gần đây, việc chứng minh tính hợp lệ của các định lý, biểu thức tiền tố có những tiến bộ đáng kể, tuy nhiên, không phải công thức nào cũng có thể chứng minh một cách tự động được. Lý do của vấn đề này là bởi lẽ nhiều công thức không quan tâm đến tính khả thi trong trường hợp tổng quát mà chỉ được quan tâm trong một lý thuyết nền tảng. Việc nghiên cứu tính khả thi của các công thức trong một lý thuyết nền tảng được gọi là các lý thuyết module về tính thỏa được (Satisfiability Modulo Theories hay SMT) và các công cụ để chứng minh một cách tự động các tính khả thi của những vẫn đề SMT được gọi là bộ giải SMT (SMT solver).

Trên thực tế, việc xây dựng và sử dụng các bộ giải SMT được phát triển khá sớm, từ đầu những năm 1980 [9]. Tại thời điểm đó, một số bộ giải được xây dựng bởi Greg Nelson và Derek Oppent tại trường đại học Stanford , Robert Shostak tại SRI, và Robert Boyer và J Moore tại trường đại học ở Texas. Đến cuối những năm 1990, việc nghiên cứu SMT hiện đại dựa trên lợi thế của công nghệ SAT đã xây dựng nhiều bộ giải SMT tiến bộ hơn .

Như đã đề cập ở trên, trong khuôn khổ đồ án, việc đánh giá về tính đúng đắn, các nghiên cứu về thuật giải của từng bộ giải sẽ không được đề cập đến. Vấn đề được đặt ra ở đây là kết quả của bộ giải nào sẽ được đưa ra sớm nhất. Hiện nay, có rất nhiều  các bộ giải như Absolver, Boolector, CVC3, OpenSMT, Yices, Z3…  Do yêu cầu của hệ thống là phải đưa ra được giá trị thỏa mãn (nếu bài toán  SMT đó có thỏa mãn) nên bộ giải hệ thống sử dụng phải hỗ trợ chức năng này. Ngoài  ra hệ thống sử dụng đầu vào theo chuẩn của SMT-Lib và ngắt thời gian giải một bài  toán (trong trường hợp bài toán cần thời gian giải quá lớn), do đó, bộ giải cần phải có  hỗ trợ những chức năng này khi hoạt động. Từ những yêu cầu đó, hai bộ giải là Yices của SRI International và Choco thuần Java đã được lựa chọn trong JPF. Hai bộ giải này tuy có cấu trúc khác nhau nhưng cùng được dựa trên thuật giải DPLL (Davis-Putnam-Logemann-Loveland ).

1.3. THỰC THI KÝ HIỆU

Trong hoạt động kiểm thử phần mềm, các ca kiểm thử thường được tạo ra một cách thủ công, gây tốn kém về chi phí cũng như thời gian để hoàn thành công đoạn này. Thực thi ký hiệu (Symbolic execution) được biết đến là một kỹ thuật nổi tiếng với khả năng tự động sinh những bộ ca kiểm thử có độ bao phủ cao với các tiêu chí kiểm thử nhằm phát hiện những lỗi sâu trong các hệ thống phần mềm phức tạp. Trong mục này sẽ trình bày các vấn đề tổng quan và một số kết quả của các nghiên cứu gần đây về kỹ thuật thực thi ký hiệu, đưa ra những thách thức cần giải quyết trong lĩnh vực này như: sự bùng nổ đường thực thi của chương trình, khả năng giải các ràng buộc, mô hình hóa bộ nhớ, các vấn đề về tương tranh, đồng thời cũng tập trung vào phân tích và đề xuất giải pháp để sinh ra dữ liệu kiểm thử cho chương trình Java một cách tự động.

Hiện nay có rất nhiều công cụ nền tảng phục vụ cho hoạt động kiểm thử phần mềm như JUnit cho ngôn ngữ Java, NUnit, VSUnit cho .NET để thực thi các ca kiểm thử mức đơn vị. Tuy nhiên, các công cụ kiểm thử này không hỗ trợ việc sinh tự động các ca kiểm thử đơn vị. Viết các ca kiểm thử là một công việc nặng nhọc và tốn nhiều công sức. Có nhiều phương pháp khác nhau hỗ trợ việc sinh tự động các ca kiểm thử giúp giảm chi phí và thời gian thực hiện đã được nghiên cứu và đưa ra như: Dựa trên kiểm chứng mô hình (Model Checking), kểm thử ngẫu nhiên (Random Testing). Nhưng hạn chế của nó là kiểm tra cùng một hành vi thực thi của chương trình nhiều lần với những đầu vào khác nhau và chỉ có thể kiểm tra được một số trường hợp thực thi của chương trình. Thêm vào đó, kiểm thử ngẫu nhiên khó xác định được khi nào việc kiểm thử nên được dừng lại và nó không biết tại điểm nào không gian trạng thái đã được thám hiểm hết. Để xác định khi nào việc kiểm thử dừng lại thì hệ thống kiểm thử ngẫu nhiên được kết hợp với các tiêu chuẩn an toàn. Để khắc phục những hạn chế của kiểm thử ngẫu nhiên, phương pháp thực thi tương trưng xây dựng các ràng buộc trên các giá trị ký hiệu và giải các ràng buộc đó để sinh ra các giá trị đầu vào cho chương trình mà có thể bao phủ tất các dòng lệnh cũng như các nhánh thực thi của chương trình

Ý tưởng của thực thi ký hiệu đã được đề xuất bởi, nhưng việc hiện thực ý tưởng mới chỉ được thực hiện trong những năm gần đây qua tiến bộ đáng kể trong lý thuyết giải các ràng buộc và các tiếp cận mở rộng thực thi ký hiệu động , một kỹ thuật kết hợp giữa các giá trị cụ thể và giá trị ký hiệu cho các giá trị đầu vào.

1.4. CÁC KỸ THUẬT THỰC THI KÝ HIỆU

a. Concolic testing

Thực thi ký hiệu động chính là sự kết hợp giữa thực thi cụ thể và thực thi ký hiệu. Trong thực thi ký hiệu động, chương trình được thực thi nhiều lần với những giá trị khác nhau của tham số đầu vào.

Bắt đầu bằng việc chọn những giá trị tùy ý cho các tham số đầu vào và thực thi chương trình với những giá trị cụ thể đó chương trình sẽ được thực thi theo một đường đi xác định. DART thực thi chương trình với các giá trị cụ thể của tham số đầu vào và thu gom các ràng buộc trong quá trình thực thi theo đường đi mà sự thực thi cụ thể này đi theo, đồng thời suy ra các ràng buộc mới từ những ràng buộc đã thu gom được.

Tại các câu lệnh rẽ nhánh, biểu thức điều kiện rẽ nhánh sẽ được đánh giá theo các giá trị cụ thể của các tham số đầu vào. Nếu biểu thức điều kiện rẽ nhánh nhận giá trị là True thì biểu thức của điều kiện rẽ nhánh sẽ được thu gom vào ràng buộc của ràng buộc lộ trình và được ghi nhớ, đồng thời phủ định của điều kiện rẽ nhánh sẽ được sinh ra và được thêm vào một ràng buộc lộ trình tương ứng với nhánh còn lại mà sự thực thi cụ thể đó không đi theo. Một bộ xử lý ràng buộc sẽ được sử dụng để giải quyết các ràng buộc mới sinh ra này để sinh ra các giá trị cụ thể của tham số đầu vào. Trong trường hợp ngược lại biểu thức phủ định của điều kiện rẽ nhánh sẽ được thu gom vào ràng buộc của ràng buộc lộ trình tương ứng với nhánh mà sự thực thi hiện thời đang đi theo và được ghi nhớ. Đồng thời điều kiện rẽ nhánh sẽ được sinh ra và thêm vào PC tương ứng với nhánh còn lại mà sự thực thi hiện thời không đi theo. Các giá trị mới được sinh ra của các tham số đầu vào sẽ tiếp tục được thực thi và quá trình này sẽ được lặp lại cho tới khi chương trình được thực thi theo tất cả các đường đi. Do các chương trình được thực thi với những giá trị cụ thể nên có thể thấy rằng tất cả các đường đi phân tích được trong quá trình thực thi ký hiệu động đều là các đường đi khả thi

b.Excution generated testing

EGT trộn lẫn giá trị cụ thể và thực thi ký hiệu bằng cách kiểm tra động trước mọi toán hạng. Nếu các giá trị liên quan đó hoàn toàn là các giá trị cụ thể thì toán hạng đó sẽ thực thi như chương trình gốc. Còn nếu có ít nhất một giá trị là ký hiệu thì toán hạng sẽ thực hiện thực thi ký hiệu và cập nhật điều kiện ràng buộc đường đi cho đường thực thi hiện thời.

1.5. CÁC THÁCH THỨC VÀ GIẢI PHÁP

a. Bùng nổ đường đi

Một trong những thách thức quan trọng của thực thi ký hiệu là nó sẽ sinh ra một số lượng lớn các đường thực thi mặc dù chương trình là nhỏ và thường là hàm mũ trong số các câu lệnh rẽ nhánh tĩnh của mã nguồn. Kết quả là trong một khoảng thời gian định trước nó sẽ quyết định khám phá con đường đầu tiên sao cho phù hợp nhất.

Trước hết, lưu ý rằng thực thi ký hiệu đã ngầm lọc ra tất cả các đường thực thi không phụ thuộc vào các biến ký hiệu đầu vào và những đường dẫn không khả thi (Infeasiblle path) trong quá trình giải các ràng buộc. Mặc dù như vậy, sự bùng nổ đường dẫn vẫn là một trong những thách thức lớn nhất đối với thực thi ký hiệu. Hiện nay có 2 cách tiếp cận chính để giải quyết vấn đề này là ưu tiên tìm kiếm kinh nghiệm (Heuristic search) và sử dụng kỹ thuật phân tích tính đúng đắn của chương trình.

b. Giải các ràng buộc

Mặc dù đã có những tiến bộ đáng kể trong kỹ thuật thực hiện giải các ràng buộc trong những năm gần đây, giúp cho thực thi ký hiệu trở nên thực tế hơn, nhưng việc giải các ràng buộc vẫn là cản trở đáng kể của thực thi ký hiệu. Nó thường chiếm nhiều thời gian trong quá trình thực hiện và là một trong những lý do chính khiến thực thi tương trưng không mở rộng được với một số loại chương trình mà mã nguồn của nó sinh ra với yêu cầu rất lớn trong việc giải các ràng buộc.

c. Mô hình hóa bộ nhớ

Độ chính xác của các câu lệnh của chương trình khi chuyển sang các ràng buộc ký hiệu có ảnh hưởng đáng kể đến độ bao phủ khi thực hiện thực thi ký hiệu. Ví dụ khi sử dụng mô hình hóa bộ nhớ mà xấp xỉ để thiết lập độ rộng cho tham biến kiểu Interger có thể có hiệu quả hơn trong thực tế nhưng mặt khác kết quả lại thiếu chính xác trong phân tích mã nguồn. Nó phụ thuộc vào khoảng lựa chọn giá trị tương ứng như lỗi tràn bộ nhớ toán học, cũng có thể gây ra thiếu đường dẫn trong thực thi ký hiệu, hoặc khai phá những đường đi không khả thi vv..

Chương 2: Giải pháp sinh dữ liệu thử cho chương trình java

2.1. giải pháp sinh dữ liệu thử cho chương trình java

a.Tổng quan về giải pháp

Mô hình tổng thể của giải pháp sinh dữ liệu thử cho chương trình Java được miêu tả như trong hình 2.1 dưới đây:

Hình 2.1. Mô hình triển khai

Tham số đầu vào của phương pháp là tệp nguồn Java cần phân tích, số vòng lặp tối đa (của các lệnh lặp for, while …), và các tiêu chuẩn phủ. Mã nguồn Java được phân rã thành các phương thức và mức độ ưu tiên xử lý của chúng được tính toán, những phương thức ít phụ thuộc vào các phương thức khác hơn sẽ có độ ưu tiên xử lý cao hơn, như vậy những phương thức không có lời gọi hàm sẽ được xử lý đầu tiên. Cuối cùng chúng ta có một danh sách các phương thức được xếp theo mức ưu tiên giảm dần, và chúng lần lượt được xử lý theo thứ tự đó.

Với mỗi phương thức, đầu tiên đồ thị luồng điều khiển được xây dựng, duyệt đồ thị luồng điều khiển sẽ cho ra các lộ trình thực thi của phương thức, tiếp đến có được tập ràng buộc tương ứng nhờ áp dụng phương pháp thực thi ký hiệu. Quá trình này được lặp lại cho đến khi tất cả các phương thức được phân tích hết.

Các lộ trình thực thi đã tìm được ở bước trên sẽ được đưa lần lượt vào SMT-Solver để kiểm tra tính thoả được và sinh ra dữ liệu kiểm thử tự động đảm bảo bao phủ được lộ trình đã đưa vào SMT-Solver

b.Phương pháp thực hiện

LIÊN HỆ:

SĐT+ZALO: 0935568275

F:\DỮ LIỆU COP CỦA CHỊ YẾN\DAI HOC DA NANG\KHOA HOC MAY TINH\PO NA\TomTatPona\TomTatPona