Luận văn thạc sĩ vnu uet 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 mô hình

Luận văn thạc sĩ nghiên cứu vnu uet 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 mô hình, đánh giá hiện trạng, phân tích vấn đề, đề xuất biện

• Tác giả: Phan Văn Tiến
• Người hướng dẫn: TS. Nguyễn Trường Thắng
• Trường học: Đại học Quốc gia Hà Nội
• Chuyên ngành: Công nghệ thông tin
• Đề tài: Nghiên Cứu Phương Pháp Sinh Dữ Liệu Kiểm Thử Phần Mềm Bằng Kỹ Thuật Kiểm Chứng Mô Hình
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2011
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CẢM ƠN
• LỜI CAM ĐOAN
• MỞ ĐẦU
• 1. CHƯƠNG 1: CƠ SỞ LÝ LUẬN
• 1.1. Tổng quan kiểm định phần mềm
• 1.2. Các nhóm kiểm định phần mềm
• 2. CHƯƠNG 2: JAVA PATH FINDER VÀ THỰC THI TƯỢNG TRƯNG
• 2.1. Giới thiệu về JPF
• 2.1.1. JPF có thể kiểm tra những chương trình gì?
• 2.1.2. Kiến trúc mức cao của JPF
• 2.1.3. Khả năng mở rộng của JPF
• 2.1.4. Một số mở rộng của JPF
• 2.2. Thực thi tượng trưng để sinh dữ liệu kiểm thử
• 2.2.1. Thực thi tượng trưng là gì?
• 2.2.2. Thực thi tượng trưng với JPF
• 3. CHƯƠNG 3: MICROSOFT Z3
• 3.1. Tại sao lại là Z3?
• 3.2. Kiến trúc của Z3
• 3.3. Định dạng đầu vào
• 3.4. Định dạng SMT-LIB
• 3.4.1. Các chức năng chính của SMT-LIB
• 3.4.2. Các quan hệ, phương thức, và hằng số
• 3.4.2.1. Tất cả các phương thức là tuyệt đối (total)
• 3.4.2.2. Uninterpreted function và hằng số
• 3.4.2.3. Phương thức đệ quy
• 3.5. Số học tuyến tính thực
• 3.6. Số học tuyến tính nguyên
• 3.7. Trộn giữa số nguyên và số thực
• 3.8. Số học phi tuyến tính
• 3.9. Kiểu dữ liệu
• 3.9.1. Kiểu bản ghi
• 3.9.2. Kiểu liệt kê (enumeration)
• 3.9.3. Kiểu dữ liệu đệ qui
• 3.10. Một vài ứng dụng của Z3
• 4. CHƯƠNG 4: TÍCH HỢP Z3 VỚI JPF
• 4.1. Nghiên cứu đánh giá các giải pháp
• 4.2. Kiến trúc hệ thống
• 4.3. Chuyển đổi dữ liệu
• 4.4. Thiết kế và cài đặt
• 4.5. Kết quả và đánh giá
• KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN CỦA ĐỀ TÀI
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng quan về Nghiên cứu phương pháp sinh dữ liệu kiểm thử phần mềm

Nghiên cứu phương pháp sinh dữ liệu kiểm thử phần mềm bằng kỹ thuật kiểm chứng mô hình đang trở thành một xu hướng quan trọng trong lĩnh vực công nghệ thông tin. Việc phát triển phần mềm ngày càng phức tạp, đòi hỏi các phương pháp kiểm thử hiệu quả hơn để đảm bảo chất lượng sản phẩm. Kỹ thuật kiểm chứng mô hình giúp tự động hóa quá trình kiểm thử, từ đó giảm thiểu thời gian và chi phí cho các tổ chức. Bài viết này sẽ đi sâu vào các khía cạnh của phương pháp này, từ lý thuyết đến ứng dụng thực tiễn.

1.1. Khái niệm về kiểm thử phần mềm và vai trò của nó

Kiểm thử phần mềm là quá trình đánh giá và xác minh rằng phần mềm đáp ứng các yêu cầu đã đề ra. Nó đóng vai trò quan trọng trong việc phát hiện lỗi và đảm bảo chất lượng sản phẩm. Việc áp dụng các phương pháp kiểm thử hiện đại như kiểm chứng mô hình giúp nâng cao hiệu quả kiểm thử.

1.2. Tại sao cần sinh dữ liệu kiểm thử tự động

