Các Kỹ Thuật Kiểm Thử Dòng Dữ Liệu Tĩnh Trong Phát Triển Phần Mềm

Khám phá các kỹ thuật kiểm thử dòng dữ liệu tĩnh, giúp nâng cao chất lượng phần mềm và phát hiện lỗi hiệu quả trong quá trình phát triển.

• Tác giả: Nguyễn Thị Yên
• Người hướng dẫn: TS. Đặng Văn Hư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: Các Kỹ Thuật Trong Kiểm Thử Dòng Dữ Liệu Tĩnh
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2016
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CAM ĐOAN
• DANH MỤC CÁC KÝ HIỆU VIẾT TẮT
• DANH MỤC CÁC HÌNH
• DANH MỤC CÁC BẢNG
• MỞ ĐẦU
• 1. CHƯƠNG 1: TỔNG QUAN VỀ KIỂM THỬ PHẦN MỀM VÀ KIỂM THỬ TĨNH
• 1.1. Khái quát về Kiểm thử phần mềm
• 1.1.1. Định nghĩa về Kiểm thử phần mềm
• 1.1.2. Qui trình phát triển phần mềm RUP
• 1.1.3. Các mức kiểm thử phần mềm
• 1.1.4. Ca kiểm thử và các phương pháp thiết kế ca kiểm thử
• 1.1.5. Các ý tưởng không đúng về kiểm thử
• 1.1.6. Các hạn chế của việc kiểm thử
• 1.2. Khái quát về Kiểm thử tĩnh
• 1.2.1. Định nghĩa về Kiểm thử tĩnh
• 1.2.2. Phân loại các kỹ thuật kiểm thử tĩnh
• 1.2.3. Sơ lược về các kỹ thuật kiểm thử tĩnh
• 2. CHƯƠNG 2: PHƯƠNG PHÁP KIỂM THỬ DÒNG DỮ LIỆU TĨNH TRONG KIỂM THỬ PHẦN MỀM
• 2.1. Phương pháp kiểm thử dòng dữ liệu tĩnh
• 2.1.1. Ý tưởng của phương pháp
• 2.1.2. Các vấn đề bất thường trong dòng dữ liệu
• 2.1.3. Phương pháp kiểm thử dòng dữ liệu tĩnh
• 3. CHƯƠNG 3: ỨNG DỤNG LOGIC HOARE TRONG KIỂM THỬ PHẦN MỀM
• 3.1. Tổng quan về Logic Hoare
• 3.1.1. Ứng dụng Logic Hoare trong kiểm thử phần mềm
• 3.1.2. Sơ lược kỹ thuật kiểm thử dựa trên kịch bản dòng dữ liệu
• 3.1.3. Ký hiệu được sử dụng trong Logic Hoare
• 3.2. Kỹ thuật kết hợp Logic Hoare với kỹ thuật kiểm thử dựa trên kịch bản dòng dữ liệu - Phương pháp TBFV
• 3.3. Áp dụng phương pháp TBFV
• 3.3.1. Áp dụng cho đoạn chương trình
• 3.3.2. Áp dụng cho việc gọi phương thức
• 3.4. Các nghiên cứu liên quan
• KẾT LUẬN VÀ KIẾN NGHỊ
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan Về Kỹ Thuật Kiểm Thử Dòng Dữ Liệu Tĩnh

Trong bối cảnh ngành công nghiệp phần mềm phát triển mạnh mẽ, việc đảm bảo chất lượng phần mềm trở nên vô cùng quan trọng. Kiểm thử phần mềm là một hoạt động không thể thiếu, tiêu tốn đến 50% thời gian và chi phí của dự án. Trong đó, kiểm thử dòng dữ liệu tĩnh đóng vai trò quan trọng. Luận văn này tập trung nghiên cứu về các kỹ thuật kiểm thử dòng dữ liệu tĩnh, từ đó đưa ra những giải pháp giúp nâng cao hiệu quả kiểm thử, giảm thiểu rủi ro và chi phí phát triển phần mềm. Mục tiêu là nghiên cứu tổng quan về kiểm thử phần mềm, các phương pháp kiểm thử, và ứng dụng Logic Hoare. Cấu trúc luận văn chia thành 3 chương chính, đi từ tổng quan đến ứng dụng cụ thể.

1.1. Định Nghĩa và Mục Tiêu của Kiểm Thử Dòng Dữ Liệu

Kiểm thử phần mềm là quy trình đảm bảo chất lượng, chứng minh phần mềm không có lỗi và phát hiện lỗi càng sớm càng tốt. Lỗi được hiểu là phần mềm không hoạt động đúng như đặc tả. Kiểm thử phần mềm hướng tới việc phát hiện càng nhiều lỗi càng tốt trong thời gian xác định, chứng minh sản phẩm phù hợp đặc tả, xác thực chất lượng kiểm thử với chi phí tối thiểu, và tạo các ca kiểm thử chất lượng cao. "Có hai mục đích chính của một phép thử: tìm thất bại hoặc chứng tỏ việc tiến hành của phần mềm là đúng đắn" (Nguyễn Thị Yên, 2016). Đây là nền tảng cho mọi hoạt động kiểm thử.

1.2. Vai Trò Quan Trọng Của Kiểm Thử Tĩnh Trong SDLC

Kiểm thử tĩnh đóng vai trò quan trọng trong việc đánh giá chất lượng phần mềm trong quá trình phát triển. Thông qua chu trình “kiểm thử - tìm lỗi - sửa lỗi”, chất lượng của sản phẩm phần mềm được cải thiện. Nhiều tác giả mô tả kiểm thử phần mềm là một quy trình kiểm chứng để đánh giá và tăng cường chất lượng của sản phẩm phần mềm. Quy trình này gồm hai công việc chính là phân tích tĩnh và phân tích động. Phân tích tĩnh và động là hai kỹ thuật bổ sung cho nhau.

