I. Tổng Quan Về Kiểm Chứng Từng Phần Chương Trình C
Đảm bảo chất lượng phần mềm là một hoạt động quan trọng và khó khăn trong quy trình phát triển phần mềm. Hoạt động này chiếm thời gian và kinh phí lớn (khoảng 15-20%) trong kinh phí của mỗi dự án. Có nhiều phương pháp được sử dụng để đảm bảo chất lượng phần mềm. Kiểm thử phần mềm đang là giải pháp phổ biến nhất. Tuy nhiên, kiểm thử chỉ cho phép chỉ ra các lỗi của phần mềm chứ không có khả năng chứng minh hệ thống không còn lỗi. Để chứng minh tính đúng đắn của các hệ thống, kiểm chứng mô hình đang được quan tâm như một giải pháp hiệu quả nhất và ngày càng được sử dụng rộng rãi, đặc biệt là trong các hệ thống phần mềm đòi hỏi độ chính xác cao. Kiểm chứng mô hình là một nhóm các kỹ thuật ứng minh tự động tính đúng đắn của hệ thống với các đặc tả thuộc tính nào đó. Với mục đích này, các kỹ thuật kiểm chứng mô hình phải xây dựng mô hình hình thức đặc tả chính xác hành vi của hệ thống cần kiểm chứng. Mô hình là một hệ thống bao gồm tập hợp có giới hạn các trạng thái và tập hợp các bước chuyển tiếp giữa các trạng thái đó. Kiểm chứng mô hình là chứng minh tính đúng đắn của mô hình bằng cách xác định xem thuộc tính mà người dùng mong muốn có được thỏa mãn bởi mô hình đó hay không [6]. Trong kiểm chứng mô hình phần mềm có hai bài toán được quan tâm chính đó là kiểm chứng tính đúng đắn của đặc tả thiết kế và kiểm chứng tính đúng đắn của mã nguồn. Bài toán kiểm chứng tự động mã nguồn được xem là ứng dụng đầu tiên của kiểm chứng mô hình trong việc đảm bảo chất lượng phần mềm. Dù cách tiếp cận này đã được đề xuất từ lâu nhưng đến nay nó vẫn là vấn đề mở và chưa có giải pháp thỏa đáng do gặp phải vấn đề bùng nổ không gian trạng thái và khó khăn trong việc xây dựng mô hình đặc tả hành vi của mã nguồn. Vì vậy kiểm chứng mã nguồn vẫn nhận được sự quan tâm rộng rãi trong nghiên cứu cũng như trong ứng dụng công nghiệp.
1.1. Tầm Quan Trọng Của Kiểm Chứng Chương Trình C
Việc kiểm chứng chương trình C đóng vai trò then chốt trong việc đảm bảo tính tin cậy và an toàn của phần mềm. Các hệ thống nhúng, hệ điều hành và nhiều ứng dụng quan trọng khác được viết bằng C, do đó việc phát hiện và sửa lỗi sớm là vô cùng quan trọng. Kiểm chứng từng phần giúp tập trung vào các thành phần quan trọng, giảm thiểu chi phí và thời gian so với kiểm chứng toàn bộ. Theo một nghiên cứu, việc phát hiện lỗi ở giai đoạn sớm giúp giảm chi phí sửa lỗi lên đến 100 lần.
1.2. Thách Thức Trong Chứng Minh Tính Đúng Đắn Chương Trình C
Một trong những thách thức lớn nhất trong chứng minh tính đúng đắn chương trình C là độ phức tạp của ngôn ngữ và sự tương tác với phần cứng. Các kỹ thuật phân tích tĩnh và kiểm thử truyền thống thường không đủ để phát hiện tất cả các lỗi tiềm ẩn. Kiểm chứng hình thức cung cấp một giải pháp mạnh mẽ hơn, nhưng đòi hỏi kiến thức chuyên sâu và công cụ hỗ trợ phù hợp. Vấn đề bùng nổ trạng thái cũng là một rào cản lớn, đặc biệt đối với các chương trình lớn và phức tạp.
II. Phương Pháp Kiểm Chứng Từng Phần Hiệu Quả Cho C
Xem xét một chương trình C có mã nguồn lớn và tồn tại nhiều lời gọi đến các hàm thư viện hoặc các hàm do người phát triển định nghĩa. Phương pháp hiện tại để kiểm chứng chương trình này là xây dựng một mô hình đặc tả toàn bộ hành vi của chương trình bao gồm cả hành vi của các hàm được gọi trong chương trình. Để làm được việc này, yêu cầu là phải có tất cả mã nguồn của các hàm này. Tuy nhiên, chúng ta thường khó khăn trong việc có đầy đủ mã nguồn và tài liệu đặc tả của các hàm được gọi vì trong nhiều trường hợp chúng ta sử dụng đến thư viện của các bên thứ ba. Kết quả là, chúng ta không áp dụng được phương pháp hiện tại cho bài toán này. Cho dù chúng ta có đủ mã nguồn của các hàm được gọi, việc áp dụng phương pháp kiểm chứng này cũng sẽ gặp phải bài toán bùng nổ không gian trạng thái vì kích thước của chương trình cộng với mã nguồn của các hàm được gọi là rất lớn. Trong luận văn này tôi xin giới thiệu một phương pháp mới [3] [4] trong kiểm chứng tự động để kiểm chứng một cài đặt của chương trình C có mã nguồn lớn và có nhiều thành phần nhằm giải quyết các vấn đề nêu trên. Cách tiếp cận của phương pháp là chúng ta đưa việc kiểm chứng một chương trình phần mềm lớn về việc kiểm chứng các thành phần con nhỏ hơn và đơn giản hơn bằng cách trừu tượng hóa hành vi [3] (procedure abstraction- PA) của các thành phần con (hay các hàm thư viện) theo một khái niệm đặc tả của máy hữu hạn trạng thái đó là hệ thống chuyển trạng thái được gán nhãn LTS (Labeled Transition System) [4]. Phương pháp cho phép chúng ta tự định nghĩa các hành vi của các hàm thư viện (chưa có mã nguồn hoặc chưa rõ hành vi) và sử dụng chúng như là giả thiết trong quá trình xây dựng mô hình kiểm chứng. Nội dung chính của luận văn là giới thiệu phương pháp kiểm chứng phần cài đặt của một chương trình viết bằng ngôn ngữ C có đảm bảo đúng với đặc tả của nó. Để làm được điều đó, trước hết từ mã nguồn C chúng ta phải xây dựng được mô hình LTS biểu diễn hành vi của chương trình bằng phương pháp trừu tượng mệnh đề (predicate abstraction) kết hợp với các LTS giả thiết biểu diễn hành vi của các thành phần con, sau đó sử dụng kỹ thuật kiểm chứng để kiểm định xem nó có đảm bảo đúng với mô hình LTS của đặc tả hay không.
2.1. Logic Hoare Trong Kiểm Chứng Từng Phần Chương Trình C
Logic Hoare là một hệ thống hình thức để chứng minh tính đúng đắn của chương trình bằng cách sử dụng tiền điều kiện và hậu điều kiện. Trong kiểm chứng từng phần, Logic Hoare có thể được áp dụng để xác minh tính đúng đắn của từng hàm hoặc khối lệnh, đảm bảo rằng chúng đáp ứng các yêu cầu đặt ra. Ví dụ, có thể sử dụng Logic Hoare để chứng minh rằng một hàm sắp xếp mảng sẽ trả về một mảng đã được sắp xếp đúng cách.
2.2. Sử Dụng Invariant Vòng Lặp Để Kiểm Chứng Tính Đúng Đắn
Invariant vòng lặp là một điều kiện luôn đúng trước, trong và sau mỗi lần lặp của vòng lặp. Việc xác định và chứng minh invariant vòng lặp là một kỹ thuật quan trọng trong kiểm chứng từng phần. Bằng cách chứng minh rằng invariant vòng lặp được duy trì trong suốt quá trình thực thi, có thể chứng minh tính đúng đắn của vòng lặp và các đoạn mã liên quan. Ví dụ, trong một vòng lặp tính tổng các phần tử của mảng, invariant có thể là tổng hiện tại luôn bằng tổng của các phần tử đã được duyệt.
2.3. Weakest Precondition và Strongest Postcondition
Weakest precondition (tiền điều kiện yếu nhất) là điều kiện yếu nhất cần thiết để đảm bảo rằng một đoạn mã sẽ đáp ứng một hậu điều kiện nhất định. Strongest postcondition (hậu điều kiện mạnh nhất) là điều kiện mạnh nhất có thể được đảm bảo sau khi thực thi một đoạn mã với một tiền điều kiện nhất định. Sử dụng weakest precondition và strongest postcondition giúp xác định chính xác các điều kiện cần thiết để đảm bảo tính đúng đắn của chương trình.
III. Xây Dựng Mô Hình LTS Cho Kiểm Chứng Chương Trình C
Nội dung chính của luận văn, đó là nêu cách xây dựng mô hình LTS biểu diễn hành vi của hệ thống từ mã nguồn bắt đầu bằng việc xây dựng sơ đồ luồng xử lý CFA (Control Flow Automata) [3] và sơ đồ luồng xử lý mở rộng (Expanding control flow Automata) [3] của chương trình có sử dụng các LTS giả thiết. Giới thiệu phương pháp trừu tượng mệnh đề để xây dựng được mô hình LTS biểu diễn hành vi của mã nguồn từ sơ đồ luồng xử lý mở rộng. Và cuối cùng nêu các kiểm chứng mô hình LTS của phần cài đặt có đảm bảo với mô hình LTS của đặc tả.
3.1. Đồ Thị Luồng Điều Khiển CFG và Automata Luồng Điều Khiển CFA
Đồ thị luồng điều khiển (CFG) là một biểu diễn đồ họa của tất cả các đường dẫn có thể được thực thi thông qua một chương trình. Automata luồng điều khiển (CFA) là một mô hình hình thức của CFG, được sử dụng để phân tích và kiểm chứng chương trình. CFA giúp xác định các trạng thái và chuyển đổi trạng thái của chương trình, từ đó giúp phát hiện các lỗi tiềm ẩn.
3.2. Trừu Tượng Hóa Mệnh Đề Trong Xây Dựng Mô Hình LTS
Trừu tượng hóa mệnh đề là một kỹ thuật để giảm độ phức tạp của mô hình bằng cách thay thế các biểu thức phức tạp bằng các mệnh đề đơn giản. Trong kiểm chứng chương trình C, trừu tượng hóa mệnh đề giúp tạo ra các mô hình LTS nhỏ gọn hơn, dễ quản lý và kiểm chứng hơn. Ví dụ, một biểu thức số học phức tạp có thể được thay thế bằng một mệnh đề cho biết liệu kết quả của biểu thức có dương hay không.
3.3. Sử Dụng LTS Giả Thiết Cho Các Hàm Thư Viện
Khi kiểm chứng chương trình C, thường gặp phải các hàm thư viện mà không có mã nguồn hoặc đặc tả đầy đủ. Trong trường hợp này, có thể sử dụng LTS giả thiết để mô tả hành vi của các hàm này. LTS giả thiết là một mô hình LTS được xây dựng dựa trên hiểu biết về hành vi của hàm, và được sử dụng như một giả định trong quá trình kiểm chứng. Việc sử dụng LTS giả thiết cho phép kiểm chứng từng phần chương trình mà không cần phải có đầy đủ thông tin về tất cả các thành phần.
IV. Ứng Dụng Thực Tế Công Cụ Coper Cho Kiểm Chứng C
Chương 4 luận văn đưa ra ứng dụng của phương pháp bằng cách giới thiệu các công cụ Coper [2]. Đầu vào của công cụ này là tập file mã nguồn C của chương trình và các đặc tả của các thuộc tính cần kiểm chứng, đầu ra là kết luận phần cài đặt đã đúng với đặc tả của nó hoặc đưa ra phản ví dụ chứng minh cài đặt không đúng với đặc tả. Trong chương này giới thiệu một vài ứng dụng đơn giản được áp dụng thực tế trên công cụ bằng cách nêu chi tiết cách xây dựng các file đặc tả cũng như cách xây dựng các PA giả thiết bằng ví dụ. Phần cuối của luận văn trình bày những kết quả đạt được, hướng nghiên cứu phát triển trong tương lai và những hạn chế cần khắc phục.
4.1. Giới Thiệu Công Cụ Coper Trong Kiểm Chứng Chương Trình C
Coper là một công cụ tự động để kiểm chứng chương trình C dựa trên kỹ thuật kiểm chứng mô hình. Coper cho phép người dùng xác định các thuộc tính cần kiểm chứng bằng ngôn ngữ đặc tả hình thức, và tự động xây dựng mô hình LTS từ mã nguồn C. Coper cũng hỗ trợ việc sử dụng LTS giả thiết cho các hàm thư viện, giúp kiểm chứng từng phần chương trình một cách hiệu quả.
4.2. Ví Dụ Ứng Dụng Coper Để Gỡ Lỗi Chương Trình C
Coper có thể được sử dụng để phát hiện các lỗi phổ biến trong chương trình C, chẳng hạn như lỗi tràn bộ đệm, lỗi sử dụng con trỏ không hợp lệ và lỗi đồng bộ hóa. Bằng cách xác định các thuộc tính an toàn và liveness, người dùng có thể sử dụng Coper để tự động tìm kiếm các vi phạm và cung cấp các phản ví dụ giúp gỡ lỗi chương trình C một cách nhanh chóng.
4.3. Đánh Giá Hiệu Quả Của Coper Trong Kiểm Chứng Từng Phần
Việc đánh giá hiệu quả của Coper trong kiểm chứng từng phần chương trình C là rất quan trọng. Các thử nghiệm thực nghiệm cho thấy rằng Coper có thể kiểm chứng các chương trình lớn và phức tạp một cách hiệu quả, đặc biệt khi sử dụng LTS giả thiết cho các hàm thư viện. Tuy nhiên, hiệu quả của Coper phụ thuộc vào chất lượng của các đặc tả và LTS giả thiết.
V. Kết Luận Và Hướng Phát Triển Kiểm Chứng Chương Trình C
Trong chương này chúng ta sẽ tìm hiểu một số khái niệm cần thiết như máy hữu hạn trạng thái, hệ chuyển trạng thái được gán nhãn và khái niệm về trừu tượng hóa hành vi một chương trình…
5.1. Tóm Tắt Các Kết Quả Đạt Được Trong Nghiên Cứu
Nghiên cứu đã trình bày một phương pháp mới để kiểm chứng từng phần chương trình C bằng cách sử dụng LTS giả thiết và trừu tượng hóa mệnh đề. Phương pháp này cho phép kiểm chứng các chương trình lớn và phức tạp một cách hiệu quả, đặc biệt khi không có đầy đủ thông tin về các hàm thư viện. Các thử nghiệm thực nghiệm với công cụ Coper đã chứng minh tính khả thi và hiệu quả của phương pháp.
5.2. Hướng Nghiên Cứu Phát Triển Trong Tương Lai
Trong tương lai, có thể phát triển phương pháp này bằng cách tự động hóa quá trình xây dựng LTS giả thiết và cải thiện hiệu quả của thuật toán kiểm chứng mô hình. Ngoài ra, có thể mở rộng phương pháp để hỗ trợ các tính năng khác của ngôn ngữ C, chẳng hạn như con trỏ và cấu trúc dữ liệu phức tạp. Nghiên cứu cũng có thể tập trung vào việc tích hợp phương pháp này với các công cụ phát triển phần mềm khác, chẳng hạn như trình biên dịch và trình gỡ lỗi.
5.3. Các Hạn Chế Cần Khắc Phục Trong Kiểm Chứng C
Mặc dù phương pháp đã đạt được những kết quả đáng khích lệ, vẫn còn một số hạn chế cần khắc phục. Việc xây dựng LTS giả thiết vẫn đòi hỏi kiến thức chuyên sâu về hành vi của các hàm thư viện. Ngoài ra, hiệu quả của phương pháp phụ thuộc vào chất lượng của các đặc tả và LTS giả thiết. Trong tương lai, cần phát triển các kỹ thuật để tự động hóa quá trình xây dựng LTS giả thiết và cải thiện độ chính xác của các đặc tả.