Sinh dữ liệu kiểm thử tự động giúp tiết kiệm thời gian và công sức cho các kỹ sư kiểm thử. Thay vì phải tạo ra từng trường hợp kiểm thử một cách thủ công, các công cụ hiện đại có thể tự động sinh ra các trường hợp kiểm thử dựa trên các điều kiện và yêu cầu đã định nghĩa.

II. Vấn đề và thách thức trong kiểm thử phần mềm hiện nay

Mặc dù có nhiều tiến bộ trong lĩnh vực kiểm thử phần mềm, nhưng vẫn tồn tại nhiều thách thức. Các phần mềm ngày càng phức tạp, với nhiều module và tính năng, dẫn đến việc kiểm thử trở nên khó khăn hơn. Ngoài ra, việc đảm bảo độ phủ kiểm thử và phát hiện lỗi tiềm ẩn cũng là một vấn đề lớn.

2.1. Các vấn đề phổ biến trong kiểm thử phần mềm

Một số vấn đề phổ biến bao gồm việc thiếu dữ liệu kiểm thử, độ phức tạp trong việc tạo ra các trường hợp kiểm thử, và khả năng phát hiện lỗi không đầy đủ. Những vấn đề này có thể dẫn đến việc phần mềm không đạt yêu cầu chất lượng.

2.2. Thách thức trong việc áp dụng kỹ thuật kiểm chứng mô hình

Kỹ thuật kiểm chứng mô hình mặc dù mang lại nhiều lợi ích, nhưng cũng gặp phải thách thức trong việc tích hợp với các công cụ và ngôn ngữ lập trình khác nhau. Việc đảm bảo tính chính xác và hiệu quả của các mô hình kiểm chứng cũng là một vấn đề cần được giải quyết.

III. Phương pháp kiểm chứng mô hình trong sinh dữ liệu kiểm thử

Phương pháp kiểm chứng mô hình là một kỹ thuật mạnh mẽ giúp tự động hóa quá trình kiểm thử phần mềm. Bằng cách sử dụng các mô hình trừu tượng hóa, phương pháp này cho phép kiểm tra các thuộc tính của phần mềm mà không cần phải chạy mã nguồn thực tế.

3.1. Khái niệm về kiểm chứng mô hình

Kiểm chứng mô hình là quá trình xác minh rằng một mô hình phần mềm đáp ứng các yêu cầu và thuộc tính đã định nghĩa. Kỹ thuật này giúp phát hiện lỗi sớm trong quá trình phát triển phần mềm.

3.2. Các công cụ hỗ trợ kiểm chứng mô hình

Hiện nay có nhiều công cụ hỗ trợ kiểm chứng mô hình như Java PathFinder (JPF) và Microsoft Z3. Những công cụ này giúp tự động hóa quá trình kiểm thử và sinh dữ liệu kiểm thử một cách hiệu quả.

IV. Ứng dụng thực tiễn của phương pháp sinh dữ liệu kiểm thử

Phương pháp sinh dữ liệu kiểm thử bằng kỹ thuật kiểm chứng mô hình đã được áp dụng thành công trong nhiều dự án phần mềm. Việc sử dụng các công cụ như JPF và Z3 đã giúp các tổ chức tiết kiệm thời gian và chi phí trong quá trình kiểm thử.

4.1. Các trường hợp ứng dụng thành công

Nhiều tổ chức đã áp dụng phương pháp này để kiểm thử các hệ thống phức tạp như phần mềm ngân hàng và y tế. Kết quả cho thấy việc phát hiện lỗi sớm giúp giảm thiểu rủi ro và chi phí phát triển.

4.2. Lợi ích của việc áp dụng kiểm chứng mô hình

Việc áp dụng kiểm chứng mô hình không chỉ giúp nâng cao chất lượng phần mềm mà còn giảm thiểu thời gian kiểm thử. Các tổ chức có thể tập trung vào việc phát triển tính năng mới thay vì dành quá nhiều thời gian cho việc kiểm thử.

V. Kết luận và tương lai của nghiên cứu

Nghiên cứu về phương pháp sinh dữ liệu kiểm thử phần mềm bằng kỹ thuật kiểm chứng mô hình đang mở ra nhiều cơ hội mới cho ngành công nghệ thông tin. Với sự phát triển không ngừng của công nghệ, các phương pháp này sẽ ngày càng trở nên quan trọng hơn trong việc đảm bảo chất lượng phần mềm.