II. Vấn Đề và Thách Thức Trong Kiểm Thử Dòng Dữ Liệu Tĩnh

Mặc dù kiểm thử dòng dữ liệu tĩnh mang lại nhiều lợi ích, nhưng cũng tồn tại không ít thách thức. Việc xác định và xử lý các vấn đề bất thường trong dòng dữ liệu (ví dụ: biến được định nghĩa nhưng không được sử dụng) đòi hỏi sự hiểu biết sâu sắc về mã nguồn và logic của chương trình. Bên cạnh đó, các công cụ hỗ trợ kiểm thử dòng dữ liệu tĩnh thường có giới hạn về khả năng phân tích và báo cáo, gây khó khăn cho việc đánh giá và sửa lỗi. Ngoài ra, việc tích hợp kiểm thử dòng dữ liệu tĩnh vào quy trình phát triển phần mềm hiện tại cũng là một thách thức không nhỏ.

2.1. Các Loại Lỗi Thường Gặp Trong Dòng Dữ Liệu Phần Mềm

Có nhiều loại lỗi có thể xảy ra trong dòng dữ liệu. Ví dụ: tính toán sai, hiệu chỉnh sai dữ liệu, trộn dữ liệu không đúng, tìm kiếm dữ liệu sai yêu cầu, xử lý sai mối quan hệ giữa các dữ liệu, coding/hiện thực sai các qui luật nghiệp vụ. Những lỗi này có thể dẫn đến kết quả không chính xác, hiệu suất kém, hoặc thậm chí là gây ra sự cố hệ thống. Việc phát hiện sớm và sửa chữa các lỗi này là rất quan trọng để đảm bảo chất lượng phần mềm.

2.2. Hạn Chế Của Các Công Cụ Phân Tích Dòng Dữ Liệu Tĩnh

Các công cụ phân tích dòng dữ liệu tĩnh có thể giúp tự động hóa quá trình kiểm thử, nhưng chúng không phải là hoàn hảo. Chúng có thể gặp khó khăn trong việc phân tích các đoạn mã phức tạp, hoặc bỏ sót các lỗi tinh vi. Ngoài ra, các công cụ này thường đưa ra nhiều cảnh báo sai (false positives), gây mất thời gian cho việc đánh giá và loại bỏ chúng.

III. Phương Pháp Kiểm Thử Dòng Dữ Liệu Tĩnh Hiệu Quả Nhất

Để khắc phục những hạn chế trên, cần áp dụng phương pháp kiểm thử dòng dữ liệu tĩnh một cách hiệu quả. Điều này bao gồm việc lựa chọn công cụ phù hợp, tùy chỉnh cấu hình phân tích, và kết hợp kiểm thử tự động với kiểm thử thủ công. Bên cạnh đó, cần chú trọng đến việc xây dựng các quy tắc kiểm thử rõ ràng và tuân thủ chúng một cách nghiêm ngặt. Các kỹ thuật kiểm thử tĩnh có thể được chia thành hai nhóm kỹ thuật: nhóm kỹ thuật kiểm thử kiểm tra (verification tests); nhóm kỹ thuật kiểm thử phân tích (analysis tests).

3.1. Lựa Chọn Công Cụ Phân Tích Phù Hợp Cho Dự Án

Việc lựa chọn công cụ phân tích dòng dữ liệu tĩnh phù hợp là rất quan trọng. Các yếu tố cần xem xét bao gồm: khả năng phân tích của công cụ, khả năng tích hợp với IDE và các công cụ khác, khả năng tùy chỉnh cấu hình, và chi phí. Cần đánh giá kỹ lưỡng các công cụ khác nhau trước khi đưa ra quyết định cuối cùng.

3.2. Kết Hợp Kiểm Thử Tự Động Và Thủ Công Để Tối Ưu

Kiểm thử tự động và kiểm thử thủ công nên được kết hợp để đạt hiệu quả tối ưu. Kiểm thử tự động có thể giúp phát hiện các lỗi cơ bản một cách nhanh chóng, trong khi kiểm thử thủ công có thể giúp phát hiện các lỗi tinh vi hơn. Việc kết hợp cả hai phương pháp sẽ giúp đảm bảo chất lượng phần mềm một cách toàn diện.

IV. Ứng Dụng Logic Hoare Trong Kiểm Thử Dòng Dữ Liệu Tĩnh

Logic Hoare là một công cụ mạnh mẽ có thể được sử dụng để chứng minh tính đúng đắn của chương trình. Bằng cách kết hợp Logic Hoare với kiểm thử dòng dữ liệu tĩnh, có thể nâng cao hiệu quả kiểm thử và giảm thiểu rủi ro. Logic Hoare cung cấp một phương pháp hình thức để mô tả và chứng minh các tính chất của chương trình, giúp phát hiện các lỗi tiềm ẩn mà các phương pháp kiểm thử thông thường có thể bỏ sót. Chương 3 của luận văn trình bày chi tiết về ứng dụng Logic Hoare trong kiểm thử phần mềm.

4.1. Tổng Quan Về Logic Hoare Và Các Ký Hiệu Sử Dụng

Logic Hoare là một hệ thống logic được sử dụng để chứng minh tính đúng đắn của chương trình. Hệ thống này dựa trên việc sử dụng các bộ ba Hoare, có dạng {P} C {Q}, trong đó P là tiền điều kiện, C là đoạn mã, và Q là hậu điều kiện. Bộ ba Hoare có nghĩa là nếu P đúng trước khi thực thi C, thì Q sẽ đúng sau khi thực thi C.

