I. Giới thiệu
Trong lĩnh vực lập trình hiện đại, việc phát hiện và sửa lỗi trong chương trình là một thách thức lớn đối với các nhà phát triển phần mềm. Để giải quyết vấn đề này, nhiều công cụ kiểm tra phần mềm đã được phát triển, trong đó có các kỹ thuật phân tích MUST và MAY. Phân tích MUST đảm bảo rằng một thuộc tính nào đó của chương trình chắc chắn xảy ra trong một số đường thực thi nhất định, trong khi phân tích MAY chứng minh rằng thuộc tính đó luôn đúng cho tất cả các đường thực thi. Tuy nhiên, cả hai phương pháp này đều có nhược điểm riêng, dẫn đến việc cần thiết phải kết hợp chúng để tăng cường độ chính xác trong việc phát hiện lỗi. Đề tài này sẽ nghiên cứu và phát triển một hệ thống sinh logic test-case dựa trên kỹ thuật slicing, nhằm cải thiện khả năng kiểm tra chương trình, đặc biệt là các chương trình thao tác trên heap.
1.1 Tổng quan về đề tài
Đề tài tập trung vào việc nghiên cứu các kỹ thuật kiểm tra chương trình, đặc biệt là kỹ thuật concolic testing và slicing. Mục tiêu là xây dựng một hệ thống sinh logic test-case cho các chương trình viết bằng ngôn ngữ HIP. Hệ thống này sẽ kết hợp các kỹ thuật phân tích MUST và MAY để đảm bảo độ bao phủ cao nhất trong việc phát hiện lỗi. Việc áp dụng separation logic sẽ giúp mô tả chính xác hơn các chương trình thao tác trên heap, từ đó cải thiện hiệu quả của quá trình kiểm tra.
II. Các kiến thức nền tảng
Phân tích MUST và MAY là hai kỹ thuật quan trọng trong việc kiểm tra phần mềm. Kỹ thuật MUST giúp xác định các thuộc tính mà chương trình phải thỏa mãn, trong khi kỹ thuật MAY giúp chứng minh rằng một thuộc tính nào đó luôn đúng. Tuy nhiên, việc áp dụng riêng lẻ các kỹ thuật này có thể dẫn đến tình trạng báo lỗi không chính xác. Do đó, việc kết hợp chúng là cần thiết để tối ưu hóa quá trình kiểm tra. Hệ thống sinh logic test-case sẽ sử dụng các kỹ thuật này để tạo ra các test-case hiệu quả nhất, đảm bảo độ bao phủ cao trong việc phát hiện lỗi.
2.1 Tổng quan về separation logic
Separation logic là một công cụ mạnh mẽ để kiểm tra các chương trình có chứa con trỏ và cấu trúc dữ liệu chia sẻ. Nó mở rộng Hoare logic bằng cách thêm các toán tử mới, cho phép mô tả chính xác hơn các trạng thái của chương trình. Việc sử dụng separation logic giúp giải quyết vấn đề bí danh, một trong những thách thức lớn trong việc kiểm tra tính đúng đắn của chương trình. Bằng cách kết hợp separation logic với các kỹ thuật phân tích khác, hệ thống sinh logic test-case có thể tạo ra các test-case chính xác và hiệu quả hơn.
III. Hệ thống sinh logic test case
Hệ thống sinh logic test-case được xây dựng dựa trên các kỹ thuật slicing và concolic testing. Kỹ thuật slicing cho phép trích xuất các phần liên quan của chương trình, từ đó giảm thiểu số lượng test-case cần thiết mà vẫn đảm bảo độ bao phủ cao. Kết hợp với kỹ thuật concolic testing, hệ thống có thể tự động sinh ra các test-case cho các chương trình thao tác trên heap. Điều này không chỉ giúp phát hiện lỗi hiệu quả hơn mà còn giảm thiểu thời gian và chi phí trong quá trình kiểm tra.
3.1 Hệ thống sinh logic test case hoàn chỉnh
Hệ thống sinh logic test-case hoàn chỉnh sẽ bao gồm các thành phần chính như module sinh test-case, cơ chế kiểm tra tự động và các quy tắc hỗ trợ. Mỗi thành phần sẽ được thiết kế để tương tác với nhau một cách hiệu quả, đảm bảo rằng các test-case được sinh ra không chỉ chính xác mà còn có thể phát hiện được nhiều loại lỗi khác nhau trong chương trình. Hệ thống này sẽ là một công cụ hữu ích cho các nhà phát triển phần mềm trong việc kiểm tra và cải thiện chất lượng sản phẩm.