5.1. Tương lai của kiểm thử phần mềm

Trong tương lai, việc áp dụng các công nghệ mới như trí tuệ nhân tạo và học máy vào kiểm thử phần mềm sẽ giúp nâng cao hiệu quả và độ chính xác của quá trình kiểm thử.

5.2. Định hướng nghiên cứu tiếp theo

Các nghiên cứu tiếp theo nên tập trung vào việc cải thiện khả năng tích hợp giữa các công cụ kiểm chứng mô hình và các ngôn ngữ lập trình khác nhau, nhằm mở rộng khả năng ứng dụng của phương pháp này.

Nội dung chính

Tổng quan nghiên cứu

Trong bối cảnh phát triển phần mềm ngày càng phức tạp và quy mô lớn, việc đảm bảo chất lượng phần mềm trở thành một yêu cầu cấp thiết, đặc biệt trong các lĩnh vực nhạy cảm như y tế, ngân hàng và hàng không. Theo ước tính, các lỗi phần mềm có thể gây thiệt hại hàng tỷ đô la mỗi năm cho các doanh nghiệp và tổ chức. Kiểm thử phần mềm thủ công không thể đáp ứng đầy đủ yêu cầu về độ chính xác và hiệu quả, dẫn đến nhu cầu phát triển các phương pháp kiểm thử tự động dựa trên lý thuyết và công cụ hiện đại. Luận văn tập trung 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 mô hình, cụ thể là tích hợp công cụ Microsoft Z3 với Java PathFinder (JPF) nhằm nâng cao khả năng sinh dữ liệu kiểm thử cho các chương trình Java.

Mục tiêu nghiên cứu là phát triển giải pháp tích hợp Z3 – một công cụ SMT solver mạnh mẽ – với JPF để tự động sinh dữ liệu kiểm thử cho các bài toán mà JPF hiện tại chưa thể xử lý, đặc biệt là các bài toán số học phi tuyến. Phạm vi nghiên cứu tập trung vào các chương trình Java, với thời gian nghiên cứu từ năm 2010 đến 2011 tại Đại học Công nghệ, Đại học Quốc gia Hà Nội. Kết quả nghiên cứu có ý nghĩa quan trọng trong việc nâng cao hiệu quả kiểm thử phần mềm, giảm thiểu lỗi logic và tiết kiệm chi phí phát triển phần mềm.

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

Khung lý thuyết áp dụng

Luận văn dựa trên hai lý thuyết và mô hình nghiên cứu chính:

1. Lý thuyết tính thỏa mãn (SMT - Satisfiability Modulo Theories): Đây là nền tảng cho các công cụ SMT solver như Microsoft Z3, cho phép kiểm tra tính thỏa mãn của các biểu thức logic trong các lý thuyết nền tảng như số nguyên, số thực, mảng, và các kiểu dữ liệu phức tạp khác. SMT giúp xác định các điều kiện đường đi trong chương trình và sinh dữ liệu kiểm thử tương ứng.

2. Kiểm chứng mô hình (Model Checking) và thực thi tượng trưng (Symbolic Execution): JPF là một công cụ kiểm chứng mô hình cho Java, thực thi chương trình trên tất cả các đường đi có thể bằng cách sử dụng giá trị tượng trưng thay vì giá trị cụ thể. Thực thi tượng trưng giúp sinh ra các điều kiện đường đi (path conditions) và từ đó tạo ra các ca kiểm thử bao phủ toàn bộ chương trình.

Các khái niệm chính bao gồm:

• Path Condition (PC): Biểu thức logic mô tả điều kiện để một đường đi trong chương trình được thực thi.
• Kiểm thử dữ liệu động và tĩnh: Phân tích mã nguồn tĩnh và kiểm thử với dữ liệu đầu vào động.
• Độ phủ dòng chảy (Control Flow Coverage) và độ phủ dữ liệu (Data Coverage): Tiêu chí đánh giá chất lượng tập ca kiểm thử.

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

Nguồn dữ liệu chính là các chương trình Java mẫu được sử dụng để kiểm thử, cùng với các công cụ JPF và Z3. Phương pháp nghiên cứu bao gồm:

• Phân tích lý thuyết: Nghiên cứu sâu về SMT, Z3, JPF và kỹ thuật thực thi tượng trưng.
• Thiết kế kiến trúc tích hợp: Xây dựng wrapper để chuyển đổi ràng buộc từ JPF sang định dạng SMT-LIB của Z3.
• Phát triển và cài đặt: Cài đặt lớp ProblemZ3 để chuyển đổi ràng buộc, gọi Z3 qua dòng lệnh và xử lý kết quả trả về.
• Đánh giá thực nghiệm: Thử nghiệm với các ví dụ về số học tuyến tính và phi tuyến, so sánh kết quả với các công cụ tìm lời giải khác như Choco.

Quá trình nghiên cứu kéo dài trong khoảng thời gian từ đầu năm 2010 đến cuối năm 2011, với các bước thử nghiệm và hoàn thiện giải pháp tại Đại học Công nghệ, Đại học Quốc gia Hà Nội.

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

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

1. Khả năng sinh dữ liệu kiểm thử với số học tuyến tính:
   Khi áp dụng cho các bài toán số học tuyến tính, cả Z3 và Choco đều cho kết quả sinh dữ liệu kiểm thử chính xác và đầy đủ. Ví dụ, với chương trình tính toán có điều kiện ràng buộc tuyến tính, Z3 và Choco đều sinh ra các ca kiểm thử tương ứng với các nhánh điều kiện, đảm bảo độ phủ dòng chảy và dữ liệu.

2. Mở rộng khả năng xử lý số học phi tuyến:
   JPF hiện tại không hỗ trợ giải quyết các ràng buộc số học phi tuyến, dẫn đến việc không thể sinh dữ liệu kiểm thử cho các bài toán phức tạp như phép nhân giữa các biến. Qua tích hợp Z3, luận văn đã chứng minh khả năng xử lý các bài toán số học phi tuyến, sinh ra các ca kiểm thử phù hợp mà JPF trước đây không thể thực hiện.

3. Hiệu quả chuyển đổi và tích hợp:
   Việc sử dụng định dạng SMT-LIB làm chuẩn trao đổi giữa JPF và Z3 giúp quá trình tích hợp trở nên đơn giản và hiệu quả. Wrapper được thiết kế tuân thủ mô hình mở rộng của JPF, cho phép dễ dàng chuyển đổi ràng buộc và xử lý kết quả trả về. Thời gian xử lý và độ chính xác được cải thiện rõ rệt so với việc sử dụng các solver Java truyền thống như Choco hay IAsolver.

4. Giới hạn và thách thức:
   Mặc dù Z3 hỗ trợ nhiều lý thuyết và kiểu dữ liệu, việc tích hợp vẫn gặp một số khó khăn về hiệu suất khi xử lý các chương trình lớn hoặc phức tạp. Ngoài ra, việc chạy Z3 qua dòng lệnh giới hạn khả năng phân tán và mở rộng hệ thống.

Thảo luận kết quả

Kết quả nghiên cứu cho thấy việc tích hợp Z3 với JPF là một hướng đi khả thi và hiệu quả để nâng cao khả năng sinh dữ liệu kiểm thử cho các chương trình Java, đặc biệt là với các bài toán phức tạp về số học phi tuyến. So với các nghiên cứu trước đây chỉ sử dụng các solver Java như Choco, giải pháp này mở rộng phạm vi ứng dụng và cải thiện độ chính xác của ca kiểm thử.

Dữ liệu có thể được trình bày qua biểu đồ so sánh số lượng ca kiểm thử sinh ra và thời gian xử lý giữa các công cụ, hoặc bảng tổng hợp các loại ràng buộc được hỗ trợ. Điều này giúp minh họa rõ ràng ưu điểm của việc tích hợp Z3.

Ngoài ra, việc sử dụng SMT-LIB làm chuẩn trao đổi dữ liệu tạo điều kiện thuận lợi cho việc tích hợp với các công cụ SMT solver khác trong tương lai, mở rộng khả năng ứng dụng của JPF trong kiểm thử phần mềm.

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

1. Phát triển giao diện tích hợp trực tiếp giữa JPF và Z3:
   Thay vì gọi Z3 qua dòng lệnh, nên xây dựng giao diện API trực tiếp để giảm thiểu độ trễ và tăng hiệu quả xử lý. Mục tiêu đạt được trong vòng 12 tháng, do nhóm phát triển phần mềm thực hiện.

2. Mở rộng hỗ trợ cho các loại ràng buộc phức tạp hơn:
   Nghiên cứu và tích hợp thêm các lý thuyết phi tuyến, uninterpreted functions và các kiểu dữ liệu phức tạp khác trong Z3 để nâng cao khả năng sinh dữ liệu kiểm thử. Thời gian thực hiện dự kiến 18 tháng, phối hợp với các chuyên gia SMT.