4.2. Kỹ Thuật Kết Hợp Logic Hoare Với Kiểm Thử Dòng Dữ Liệu

Việc kết hợp Logic Hoare với kiểm thử dòng dữ liệu có thể giúp phát hiện các lỗi tiềm ẩn mà các phương pháp kiểm thử thông thường có thể bỏ sót. Kỹ thuật này dựa trên việc sử dụng Logic Hoare để mô tả các tính chất của dòng dữ liệu, và sau đó sử dụng kiểm thử dòng dữ liệu để kiểm tra xem các tính chất này có được thỏa mãn hay không.

V. Kết Luận và Hướng Phát Triển Kỹ Thuật Kiểm Thử Tĩnh

Kiểm thử dòng dữ liệu tĩnh là một kỹ thuật quan trọng trong quá trình phát triển phần mềm, giúp phát hiện các lỗi tiềm ẩn và nâng cao chất lượng sản phẩm. Luận văn này đã trình bày tổng quan về kiểm thử dòng dữ liệu tĩnh, các vấn đề và thách thức liên quan, các phương pháp kiểm thử hiệu quả, và ứng dụng Logic Hoare. Trong tương lai, kỹ thuật kiểm thử dòng dữ liệu tĩnh sẽ tiếp tục phát triển và đóng vai trò ngày càng quan trọng trong việc đảm bảo chất lượng phần mềm.

5.1. Tóm Tắt Các Kết Quả Nghiên Cứu Chính Về Kiểm Thử Tĩnh

Luận văn đã trình bày các khái niệm cơ bản về kiểm thử tĩnh, phân loại các kỹ thuật kiểm thử tĩnh thành verification và phân tích tĩnh. Đồng thời, luận văn cũng đề cập đến các kỹ thuật phân tích style, phân tích dòng điều khiển và phân tích dòng dữ liệu.

5.2. Hướng Nghiên Cứu Phát Triển Trong Tương Lai Của Kiểm Thử

Trong tương lai, có nhiều hướng nghiên cứu phát triển cho kiểm thử dòng dữ liệu tĩnh. Một trong số đó là phát triển các công cụ phân tích mạnh mẽ hơn, có khả năng phân tích các đoạn mã phức tạp và phát hiện các lỗi tinh vi hơn. Một hướng khác là phát triển các phương pháp kiểm thử dựa trên trí tuệ nhân tạo, có khả năng tự động hóa quá trình kiểm thử và cải thiện hiệu quả phát hiện lỗi.

Nội dung chính

Tổng quan nghiên cứu

Trong kỹ nghệ phần mềm hiện đại, hoạt động bảo đảm chất lượng đóng vai trò sống còn đối với sự thành bại của mọi hệ thống thông tin. Các thống kê từ thực tế sản xuất phần mềm cho thấy hoạt động kiểm thử thường tiêu tốn khoảng 50% tổng thời gian và chiếm hơn 50% ngân sách của toàn bộ dự án phát triển. Mặc dù chiếm tỷ trọng tài nguyên rất lớn, các phương pháp kiểm thử truyền thống chủ yếu dựa trên kiểm thử động vẫn bộc lộ hạn chế cố hữu: chỉ có thể phát hiện sự hiện diện của lỗi tại các ca kiểm thử cụ thể mà không thể chứng minh sự vắng mặt hoàn toàn của các khiếm khuyết trong mã nguồn. Đặc biệt, các lỗi liên quan đến việc khởi tạo, gán giá trị và sử dụng biến dữ liệu chiếm khoảng 30% đến 40% tổng số lỗi logic tiềm ẩn, gây ra những rủi ro nghiêm trọng về an toàn và hiệu năng hệ thống.

Nhằm giải quyết thách thức này, nghiên cứu tập trung giải quyết bài toán phát hiện sớm các bất thường trong mã nguồn thông qua đề tài nghiên cứu các kỹ thuật trong kiểm thử dòng dữ liệu tĩnh do tác giả Nguyễn Thị Yên thực hiện dưới sự hướng dẫn khoa học của Tiến sĩ Đặng Văn Hưng tại Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội vào năm 2016. Mục tiêu cụ thể của luận văn là hệ thống hóa toàn diện các kỹ thuật phân tích và kiểm thử dòng dữ liệu tĩnh, đồng thời đề xuất giải pháp đột phá kết hợp giữa Logic Hoare và kiểm thử dựa trên kịch bản dòng dữ liệu nhằm nâng cao năng lực kiểm chứng phần mềm.

Phạm vi nghiên cứu tập trung vào việc phân tích mã nguồn ở cấp độ kiểm thử đơn vị, khai thác mô hình toán học hình thức và thử nghiệm trên hệ thống phần mềm điều khiển thẻ thông minh trong giao thông công cộng. Ý nghĩa học thuật và thực tiễn của công trình thể hiện ở khả năng phát hiện lỗi ở giai đoạn sớm nhất, giúp giảm thiểu khoảng 60% đến 70% chi phí khắc phục lỗi so với việc phát hiện muộn ở giai đoạn kiểm thử hệ thống hoặc vận hành.

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 sự kết hợp chặt chẽ giữa lý thuyết kiểm thử dòng dữ liệu cổ điển, kỹ thuật lát cắt chương trình và lý thuyết logic hình thức. Khung lý thuyết trọng tâm bao gồm:

Lý thuyết kiểm thử dòng dữ liệu của Sandra Rapps và Elaine Weyuker được công bố từ những năm 1980, thiết lập 9 tiêu chuẩn đo độ bao phủ dòng dữ liệu dựa trên đồ thị chương trình, bao gồm các tiêu chuẩn cốt lõi như All-Paths, All-DU-Paths, All-Uses, All-Defs, All-P-Uses và All-C-Uses. Mô hình này phân định rõ hai trạng thái cơ bản của biến gồm điểm định nghĩa DEF (khi biến được gán giá trị) và điểm sử dụng USE (khi biến được tham chiếu). Điểm sử dụng được chia chi tiết thành sử dụng trong biểu thức điều kiện (P-use) và sử dụng trong tính toán (C-use).

Lý thuyết lát cắt chương trình (Program Slicing) do Mark Weiser khởi xướng năm 1984 và được Keith Gallagher cùng James Lyle phát triển mở rộng vào năm 1991. Kỹ thuật này cho phép trích xuất một tập con mã nguồn ảnh hưởng trực tiếp hoặc gián tiếp đến giá trị của một biến cụ thể tại một câu lệnh xác định, thiết lập nên cấu trúc lưới lát cắt giúp cô lập hoàn toàn phạm vi lỗi.

Hệ thống Logic Hoare do C.A.R. Hoare đề xuất năm 1969, cung cấp nền tảng suy diễn hình thức về tính đúng đắn của chương trình thông qua cấu trúc bộ ba Hoare gồm tiền điều kiện, câu lệnh thực thi và hậu điều kiện, kết hợp giải thuật tính toán tiền điều kiện yếu nhất (weakest precondition).

Nghiên cứu tập trung làm rõ 3 khái niệm bất thường dòng dữ liệu nền tảng theo phân loại của Fosdick và Osterweil: gán giá trị liên tiếp không qua sử dụng (loại 1 - dd), sử dụng biến khi chưa khởi tạo giá trị (loại 2 - ur), và khai báo hoặc gán giá trị nhưng không bao giờ sử dụng (loại 3 - du). Đồng thời, mô hình chuyển trạng thái U-D-R-A của Huang được sử dụng để phát hiện trạng thái lỗi bất thường tự động.

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

Nghiên cứu sử dụng nguồn dữ liệu bao gồm các đoạn mã giả định chuẩn hóa, cấu trúc điều khiển phức hợp và mô hình đặc tả hình thức bằng ngôn ngữ SOFL. Nguồn dữ liệu thực nghiệm tiêu biểu được trích xuất từ phân hệ xử lý nghiệp vụ tính giá vé giảm trừ ChildFareDiscount thuộc hệ thống quản lý thẻ giao thông đường sắt JR tại Tokyo.

Cỡ mẫu nghiên cứu bao gồm 10 kịch bản dòng dữ liệu chức năng (FSF) đại diện cho toàn bộ các nhánh rẽ điều kiện, phép gán số học và vòng lặp phức tạp. Phương pháp chọn mẫu là chọn mẫu có chủ đích (purposive sampling), tập trung vào các đoạn mã chứa cấu trúc lặp While và rẽ nhánh If-Then-Else có độ phức tạp dòng điều khiển cao.

Phương pháp phân tích chủ đạo là phương pháp chứng minh hình thức dựa trên kiểm thử TBFV (Testing-Based Formal Verification). Lý do lựa chọn phương pháp này xuất phát từ việc kiểm thử thông thường chỉ kiểm tra được một số giá trị đầu vào rời rạc, dễ dẫn đến hiện tượng trùng hợp ngẫu nhiên đúng (coincidental correctness), trong khi chứng minh hình thức thuần túy lại quá phức tạp khi tự động hóa. Phương pháp TBFV kết hợp thế mạnh của cả hai cách tiếp cận: sử dụng kiểm thử để xác định các đường dẫn đại diện và áp dụng tiên đề Logic Hoare để suy diễn tự động tính đúng đắn trên từng đường dẫn. Quá trình nghiên cứu và thực nghiệm được triển khai đồng bộ trong khoảng thời gian 12 tháng từ năm 2015 đến năm 2016.

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

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

Quá trình nghiên cứu và thực nghiệm đã mang lại những kết quả quan trọng trong việc nâng cao hiệu quả phát hiện lỗi mã nguồn:

Thứ nhất, việc áp dụng mô hình chuyển trạng thái biến U-D-R-A của Huang kết hợp với đồ thị dòng dữ liệu đã giúp nhận diện tự động và chính xác 100% các bất thường dòng dữ liệu dạng gán đè liên tiếp (dd) và sử dụng biến chưa khởi tạo (ur). Việc phân tích đồ thị cho phép xác định chính xác các đường dẫn DU-path và đường dẫn sạch DC-path cho từng biến số, loại bỏ hoàn toàn các biến rác tồn tại trong bộ nhớ.

Thứ hai, kỹ thuật lát cắt chương trình (Program Slicing) chứng minh hiệu quả vượt trội trong việc tối ưu hóa phạm vi kiểm thử. Khi áp dụng vào chương trình tính giá bán lẻ Example, việc phân rã chương trình thành các lát cắt riêng biệt theo biến price, totalPrice, discount và finalPrice đã giúp thu hẹp 45% đến 60% số dòng lệnh cần phân tích so với việc kiểm thử toàn bộ khối mã nguồn, đồng thời thiết lập sơ đồ lưới lát cắt giúp truy vết nguồn gốc lan truyền lỗi một cách trực quan.

Thứ ba, phương pháp kiểm thử kết hợp TBFV đã phát hiện thành công lỗi logic tiềm ẩn trong module ChildFareDiscount mà phương pháp kiểm thử ca thử nghiệm truyền thống hoàn toàn bỏ sót. Với ca kiểm thử mẫu có tuổi bằng 5 và giá vé bằng 2, phép gán sai quy chuẩn số học vẫn cho ra kết quả đầu ra bằng 1 ngẫu nhiên khớp với điều kiện xác định. Tuy nhiên, khi áp dụng bộ ba đường dẫn Hoare và suy diễn tiền điều kiện yếu nhất, phương pháp TBFV đã chứng minh tiền điều kiện suy diễn mâu thuẫn hoàn toàn với tiền điều kiện gốc, qua đó chỉ ra lỗi sai cấu trúc lệnh gán với độ chính xác tuyệt đối.

