I. Tổng quan về kiểm thử phần mềm
Kiểm thử phần mềm là một giai đoạn quan trọng trong quy trình phát triển phần mềm. Nó không chỉ giúp phát hiện lỗi mà còn đảm bảo rằng phần mềm hoạt động đúng theo yêu cầu. Kiểm thử phần mềm thường được chia thành hai giai đoạn chính: sinh ca kiểm thử và thực thi ca kiểm thử. Trong đó, việc sinh ca kiểm thử là một bước quan trọng, quyết định đến chất lượng của quá trình kiểm thử. Đặc biệt, trong các hệ thống lớn, việc sinh ca kiểm thử có thể chiếm tới 60% tổng chi phí phát triển phần mềm. Do đó, việc tự động hóa quá trình này trở nên cần thiết, đặc biệt là với các phần mềm phức tạp. Phương pháp kiểm thử dựa trên mô hình đã được phát triển nhằm giải quyết vấn đề này, cho phép sinh ca kiểm thử từ các mô hình đặc tả hành vi của hệ thống.
1.1 Khái niệm kiểm thử dựa trên mô hình
Kiểm thử dựa trên mô hình là một phương pháp trong đó các ca kiểm thử được sinh ra từ mô hình đặc tả hành vi của hệ thống. Mô hình này có thể được biểu diễn bằng các công cụ như UML 2.0. Quá trình này giúp giảm thiểu thời gian và chi phí trong việc tạo ra các kịch bản kiểm thử. Mô hình hóa hành vi của hệ thống cho phép kiểm thử viên dễ dàng xác định các tình huống kiểm thử và các đầu vào cần thiết. Việc sử dụng biểu đồ tuần tự trong UML 2.0 giúp mô tả các tương tác giữa các đối tượng trong hệ thống, từ đó tạo ra các ca kiểm thử một cách tự động và hiệu quả.
II. Phương pháp sinh đồ thị dòng điều khiển từ biểu đồ tuần tự
Phương pháp sinh đồ thị dòng điều khiển từ biểu đồ tuần tự là một bước quan trọng trong quy trình kiểm thử dựa trên mô hình. Đầu tiên, biểu đồ tuần tự được phân tích và chuyển đổi thành các khối (fragment) tương ứng. Các khối này có thể là tuần tự hoặc lồng nhau, tùy thuộc vào mối quan hệ giữa chúng. Sau khi xác định các khối, đồ thị dòng điều khiển được xây dựng từ các khối này. Việc chuyển đổi này không chỉ giúp tạo ra một mô hình rõ ràng mà còn tạo điều kiện cho việc phân tích và sinh ca kiểm thử. Kỹ thuật thực thi tượng trưng (Symbolic Execution) được áp dụng để xây dựng hệ ràng buộc cho tập đường kiểm thử. Cuối cùng, công cụ SMT solver được sử dụng để giải hệ ràng buộc và tìm kiếm nghiệm, từ đó sinh ra các ca kiểm thử.
2.1 Đồ thị dòng điều khiển
Đồ thị dòng điều khiển là một biểu diễn trực quan của các luồng điều khiển trong chương trình. Nó cho phép kiểm thử viên dễ dàng theo dõi các đường đi của chương trình và xác định các điểm có thể xảy ra lỗi. Việc xây dựng đồ thị dòng điều khiển từ biểu đồ tuần tự giúp tạo ra một mô hình rõ ràng hơn về cách thức hoạt động của phần mềm. Đồ thị này không chỉ hỗ trợ trong việc sinh ca kiểm thử mà còn giúp phát hiện các lỗi tiềm ẩn trong thiết kế phần mềm. Bằng cách phân tích đồ thị dòng điều khiển, kiểm thử viên có thể xác định các đường kiểm thử cần thiết để đảm bảo rằng tất cả các tình huống có thể xảy ra đều được kiểm tra.
III. Phương pháp sinh bộ kiểm thử từ đồ thị dòng điều khiển
Phương pháp sinh bộ kiểm thử từ đồ thị dòng điều khiển bao gồm hai bước chính: xây dựng hệ ràng buộc và tìm nghiệm thỏa mãn hệ ràng buộc. Đầu tiên, hệ ràng buộc được xây dựng dựa trên các đường kiểm thử đã xác định từ đồ thị dòng điều khiển. Kỹ thuật thực thi tượng trưng được sử dụng để tạo ra các ràng buộc tương ứng cho từng đường kiểm thử. Sau đó, công cụ SMT solver được áp dụng để giải hệ ràng buộc này. Quá trình này không chỉ giúp tìm ra các nghiệm thỏa mãn mà còn tạo ra các ca kiểm thử có thể được sử dụng để kiểm tra tính đúng đắn của phần mềm. Kết quả thực nghiệm cho thấy phương pháp này có tiềm năng ứng dụng cao trong việc kiểm thử tự động tại các công ty.
3.1 Xây dựng hệ ràng buộc
Xây dựng hệ ràng buộc là một bước quan trọng trong quá trình sinh ca kiểm thử. Hệ ràng buộc được tạo ra từ các đường kiểm thử đã xác định trong đồ thị dòng điều khiển. Mỗi đường kiểm thử sẽ tương ứng với một tập hợp các ràng buộc, phản ánh các điều kiện cần thiết để thực hiện đường kiểm thử đó. Việc xây dựng hệ ràng buộc không chỉ giúp xác định các điều kiện cần thiết mà còn tạo ra một cơ sở dữ liệu cho việc kiểm thử. Kỹ thuật thực thi tượng trưng được áp dụng để đảm bảo rằng tất cả các điều kiện đều được xem xét và kiểm tra một cách chính xác.