3. Tối ưu hóa hiệu suất xử lý:
   Áp dụng các kỹ thuật tối ưu hóa bộ nhớ và thuật toán tìm kiếm trong JPF và Z3 để xử lý các chương trình lớn hơn, giảm thiểu hiện tượng bùng nổ trạng thái. Mục tiêu cải thiện hiệu suất ít nhất 30% trong 1 năm.

4. Phát triển công cụ hỗ trợ trực quan hóa kết quả kiểm thử:
   Xây dựng module hiển thị các điều kiện đường đi, ca kiểm thử và kết quả phân tích dưới dạng biểu đồ hoặc bảng, giúp người dùng dễ dàng đánh giá và phân tích. Thời gian hoàn thành dự kiến 6 tháng, do nhóm phát triển giao diện người dùng đảm nhận.

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

1. Nhà phát triển phần mềm và kiểm thử:
   Có thể áp dụng phương pháp tích hợp Z3 với JPF để tự động sinh dữ liệu kiểm thử, nâng cao chất lượng sản phẩm và giảm thiểu lỗi logic.

2. Nhà nghiên cứu trong lĩnh vực kiểm thử phần mềm và SMT:
   Luận văn cung cấp cơ sở lý thuyết và thực nghiệm về tích hợp SMT solver với công cụ kiểm chứng mô hình, làm nền tảng cho các nghiên cứu tiếp theo.

3. Các tổ chức phát triển phần mềm trong lĩnh vực nhạy cảm:
   Ngành y tế, ngân hàng, hàng không có thể ứng dụng giải pháp để đảm bảo phần mềm hoạt động chính xác, an toàn và tin cậy.

4. Giảng viên và sinh viên ngành Công nghệ Thông tin:
   Tài liệu tham khảo hữu ích cho việc giảng dạy và học tập về kiểm thử phần mềm, kiểm chứng mô hình và ứng dụng SMT solver.

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

1. Tại sao cần tích hợp Z3 với JPF mà không dùng riêng JPF?
   JPF hiện tại chỉ hỗ trợ các solver Java với hạn chế về số học phi tuyến và các ràng buộc phức tạp. Z3 là công cụ SMT solver mạnh, hỗ trợ đa dạng lý thuyết, giúp mở rộng khả năng sinh dữ liệu kiểm thử cho JPF.

2. Định dạng SMT-LIB có vai trò gì trong tích hợp này?
   SMT-LIB là chuẩn định dạng biểu diễn các biểu thức logic, giúp chuyển đổi ràng buộc từ JPF sang Z3 một cách chuẩn hóa, dễ dàng và hiệu quả, đồng thời hỗ trợ nhiều công cụ SMT khác.

3. Giải pháp này có thể áp dụng cho ngôn ngữ lập trình khác ngoài Java không?
   Hiện tại tập trung cho Java do JPF là công cụ kiểm chứng mô hình cho Java. Tuy nhiên, ý tưởng tích hợp SMT solver có thể mở rộng cho các ngôn ngữ khác với công cụ tương ứng.

4. Làm thế nào để xử lý hiện tượng bùng nổ trạng thái khi thực thi tượng trưng?
   Có thể áp dụng các kỹ thuật trừu tượng hóa, giới hạn phạm vi kiểm thử, hoặc tối ưu thuật toán tìm kiếm trong JPF để giảm thiểu số lượng trạng thái cần duyệt.

5. Có thể sử dụng Z3 để kiểm thử các chương trình có tham số thực không?
   Z3 hỗ trợ số thực và số nguyên, tuy nhiên việc kiểm thử tham số thực có thể gặp một số hạn chế do đặc tính của thực thi tượng trưng và cách dịch mã bytecode Java. Giải pháp tích hợp đã thử nghiệm với các trường hợp tham số thực và cho kết quả khả quan.

Kết luận