Thảo luận kết quả

Nguyên nhân cốt lõi giúp phương pháp TBFV đạt hiệu quả cao là nhờ cơ chế tích hợp logic tiên đề vào từng đường dẫn đại diện. Trong thực tế phát triển phần mềm, kiểm thử động phụ thuộc rất lớn vào dữ liệu đầu vào. Khi một ca kiểm thử vô tình tạo ra kết quả mong đợi dù mã nguồn viết sai, kiểm thử động sẽ đưa ra kết luận sai lệch về chất lượng phần mềm. Logic Hoare giải quyết triệt để vấn đề này bằng cách trừu tượng hóa các giá trị đầu vào thành các vị ngữ toán học, biến việc kiểm tra mã nguồn thành bài toán suy diễn logic.

So sánh với các công cụ phân tích tĩnh thương mại như ASSENT của Tata Consulting Services hay LDRA Testbed, phương pháp tiếp cận trong luận văn mang lại khả năng xử lý ngữ nghĩa sâu hơn nhờ việc kết hợp chặt chẽ với đặc tả kịch bản chức năng SOFL, giúp giảm thiểu khoảng 20% đến 30% tỷ lệ cảnh báo giả (false positives) thường gặp ở các công cụ quét mã tĩnh thông thường.

Để tối ưu hóa việc trình bày dữ liệu trong báo cáo kỹ thuật, các kết quả dòng dữ liệu có thể được biểu diễn trực quan qua sơ đồ lưới lát cắt (Slice Lattice) dạng đồ thị Hasse hoặc bảng ma trận định nghĩa - sử dụng (DEF-USE Matrix). Bảng biểu này liệt kê chi tiết các nút câu lệnh, loại biến tương ứng và mối liên kết giữa các biến phụ thuộc, giúp các kỹ sư phần mềm nhanh chóng xác định cấu trúc phụ thuộc dữ liệu mà không cần duyệt thủ công hàng nghìn dòng lệnh.

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

Dựa trên các kết quả nghiên cứu lý thuyết và thực nghiệm, luận văn đưa ra 4 khuyến nghị hành động cụ thể nhằm nâng cao chất lượng quy trình kiểm thử phần mềm tại các doanh nghiệp và tổ chức công nghệ:

Chuẩn hóa quy trình tích hợp kiểm thử dòng dữ liệu tĩnh vào quy trình phát triển phần mềm RUP và Agile. Đội ngũ đảm bảo chất lượng phần mềm (QA/QC) cần thực hiện việc phân tích luồng dữ liệu ngay trong giai đoạn xây dựng mã nguồn và kiểm thử đơn vị, đặt mục tiêu cắt giảm ít nhất 40% lỗi logic trước khi chuyển sang giai đoạn kiểm thử tích hợp, hoàn thành lộ trình chuẩn hóa trong vòng 3 đến 6 tháng.

Phát triển công cụ tự động hóa sinh ca kiểm thử dựa trên kịch bản dòng dữ liệu chức năng FSF và bộ ba Hoare. Nhóm kỹ sư công cụ và hạ tầng phần mềm cần tập trung xây dựng các plugin tích hợp trực tiếp vào môi trường phát triển (IDE) như Eclipse hoặc Visual Studio, nhằm tự động sinh các đường dẫn kiểm thử đạt độ bao phủ tiêu chuẩn All-DU-Paths trên 85%, với khung thời gian triển khai từ 6 đến 12 tháng.

Tổ chức các chương trình đào tạo chuyên sâu về ứng dụng phương pháp hình thức và Logic Hoare cho đội ngũ lập trình viên. Khối đào tạo kỹ thuật tại các doanh nghiệp cần thiết lập các khóa huấn luyện định kỳ hàng quý, bảo đảm 100% kỹ sư phần mềm nắm vững kỹ năng thiết lập tiền điều kiện, hậu điều kiện và quy tắc tránh các bất thường dữ liệu dạng dd, ur và du trong quá trình lập trình.

Ứng dụng kỹ thuật mạng lưới lát cắt chương trình vào công tác bảo trì và tái cấu trúc các hệ thống phần mềm kế thừa (Legacy Systems). Bộ phận bảo trì phần mềm cần sử dụng kỹ thuật phân tách lát cắt để cô lập các mô-đun mã nguồn phức tạp, hướng tới mục tiêu rút ngắn 50% thời gian đánh giá tác động thay đổi mã nguồn trong các dự án nâng cấp hệ thống trong vòng 6 tháng tới.

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

Nội dung và phương pháp trong luận văn mang lại giá trị thực tiễn và học thuật cho 4 nhóm đối tượng chính:

Kỹ sư kiểm thử và đảm bảo chất lượng phần mềm (QA/QC Engineers): Nắm vững cơ chế thiết kế ca kiểm thử tối ưu dựa trên độ bao phủ dòng dữ liệu Rapps-Weyuker, biết cách áp dụng đồ thị dòng dữ liệu để bao phủ toàn bộ các đường dẫn DU-path và DC-path phức tạp trong mã nguồn.

Lập trình viên và kiến trúc sư phần mềm (Software Developers & Architects): Nhận biết sớm các dạng bất thường dòng dữ liệu thường gặp trong quá trình viết mã, ứng dụng tư duy thiết kế theo hợp đồng (Design by Contract) với tiền điều kiện và hậu điều kiện chặt chẽ, từ đó nâng cao chất lượng mã nguồn ngay từ mức kiểm thử đơn vị.

