chương 1. Chương 2 trình bày về kiểm chứng chương trình, thực thi tượng trưng và một số kỹ thuật thực thi tượng trưng hiện đại đang được áp dụng trong các công cụ kiểm chứng. Chương 3 trình bày về SMT một công cụ giải các công thức logic trên lý thuyết vị từ cấp I và việc áp dụng SMT, thực thi tượng trưng để kiểm chứng chương trình trên một số lý thuyết cụ thể. Chương 4 trình bày về công cụ KLEE, thực nghiệm trên công cụ KLEE và các ứng dụng của nó trong việc kiểm chứng và phát hiện những lỗi của chương trình.
Phần kết luận trình bày kết luận quá trình nghiên cứu, đưa ra các kết quả đạt được và hướng nghiên cứu tiếp theo. TIEU LUAN MOI download : skknchat@gmail.com 3 Chƣơng 2. KIỂM CHỨNG CHƢƠNG TRÌNH VÀ THỰC THI TƢỢNG TRƢNG Kiểm chứng chương trình là một trong những vấn đề quan trọng quyết định đến chất lượng phần mềm. Trong chương này luận văn trình bày về kiểm chứng chương trình, kỹ thuật kiểm chứng mô hình.
Đồng thời luận văn cũng trình bày về thực thi tượng trưng (symbolic execution), thực thi tượng trưng động và một số giải pháp khắc phục những vấn đề phát sinh trong thực thi tượng trưng. Kiểm chứng chƣơng trình Kiểm chứng chương trình là một trong những giai đoạn quan trọng trong quy trình sản xuất phần mềm. Các vấn đề tổng quan về kiểm chứng chương trình, kỹ thuật kiểm chứng mô hình sẽ được trình bày ngay sau đây. Tổng quan về kiểm chứng chƣơng trình Hai kỹ thuật chủ yếu được áp dụng để đảm bảo chất lượng phần mềm hiện nay đó là kỹ thuật kiểm thử (Software testing) và kỹ thuật kiểm chứng (Software verification).
Trong khi các kỹ thuật kiểm thử chỉ được thực hiện khi đã có mã nguồn hệ thống và cũng chỉ có khả năng phát hiện những lỗi hoặc khiếm khuyết của hệ thống mà không thể khẳng định được là chương trình không còn lỗi. Do đó, áp dụng kỹ thuật kiểm thử không thôi thì chưa đủ để đảm bảo chất lượng của hệ thống. Các kỹ thuật kiểm chứng có thể giải quyết được vấn đề này. Kiểm chứng [1] là hoạt động giúp đánh giá một hệ thống phần mềm bằng cách xác định sản phẩm ở các pha phát triển có thỏa mãn các đặc tả yêu cầu phần mềm hoặc các thuộc tính của chương trình có thỏa mãn hay không? Sản phẩm ở đây có thể hiểu là sản phẩm trung gian như: Đặc tả yêu cầu, thiết kế chi tiết, mã nguồn.
Những hoạt động kiểm tra tính đúng đắn của các pha phát triển được gọi là hoạt động kiểm chứng. Kiểm chứng trả lời cho câu hỏi “Hệ thống TIEU LUAN MOI download : skknchat@gmail.com 4 được xây dựng có đúng với đặc tả”. Mục đích của hoạt động kiểm chứng là xác thực xem đã xây dựng đúng sản phẩm. Về cơ bản, kiểm chứng hệ thống là kỹ thuật được áp dụng để xác minh tính đúng đắn của một thiết kế, một sản phẩm.
Đó là những đặc tả quy định các hành vi đã thực hiện của hệ thống và những gì hệ thống không thực hiện từ đó tạo cơ sở cho hoạt động kiểm chứng. Hệ thống được coi là đúng nếu nó thỏa mãn tất cả các thuộc tính thu được từ các đặc tả cụ thể của nó. Sơ đồ minh họa quá trình kiểm chứng được trình bày trong hình 2. Đặc tả (System Specification) Các thuộc tính (Properties) Quy trình thiết kế (Design Process) Kiểm chứng Sản phẩm hoặc bản thử (Verification) (product of prototype) Phát hiện lỗi Không tìm thấy (bug (s) found) lỗi (no bugs found) Hình 2.
Sơ đồ của hệ thống kiểm chứng [3] 2. Kiểm chứng mô hình Các kỹ thuật kiểm chứng đang được sử dụng hiện nay đó là áp dụng các phương pháp hình thức (formal methods). Mục đích của các phương pháp này là cố gắng chứng minh một cách tự động rằng chương trình sẽ thực thi đúng đắn TIEU LUAN MOI download : skknchat@gmail.com 5 trên mọi môi trường được đặc tả. Có thể kể đến một số phương pháp như: Phương pháp suy diễn (deductive methods), kiểm chứng mô hình (model checking), định kiểu chương trình (program typing), phân tích chương trình tĩnh (static program analysis).
Trong số các phương pháp kể trên, phương pháp kiểm chứng mô hình (model checking) là phương pháp ra đời khá sớm. Tuy nhiên, nó còn hạn chế là chỉ áp dụng được cho các hệ thống nhỏ. Phần tiếp theo sẽ tập trung trình bày về kỹ thuật này. Kỹ thuật kiểm chứng mô hình [3] là kỹ thuật mô tả những hành vi có thể có của hệ thống dưới dạng các công thức toán học rõ ràng, chính xác và biểu diễn hệ thống dưới dạng các trạng thái.
Kiểm chứng mô hình là kỹ thuật phát hiện lỗi chương trình theo cách thức vét cạn tất cả các trạng thái có thể có của hệ thống. Các công cụ kiểm chứng phần mềm mà sử dụng kỹ thuật kiểm chứng mô hình sẽ tiến hành kiểm tra tất cả những kịch bản có thể có của hệ thống. Bằng cách này, nó có thể chỉ ra rằng mô hình hệ thống có thật sự thỏa mãn các thuộc tính nhất định. Những thuộc tính của chương trình được kiểm tra bằng cách sử dụng mô hình có tính chất định tính như: Kết quả sinh ra liệu có chính xác.
Liệu hệ thống có gặp phải tình huống deadlock, ví dụ hai tiến trình cùng tiến hành chờ đợi nhau dẫn đến sự bế tắc của hệ thống. Kiểm chứng mô hình đòi hỏi phải có một khẳng định chính xác về các thuộc tính đã được kiểm tra của hệ thống. Việc mô hình hóa hệ thống một cách chính xác thường phát hiện được những lỗi tiềm ẩn của hệ thống. Các mô hình hệ thống thường được tự động tạo ra từ một mô tả về mô hình được thể hiện cho từng ngôn ngữ lập trình như C, Java hoặc ngôn ngữ mô tả phần cứng như Verilog.
Cần lưu ý rằng đặc tả thuộc tính quy định cái gì hệ thống nên làm và cái gì hệ thống không nên làm. Trong khi mô hình hóa hệ thống lại kiểm tra tất cả các trạng thái liên quan để kiểm tra xem chúng có thỏa mãn cái mà thuộc tính mong muốn. Phản ví dụ (Counterexample) mô tả một đường thực thi từ trạng thái khởi tạo của hệ thống tới trạng thái vi phạm thuộc TIEU LUAN MOI download : skknchat@gmail.com 6 tính đang được kiểm chứng. Cùng với sự trợ giúp của mô phỏng người sử dụng có thể xem lại kịch bản vi phạm, theo cách này thu thập thông tin gỡ lỗi hữu ích và phù hợp với mô hình.
Cách tiếp cận về kiểm chứng mô hình xem hình 2. Đặc tả Hệ thống (requirements) (System) (Hình thức Mô hình hóa hóa) (Modeling) Formalizing Đặc tả thuộc tính Mô hình hóa hệ (Property Specification) thống (System model) Kiểm chứng mô hình (Model Checking) Vi phạm + phản Mô phỏng Thỏa mãn ví dụ (Violated (Simulation) (Satisfied) + counterexample ) Lỗi cụ thể (local error) Hình 2. Mô hình hóa cách tiếp cận của kiểm chứng mô hình [3] Quy trình thực hiện của kiểm chứng mô hình được thể hiện qua các pha sau đây: TIEU LUAN MOI download : skknchat@gmail.com 7 Pha mô hình hóa (modeling phase): Điều kiện tiên quyết của các đầu vào của kiểm chứng mô hình là mô hình của hệ thống đang được xem xét và đặc trưng hình thức hóa của các thuộc tính được kiểm tra. Mô hình của hệ thống mô tả hành vi của hệ thống một cách rõ ràng chính xác.
Nó thường thể hiện bằng ôtômát hữu hạn bao gồm một tập hữu hạn các trạng thái và hàm chuyển tương ứng. Trạng thái bao gồm thông tin về các giá trị hiện tại của các biến, câu lệnh được thực hiện trước đó. Hàm chuyển mô tả cách thức để chuyển từ trạng thái hiện thời sang trạng thái khác. Để việc kiểm chứng cho kết quả đúng, các thuộc tính ở đầu vào cũng nên được mô tả một cách chính xác và rõ ràng.
Để làm được điều này thì sử dụng ngôn ngữ đặc tả thuộc tính. Sử dụng logic thời gian (temporal logic) là cách thức hiệu quả để đặc tả thuộc tính. Pha thực thi: Chạy bộ công cụ kiểm chứng để kiểm tra tính hợp lệ của các thuộc tính trong mô hình hệ thống. Pha phân tích: + Nếu một thuộc tính thỏa mãn thì tiếp tục với thuộc tính tiếp (nếu có).
+ Nếu thuộc tính vi phạm thực hiện: - Phân tích và sinh ra phản ví dụ bằng mô phỏng. - Cải tiến mô hình, cải tiến thiết kế hoặc thuộc tính. - Lặp lại toàn bộ thủ tục. + Nếu truy nhập ngoài bộ nhớ thì cố gắng giảm thiểu mô hình và thử lại.
Như đã trình bày ở trên, kỹ thuật kiểm chứng mô hình [16] được đánh giá là kỹ thuật hiệu quả được sử dụng nhiều trong các công cụ kiểm chứng với những ưu điểm sau: - Là kỹ thuật có thể thực hiện hoàn toàn tự động. - Thuật toán kiểm chứng mô hình sẽ kết thúc với câu trả lời đúng và đưa ra một mô hình cụ thể. Hoặc chỉ ra một phản ví dụ (counterexamples) là lý do tại sao biểu thức là không thỏa mãn. Các TIEU LUAN MOI download : skknchat@gmail.com 8 phản ví dụ đóng vai trò đặc biệt quan trọng trong việc phát hiện các lỗi của các hệ thống chuyển phức tạp.
- Thực hiện nhanh, cụ thể nó có thể thực hiện trên từng phần của hệ thống. Do đó, có thể tập trung vào những phần có nguy cơ phát sinh lỗi cao trước. Khi một trường hợp là không thỏa mãn, các công thức khác không thuộc trường hợp đó có thể được kiểm tra để xác định nguồn gốc của lỗi. - Cuối cùng, lý thuyết logic được sử dụng trong kỹ thuật này đóng vai trò quan trọng.
Nó thể hiện nhiều tính chất cần thiết cho lý luận về hệ thống hiện thời. Tuy nhiên kiểm chứng mô hình (model checking) cũng có những điểm hạn chế như sau: - Phương pháp này chủ yếu thích hợp với các ứng dụng điều khiển hơn là các ứng dụng hướng dữ liệu bởi vì dữ liệu thường vượt quá các miền vô hạn. - Nó chỉ kiểm tra các yêu cầu đã được trạng thái hóa. Nó không đảm bảo tính toàn vẹn.
Tính hợp lý của các thuộc tính không được kiểm chứng có thể không được đảm bảo. - Phương pháp này gặp phải trở ngại lớn nhất đó là vấn đề bùng nổ không gian trạng thái, số các trạng thái cần cho mô hình hệ thống có thể vượt quá bộ nhớ của máy vi tính. - Nó không đảm bảo cho ra kết quả chính xác hoàn toàn vì cũng như các công cụ khác thì bộ kiểm chứng cũng là một phần mềm và có thể có lỗi.