• Luận văn đã nghiên cứu và phát triển thành công phương pháp tích hợp Microsoft Z3 với Java PathFinder để sinh dữ liệu kiểm thử tự động cho chương trình Java.
• Giải pháp mở rộng khả năng xử lý các bài toán số học phi tuyến mà JPF truyền thống chưa hỗ trợ.
• Sử dụng định dạng SMT-LIB làm chuẩn trao đổi dữ liệu giữa JPF và Z3 giúp quá trình tích hợp hiệu quả và dễ dàng mở rộng.
• Kết quả thực nghiệm cho thấy Z3 và JPF tích hợp có thể sinh ra các ca kiểm thử đầy đủ, chính xác và tiết kiệm thời gian so với các công cụ tìm lời giải khác.
• Đề xuất các hướng phát triển tiếp theo nhằm nâng cao hiệu suất, mở rộng hỗ trợ lý thuyết và cải thiện giao diện người dùng.

Các nhà nghiên cứu và phát triển phần mềm nên áp dụng và tiếp tục hoàn thiện giải pháp tích hợp này để nâng cao chất lượng kiểm thử phần mềm, đồng thời mở rộng nghiên cứu sang các lĩnh vực và ngôn ngữ lập trình khác.

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

Mở đầu: Giới thiệu về đề tài, tính cấp thiết cũng nhƣ mục tiêu của đề tài Chƣơng 1: Cơ sở lý luận Chƣơng 2: JPF và Thực thi tƣợng trƣng 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. Chƣơng 3: Microsoft Z3 Nội dung: Giới thiệu về lý thuyết tính thỏa đƣợc SMT, Z3, các lý thuyết đƣợc hỗ trợ trên Z3, các API của Z3 để tích hợp với JPF, các ứng dụng của Z3.

Chƣơng 4: Tích hợp JPF với Z3 Nội dung: Nghiên cứu, đánh giá các giải pháp. Sau khi đã có giải pháp 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ả. 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, triển khai và hƣớng phát triển tiếp theo. LUAN VAN CHAT LUONG download : add [e-mail] 10 CHƢƠNG 1- CƠ SỞ LÝ LUẬN 1.1 Tổng quan kiểm định phần mềm Nhƣ chúng ta đã biết, việc kiểm thử phần mềm là một khâu không thể thiếu trong các bƣớc phát triển phần mềm, đặc biệt các phần mềm lớn, nhiều module do nhiều ngƣời phát triển, dễ sinh ra các lỗi tiềm ẩn mà nhà phát triển không thể lƣờng trƣớc.

Trong lĩnh vực kiểm định chất lƣợng phần mềm hiện nay trên thế giới, hiện có nhiều kỹ thuật nhƣng tựu chung có thể phân theo ba nhóm chính: Phân tích mã nguồn tĩnh (static code analysis), kiểm thử dữ liệu động (dynamic data testing) và kỹ thuật hình thức dựa trên mô hình (model-based verification). Hai nhóm đầu tập trung vào việc nâng cao chất lƣợng phần mềm tại mức mã nguồn, trong khi nhóm cuối cùng xử lý phần mềm tại mức trừu tƣợng cao hơn – mô hình.2 Các nhóm kiểm định phần mềm Phân tích mã nguồn tĩnh là kỹ thuật phát hiện lỗi chƣơng trình mà không yêu cầu chạy chƣơng trình đó. Không giống nhƣ kỹ thuật kiểm thử dữ liệu động đòi hỏi phải chạy chƣơng trình với dữ liệu đầu vào thật, kỹ thuật phân tích mã nguồn tĩnh chỉ xem xét mã nguồn của chƣơng trình. Kỹ thuật kiểm thử phần mềm dựa trên mô hình: khác với hai nhóm ở trên ở điểm đối tƣợng đƣợc kiểm thử là các mô hình đƣợc trừu tƣợng hóa từ hệ thống đƣợc xem xét.

Quá trình trừu tƣợng hóa là việc lƣợc bỏ những chi tiết của hệ thống trong khi chỉ giữ lại những thông tin/khía cạnh quan trọng cần đƣợc lƣu tâm. Kỹ thuật trừu tƣợng hóa đơn giản hóa hệ thống đƣợc xem xét và do đó giảm không gian tìm kiếm và thời gian phân tích chƣơng trình đi nhiều lần so với lúc thực hiện công việc phân tích đó trên mã nguồn. Khi xây dựng xong phần mềm, chúng ta phải sử dụng các testcase (trƣờng hợp kiểm thử) cho việc kiểm thử. Chất lƣợng của việc kiểm thử phụ thuộc rất lớn vào tập hợp các testcase mà chúng ta sử dụng.