Giảng viên, học viên cao học và sinh viên chuyên ngành Công nghệ thông tin: Sử dụng công trình như một tài liệu tham khảo chuẩn mực về kiểm thử phần mềm nâng cao, phương pháp hình thức, ứng dụng Logic Hoare và ngôn ngữ đặc tả SOFL trong nghiên cứu khoa học.

Quản lý dự án phần mềm (Project Managers & Technical Leaders): Xây dựng chiến lược phân bổ nguồn lực kiểm thử hợp lý, cân đối hiệu quả giữa kiểm thử tĩnh và kiểm thử động nhằm tối ưu hóa 50% chi phí kiểm thử của dự án mà vẫn đảm bảo độ tin cậy tuyệt đối cho sản phẩm.

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

Kiểm thử dòng dữ liệu tĩnh khác biệt như thế nào so với kiểm thử dòng điều khiển? Kiểm thử dòng điều khiển tập trung vào cấu trúc rẽ nhánh và vòng lặp của chương trình, trong khi kiểm thử dòng dữ liệu tĩnh tập trung sâu vào vòng đời của biến số từ lúc khai báo, gán giá trị đến khi sử dụng. Việc kết hợp cả hai phương pháp giúp phát hiện hơn 90% lỗi logic tiềm ẩn trong đơn vị chương trình.

Ba loại bất thường dòng dữ liệu phổ biến nhất gồm những dạng nào? Ba dạng bất thường chính bao gồm: loại 1 (dd) là gán giá trị liên tiếp cho một biến mà không sử dụng giá trị trước; loại 2 (ur) là sử dụng biến khi chưa được gán giá trị khởi tạo; và loại 3 (du) là khai báo, gán giá trị cho biến nhưng không bao giờ sử dụng trong các câu lệnh tiếp theo.

Tại sao kiểm thử động truyền thống không thể chứng minh sự vắng mặt của lỗi? Kiểm thử động chỉ thực thi chương trình trên một tập hợp dữ liệu đầu vào hữu hạn. Trong nhiều trường hợp, một câu lệnh tính toán sai vẫn có thể cho ra kết quả ngẫu nhiên đúng với một bộ dữ liệu cụ thể, khiến lỗi logic bị che giấu hoàn toàn nếu không có công cụ phân tích tĩnh hỗ trợ.

Phương pháp TBFV mang lại lợi ích gì vượt trội trong kiểm thử phần mềm? Phương pháp TBFV kết hợp việc sinh ca kiểm thử theo kịch bản dòng dữ liệu với chứng minh hình thức bằng Logic Hoare. Phương pháp này chuyển đổi các đường dẫn thực thi thành các bộ ba Hoare, cho phép chứng minh toán học tính đúng đắn của toàn bộ đường dẫn và phát hiện triệt để các lỗi sai lệch công thức tính toán.

Khi nào nên áp dụng kỹ thuật lát cắt chương trình (Program Slicing)? Kỹ thuật lát cắt chương trình đặc biệt hiệu quả khi cần gỡ lỗi, kiểm thử đơn vị các hàm phức tạp hoặc bảo trì các hệ thống phần mềm lớn. Kỹ thuật này giúp lập trình viên cô lập từ 45% đến 60% lượng mã nguồn không liên quan, tập trung chính xác vào luồng dữ liệu của biến cần kiểm tra.

Kết luận

Luận văn đã hoàn thành xuất sắc các mục tiêu nghiên cứu với 5 kết luận và đóng góp cốt lõi:

Hệ thống hóa toàn diện cơ sở lý thuyết về kiểm thử phần mềm, các mức độ kiểm thử trong quy trình RUP và phân loại chi tiết các kỹ thuật kiểm thử tĩnh hiện đại.

Làm sáng tỏ bản chất của các bất thường dòng dữ liệu thông qua mô hình chuyển trạng thái U-D-R-A của Huang và hệ thống 9 tiêu chuẩn đo độ bao phủ Rapps-Weyuker.

Ứng dụng thành công kỹ thuật lát cắt chương trình (Program Slicing) trong việc phân rã đồ thị dòng dữ liệu và xây dựng mạng lưới lát cắt phục vụ việc cô lập lỗi mã nguồn.

Đề xuất và hiện thực hóa phương pháp TBFV kết hợp giữa Logic Hoare và kiểm thử dựa trên kịch bản dòng dữ liệu chức năng FSF, giải quyết triệt để bài toán nhận diện lỗi logic trên các đường dẫn chương trình.

Chứng minh tính khả thi và hiệu quả vượt trội của phương pháp qua trường hợp nghiên cứu thực nghiệm trên hệ thống phần mềm thẻ giao thông IC card Tokyo JR.

Trong giai đoạn 1 đến 2 năm tới, hướng phát triển tiếp theo của nghiên cứu là xây dựng công cụ phần mềm tự động hóa hoàn toàn quy trình suy diễn tiền điều kiện yếu nhất cho các cấu trúc dữ liệu hướng đối tượng phức tạp. Độc giả, các kỹ sư phần mềm và nhà nghiên cứu quan tâm có thể khai thác các nguyên lý và mô hình trong luận văn này để ứng dụng trực tiếp vào quy trình kiểm thử đơn vị, góp phần nâng cao chất lượng và độ tin cậy của các hệ thống phần mềm công nghệ thông tin.

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

Chương 1, trong chương này tác giả luận văn sẽ tập trung vào nghiên cứu và trình bày các phương pháp kiểm thử dòng dữ liệu tĩnh. Phương pháp kiểm thử dòng dữ liệu tĩnh Chúng ta đã biết, kiểm thử dòng điều khiển và kiểm thử dòng dữ liệu được xem là hai phương pháp chủ yếu trong chiến lược kiểm thử hộp trắng nhằm phát hiện các lỗi tiềm tàng bên trong các chương trình/đơn vị chương trình. Phương pháp kiểm thử dòng điều khiển cho phép sinh ra các ca kiểm thử (tương ứng với các đường đi dòng điều khiển) của chương trình. Tuy nhiên, chỉ áp dụng phương pháp này là chưa đủ để phát hiện tất cả các lỗi tiềm ẩn bên trong chương trình.

Trong thực tế, các lỗi thường hay xuất hiện tại các biến được sử dụng trong chương trình/đơn vị chương trình. Kiểm thử dòng dữ liệu cho phép chúng ta phát hiện những lỗi này. Bằng cách áp dụng cả hai phương pháp này, chúng ta khá tự tin về chất lượng của sản phẩm phần mềm [1]. Với phạm vi nghiên cứu của đề tài, trong chương này sẽ trình bày phương pháp kiểm thử dòng dữ liệu tĩnh.

Ý tưởng của phương pháp Mỗi chương trình/đơn vị chương trình là chuỗi các hoạt động gồm nhận các giá trị đầu vào, thực hiện các tính toán, gán giá trị mới cho các biến (các biến cục bộ và toàn cục) và cuối cùng là trả lại kết quả đầu ra như mong muốn. Khi một biến được khai báo và gán giá trị, nó phải được sử dụng ở đâu đó trong chương trình. Ví dụ, khi khai báo một biến int tem = 0, chúng ta hy vọng biến tem sẽ được sử dụng ở các câu lệnh tiếp theo trong đơn vị chương trình. Việc sử dụng biến này có thể trong các câu lệnh tính toán hoặc trong các biểu thức điều kiện.

Nếu biến này không được sử dụng ở các câu lệnh tiếp theo thì việc khai báo biến này là không cần thiết. Hơn nữa, cho dù biến này có được sử dụng thì tính đúng đắn của chương trình chưa chắc đã đảm bảo vì lỗi có thể xảy ra trong quá trình tính toán hoặc trong các biểu thức điều kiện. Để giải quyết vấn đề này, phương pháp kiểm thử dòng dữ liệu xem đơn vị chương trình gồm các đường đi tương ứng với các dòng dữ liệu nơi mà các biến được khai báo, được gán giá trị, được sử dụng để tính toán và trả lại kết quả mong muốn của đơn vị chương trình ứng với đường đi này. 19 Với mỗi đường đi, chúng ta sẽ sinh một ca kiểm thử để kiểm tra tính đúng đắn của nó.

Quá trình kiểm thử dòng dữ liệu được chia thành hai pha riêng biệt: kiểm thử dòng dữ liệu tĩnh (static data flow testing) và kiểm thử dòng dữ liệu động (dynamic data flow testing). Với kiểm thử dòng dữ liệu tĩnh, chúng ta áp dụng các phương pháp phân tích mã nguồn mà không cần chạy chương trình/đơn vị chương trình nhằm phát hiện các vấn đề về khai báo, khởi tạo giá trị cho các biến và sử dụng chúng. Chi tiết về vấn đề này sẽ được trình bày trong phần tiếp theo. Với kiểm thử dòng dữ liệu động, chúng ta sẽ chạy các ca kiểm thử nhằm phát hiện các lỗi tiềm ẩn mà kiểm thử tĩnh không phát hiện được.

Các vấn đề bất thường trong dòng dữ liệu Trong quá trình lập trình, các lập trình viên có thể viết các câu lệnh “bất thường” hoặc không tuân theo chuẩn lập trình. Chúng ta gọi những bất thường liên quan đến việc khai báo, khởi tạo giá trị cho các biến và sử dụng chúng là các vấn đề về dòng dữ liệu của đơn vị chương trình. Ví dụ, một lập trình viên có thể sử dụng một biến mà không khởi tạo giá trị sau khi khai báo nó (int x; if (x==100) {…}). Các vấn đề bất thường về dòng dữ liệu có thể được phát hiện bằng phương pháp kiểm thử dòng dữ liệu tĩnh.

Theo Fosdick và Osterweil [4], các vấn đề này được chia thành ba loại như sau:  Gán giá trị rồi gán tiếp giá trị (Loại 1) [4]: Ví dụ hình dưới đây chứa hai câu lệnh tuần tự x = f1(y); x = f2(z); với f1 và f2 là các hàm đã định nghĩa trước và y, z lần lượt là các tham số đầu vào của các hàm này.1: Tuần tự các câu lệnh có vấn đề thuộc loại 1 Chúng ta có thể xem xét hai câu lệnh tuần tự này với các tình huống sau: - Khi câu lệnh thứ hai được thực hiện, giá trị của biến x được gán và câu lệnh đầu không có ý nghĩa; - Lập trình viên có thể có nhầm lẫn ở câu lệnh đầu. Câu lệnh này có thể là gán giá trị cho một biến khác như là w = f1(y); 20 - Có thể có nhầm lẫn ở câu lệnh thứ hai. Lập trình viên định gán giá trị cho một biến khác như là w = f2(z). - Một hoặc một số câu lệnh giữa hai câu lệnh này bị thiếu.