Hai tiêu chí chính của việc đánh giá chất lƣợng kiểm thử đó là hiệu quả cho chất lƣợng phần mềm đƣợc kiểm thử là độ phủ dòng chảy (control flow coverage) và độ phủ dữ liệu (data coverage). Tiêu chí thứ nhất tập trung vào việc kiểm thử tất cả các điểm điều khiển trên chƣơng trình (ví dụ: các nhánh rẽ khả đạt trong cấu trúc chƣơng trình – reachable control points). Trong khi tiêu chí thứ hai tập trung vào tập dữ liệu kiểm thử ứng với mỗi điểm điều khiển trong cấu trúc chƣơng trình. Bằng kỹ thuật phân tích chƣơng trình dựa trên mô hình sau khi trừu tƣợng hóa mã nguồn của chƣơng trình đƣợc kiểm thử, việc phân tích cấu trúc logic của chƣơng trình và tập dữ liệu ứng với mỗi điểm điều khiển trong chƣơng trình sẽ dễ dàng hơn.

Qua đó, quá LUAN VAN CHAT LUONG download : add [e-mail] 11 trình sinh ra tập các testcase sẽ nhanh chóng và chính xác, đảm bảo các tiêu chí control flow và data coverage tốt hơn nhiều so với cách tiếp cận ở mức mã nguồn truyền thống. Hơn nữa, nếu quá trình này đƣợc thực hiện một cách tự động sẽ giảm thiểu nhiều công sức cho các chuyên gia kiểm thử chƣơng trình. Với cách tiếp cận nhƣ vậy, phần mềm có thể đƣợc kiểm thử một cách tự động bằng máy, đem lại kết quả chuẩn hơn, xét đƣợc nhiều trƣờng hợp hơn, đặt biệt là các lỗi logic, tiết kiệm chi phí sản xuất. Đánh giá tập dữ liệu kiểm thử: Ngoại trừ những chƣơng trình đơn giản, sẽ là không thực tế nếu kiểm chứng phần mềm trên tập tất cả dữ liệu đầu vào có thể.

Ngay cả khi chỉ tính tổ hợp của các dữ liệu đầu vào hoặc tổ hợp của các hàm, số lƣợng đầu vào và số lƣợng các trạng thái cũng là quá lớn. Khi hệ thống có bộ nhớ lớn, các dữ liệu đầu vào, đầu ra sẽ đƣợc log lại để theo dõi trạng thái. Trong khi không có một công cụ để tạo ra một thiết kế phần mềm chuẩn, hoàn chỉnh và chắc chắn thì việc kiểm thử là một khâu không thể thiếu để có thể đánh giá đƣợc chất lƣợng phần mềm. Vì thế ngƣời ta phải tìm cách chọn đƣợc một tập dữ liệu nhỏ mà có thể kiểm thử mang lại đƣợc độ tin cậy cao với mỗi hệ thống.

Độ phủ hay mức độ đầy đủ bằng trực quan đánh giá đƣợc phạm vi hay mức độ kiểm thử. Nếu kiểm thử không đầy đủ đƣợc hết mọi khía cạnh của phần mềm đồng nghĩa với việc chúng ta bỏ sót nhiều lỗi. Các tấn suất của các trƣờng hợp cũng không giống nhau. Khái niệm ca kiểm thử đơn giản là kiểm chứng các trạng thái đƣa ra thể hiện cho hoạt động của hệ thống.

Chúng ta có thể tạo ra ca kiểm thử đề đạt đƣợc trạng thái có thể bằng cách đƣa vào các biến đặc biệt, trạng thái để điều khiển hệ thống. LUAN VAN CHAT LUONG download : add [e-mail] 12 CHƢƠNG 2- JAVA PATH FINDER VÀ THỰC THI TƯỢNG TRƯNG Trong chƣơng này sẽ bao gồm hai 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 [5].

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 2-1 mô tả mô hình hoạt động của JPF.1: Mô hình hoạt động của JPF 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 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. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.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.java 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.2: Sơ đồ trạng thái trong quá trình kiểm thử LUAN VAN CHAT LUONG download : add [e-mail] 14 Hoạt động của lớp trên đó là khởi tạo 2 biến a và b một cách ngẫu nhiên trong các khoang tƣơng ứng la [0,2] và [0,3]. 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 vẽ bên dƣới: 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 đỏ 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 2.3: Kiến trúc mức cao LUAN VAN CHAT LUONG download : add [e-mail] 15 Hình 2-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. 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 Hình 2.4: Mẫu Listener LUAN VAN CHAT LUONG download : add [e-mail] 16 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ơ 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.