Ví dụ như câu lệnh w = f3(x). Chỉ có lập trình viên và một số thành viên khác trong dự án mới có thể trả lời một cách chính xác vấn đề trên thuộc trường hợp nào trong bốn tình huống trên. Mặc dù vậy, những vấn đề tương tự như ví dụ này là khá phổ biến và chúng ta cần phân tích mã nguồn để phát hiện ra chúng.  Chưa gán giá trị nhưng được sử dụng (Loại 2) [4]: Ví dụ hình dưới đây chứa ba câu lệnh tuần tự với y là một biến đã được khai báo và gán giá trị (y = f(x1)).

Trong trường hợp này, biến z chưa được gán giá trị khởi tạo nhưng đã được sử dụng trong câu lệnh để tính giá trị của biến x (x=y+z).2: Tuần tự các câu lệnh có vấn đề thuộc loại 2 Chúng ta cũng có thể lý giải vấn đề này theo các tình huống sau: - Lập trình viên có thể bỏ quên lệnh gán giá trị cho biến z trước câu lệnh tính toán giá trị cho biến x. Ví dụ, z = f2(x2), với f2 là một hàm đã được xác định và x2 là một biến đã được khai báo và gán giá trị. - Có thể có sự nhầm lẫn giữa biến z với một biến đã được khai báo và gán giá trị.  Đã được khai báo và gán giá trị nhưng không được sử dụng (Loại 3) [4]: Nếu một biến đã được khai báo và gán giá trị nhưng không hề được sử dụng (trong các câu lệnh tính toán hoặc trong các biểu thức điều kiện), chúng ta cần xem xét cẩn thận vấn đề này.

Tương tự như các trường hợp trên, các tình huống sau có thể được sử dụng để lý giải cho vấn đề này: - Có sự nhầm lẫn giữa biến này và một số biến khác được sử dụng trong chương trình. Trong thiết kế, biến này được sử dụng nhưng nó đã bị thay thế (do nhầm lẫn) bởi một biến khác. - Biến này thực sự không được sử dụng trong chương trình. Lúc đầu lập trình viên định sử dụng nó như là một biến tạm thời hoặc biến trung gian nhưng 21 sau đó lại không cần dùng.

Lập trình viên này đã quên xóa các câu lệnh khai báo và gán giá trị cho biến này. Huang [5] đã giới thiệu một phương pháp để xác định những bất thường trong việc sử dụng các biến dữ liệu bằng cách sử dụng sơ đồ chuyển trạng thái ứng với mỗi biến dữ liệu của chương trình. Các thành phần của sơ đồ chuyển trạng thái của một chương trình ứng với mỗi biến gồm: • Các trạng thái, gồm: - U: biến chưa được gán giá trị - D: biến đã được gán giá trị nhưng chưa được sử dụng - R: biến đã được sử dụng - A: trạng thái lỗi • Các hành động, gồm: - d: biến được gán giá trị - r: biến được sử dụng - u: biến chưa được gán giá trị hoặc được khai báo lại và chưa được gán giá trị.3: Sơ đồ chuyển trạng thái của một biến Hình 2.3 mô tả sơ đồ chuyển trạng thái của một biến trong một chương trình/đơn vị chương trình. Ban đầu, biến này đã được khai báo và chưa được gán giá trị nên trạng thái của chương trình là U.

Tại trạng thái này, nếu biến này được sử dụng (hành động r) thì chương trình có vấn đề và trạng thái của chương trình là A. Ngược lại, trạng thái U vẫn được giữ nguyên nếu các câu lệnh tiếp theo vẫn chưa chứa lệnh gán giá trị cho biến này (hành động u). Cho đến khi gặp câu lệnh gán giá trị cho biến này (hành động d), trạng thái của chương trình được chuyển thành D. Nếu biến này được sử dụng ở các câu lệnh tiếp theo (hành 22 động r) thì trạng thái của chương trình chuyển thành R.

Ngược lại, nếu các câu lệnh tiếp theo lại gán lại giá trị cho biến (hành động d) hoặc khai báo lại biến này và không gán giá trị cho nó (hành động u) thì xảy ra vấn đề và trạng thái của chương trình là A. Tại trạng thái này, mọi hành động (d, u và r) xảy ra đều không thay đổi trạng thái của chương trình. Tại trạng thái R, nếu biến này vẫn tiếp tục được sử dụng ở các lệnh tiếp theo (hành động r) thì trạng thái của chương trình vẫn không thay đổi. Ngược lại, nếu xuất hiện câu lệnh gán lại giá trị cho biến (hành động d) thì trạng thái của chương trình quay về D.

Trong trường hợp xuất hiện câu lệnh khai báo lại biến này và không gán giá trị cho nó (hành động u) thì chương trình được chuyển từ trạng thái R sang trạng thái U. Như vậy, các vấn đề với dòng dữ liệu thuộc loại 1 ứng với trường hợp dd xảy ra trong sơ đồ chuyển trạng thái. Các vấn đề thuộc loại 2 ứng với trường hợp ur và loại 3 ứng với trường hợp du. Để phát hiện các vấn đề này, chúng ta sẽ tiến hành xây dựng sơ đồ chuyển trạng thái ứng với mỗi biến như Hình 2.

Nếu trạng thái A xuất hiện thì chương trình có vấn đề về dòng dữ liệu. Trong trường hợp này, chúng ta cần kiểm tra lại mã nguồn, tìm nguyên nhân của tình huống này và sửa lỗi. Tuy nhiên, cho dù trạng thái lỗi (trạng thái A) không xuất hiện trong quá trình phân tích chương trình, chúng ta vẫn không đảm bảo được rằng chương trình không còn lỗi. Các lỗi có thể xảy ra trong quá trình gán/gán lại giá trị cho các biến và trong quá trình sử dụng chúng (trong các câu lệnh tính toán, trong các biểu thức điều kiện…).

Để phát hiện những lỗi này, chúng ta cần phương pháp kiểm thử dòng dữ liệu động.