Tài liệu Kiểm chứng chương trình dựa trên SMT

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ LÊ THỊ HẰNG KIỂM CHỨNG CHƢƠNG TRÌNH DỰA TRÊN SMT LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN Hà Nội - Năm 2014 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ LÊ THỊ HẰNG KIỂM CHỨNG CHƢƠNG TRÌNH DỰA TRÊN SMT Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60480103 LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN NGƢỜI HƢỚNG DẪN KHOA HỌC: TS. TÔ VĂN KHÁNH Hà Nội - Năm 2014 i LỜI CAM ĐOAN Tôi xin cam đoan rằng nội dung và những kết quả của luận văn tốt nghiệp: “Kiểm chứng chương trình dựa trên SMT là sản phẩm nghiên cứu của riêng tôi dưới sự giúp đỡ rất lớn từ TS. Tô Văn Khánh. Tôi không sao chép của người khác. Toàn bộ nội dung được trình bày trong luận văn này hoặc là của chính tôi hoặc là được tổng hợp từ nhiều nguồn tài liệu khác. Tất cả các tài liệu tham khảo đều được trích dẫn rõ ràng ở phần cuối của luận văn. Tôi xin hoàn toàn chịu trách nhiệm và chịu mọi hình thức kỷ luật theo quy định cho lời cam đoan của mình. Hà Nội, tháng 11 năm 2014 Học viên Lê Thị Hằng. ii LỜI CẢM ƠN Trước hết, tôi xin được bày tỏ lòng biết ơn chân thành và sâu sắc đến thầy giáo, TS. Tô Văn Khánh người đã dành nhiều tâm huyết và tận tình chỉ bảo giúp tôi hoàn thiện luận văn này. Tôi cũng xin gửi lời cám ơn đến tập thể các thầy cô giáo trong Khoa CNTT – Trường ĐH Công Nghệ - ĐH Quốc Gia Hà Nội . Những bài giảng của thầy cô là nền tảng kiến thức cơ bản giúp tôi hoàn thành luận văn ngày hôm nay. Cuối cùng, tôi xin gửi lời cảm ơn tới gia đình tôi – những người thân đã động viên tôi bằng cả vật chất lẫn tinh thần trong suốt thời gian tôi học tập và thực hiện luận văn này. Tuy rằng, tôi đã cố gắng hết sức trong quá trình làm luận văn nhưng không thể tránh khỏi thiếu sót, tôi rất mong nhận được những góp ý của thầy cô và các bạn. Hà Nội, tháng 11 năm 2014 Học viên Lê Thị Hằng iii MỤC LỤC LỜI CAM ĐOAN .............................................................................................. i LỜI CẢM ƠN ................................................................................................... ii MỤC LỤC ....................................................................................................... iii BẢNG CÁC THUẬT NGỮ VIẾT TẮT .......................................................... v DANH MỤC HÌNH VẼ................................................................................... vi Chƣơng 1. GIỚI THIỆU .................................................................................. 1 1.1. Đảm bảo chất lƣợng phần mềm ............................................................ 1 1.2. Mục tiêu của luận văn ........................................................................... 2 1.3. Nội dung luận văn .................................................................................. 2 Chƣơng 2. KIỂM CHỨNG CHƢƠNG TRÌNH VÀ THỰC THI TƢỢNG TRƢNG ............................................................................................................. 3 2.1. Kiểm chứng chƣơng trình ..................................................................... 3 2.1.1. Tổng quan về kiểm chứng chương trình ............................................ 3 2.1.2. Kiểm chứng mô hình ........................................................................ 4 2.2. Thực thi tƣợng trƣng ............................................................................. 8 2.2.1. Tổng quan về thực thi tượng trưng .................................................... 9 2.2.2. Kỹ thuật thực thi tượng trưng động ................................................. 13 2.2.3 Thực thi tƣợng trƣng động và giải pháp .......................................... 17 Chƣơng 3. SATISFIABILITY MODULO THEORIES (SMT) ................... 20 3.1 SAT solver ............................................................................................ 20 3.1.1 Bài toán SAT ................................................................................... 20 3.1.2 Thuật toán DPLL cho SAT .............................................................. 21 3.2 SMT solver ............................................................................................ 26 3.3.1 Bài toán của SMT ............................................................................ 26 3.3.2 Thuật toán DPLL cho SMT ............................................................ 28 3.2.3 SMT solver Boolector, Z3, và STP .................................................. 29 Chƣơng 4. KIỂM CHỨNG DỰA TRÊN KLEE ........................................... 39 4.1. Giới thiệu về khung làm việc của KLEE ............................................ 39 4.1.1. Đầu vào của KLEE ......................................................................... 41 iv 4.4.2. Tối ưu hóa tập các ràng buộc với KLEE ......................................... 42 4.1.3. Giải ràng buộc tự động với metaSMT ............................................. 45 4.2. Độ bao phủ mã nguồn của ca kiểm thử đƣợc sinh bởi KLEE ........... 49 4.3. Thực thi tƣơng trƣng động với KLEE................................................ 55 4.4. Thực thi tƣợng trƣng động và giải pháp của KLEE .......................... 56 4.5. Một số bài toán kiểm chứng và kiểm thử tự động dựa trên KLEE .. 57 4.3.1. Kiểm tra lỗi chia cho 0 trong chương trình ..................................... 57 4.3.2. Phát hiện lỗi truy cập ra ngoài kích thước của mảng ....................... 59 4.3.3. Phát hiện lỗi hàm khi đột ngột gọi hàm abort ................................. 62 4.3.4. Sinh dữ liệu kiểm thử tự động ......................................................... 63 KẾT LUẬN ..................................................................................................... 69 v BẢNG CÁC THUẬT NGỮ VIẾT TẮT Thuật ngữ viết tắt Thuật ngữ đầy đủ 1. DPLL Davis Putnam Logemann Loveland 2. EGT Execution Generated Testing 3. SAT Satisfiability 4. SMT Satisfiability Modulo Theories 5. AOT A head Of Time 6. JIT Just In Time 7. API Application Programing Interface 8. CNF Conjunctive Normal Form 9. FIFO First In First Out 10. DAG Directed Acyclic Graph 11. CI Constraint Independence 12. CEC Counter Example Cache 13. BC Branch Cache 14 PC Path Condition 15 GCC GNU Compiler Collection 16 SE Symbolic Execution 17 GPU Graphics Processing Unit STT vi DANH MỤC HÌNH VẼ Hình 2.1. Sơ đồ của hệ thống kiểm chứng [3] ......................................................................... 4 Hình 2.2. Mô hình hóa cách tiếp cận của kiểm chứng mô hình [3] .......................................... 6 Hình 2.3. Một đoạn mã nguồn C++ và thực thi tượng trưng tương ứng ................................ 10 Hình 2.4. Một đoạn mã nguồn chứa vòng lặp ....................................................................... 12 Hình 2.5 Công thức biểu diễn thực thi tượng trưng cho vòng lặp [5] .................................... 12 Hình 2.6 Đoạn mã nguồn C chứa biểu thức không tuyến tính ............................................... 13 Hình 2.6 Đoạn mã nguồn C kết hợp đầu vào cụ thể và tượng trưng ...................................... 14 Hình 3.1.a Hình vẽ mô tả thủ tục DPLL ............................................................................... 23 Hình 3.1.b. Sơ đồ cơ chế hoạt động của thủ tục DPLL cho SAT [6] ..................................... 23 Hình 3.2. Sơ đồ tổng quan của Boolector [21] ...................................................................... 30 Hình 3.3 Sơ đồ tổng quan của Z3 [15] .................................................................................. 33 Hình 3.4 Sơ đồ kiến trúc của STP solver [26] ....................................................................... 36 Hình 4.1 Kiến trúc tổng quan của KLEE .............................................................................. 40 Hình 4.2 Kiến trúc của metaSMT [10] ................................................................................. 46 Hình 4.3. Biểu thức đầu vào dạng đồ thị [8] ......................................................................... 48 Hình 4.4. Mô hình quá trình giải ràng buộc của metaSMT [10] ............................................ 49 Hình 4.6 là đồ thị luồng điều khiển của chương trình trên. ................................................... 50 Hình 4.5. Ví dụ về mã nguồn hàm ReturnAverage ............................................................... 50 Hình 4.6 Đồ thị luồng điều khiển của hàm ReturnAverager [14] .......................................... 51 Hình 4.7. Minh họa việc loại đường thực thi dư thừa ............................................................ 53 Hình 4.3.1.a. Hàm phát sinh lỗi chia cho 0 .......................................................................... 57 Hình 4.3.1.b. Gọi tượng trưng trong KLEE cho hàm có lỗi chia cho 0 .................................. 58 Hình 4.3.1.c. Cây thực thi tượng trưng chương trình phát hiện lỗi chia cho 0 ....................... 58 Hình 4.3.1.d Mô hình quá trình giải các ràng buộc của các solver ........................................ 59 Hình 4.3.2.a Hàm phát sinh lỗi cập ngoài kích thước của mảng. .......................................... 60 Hình 4.3.2.b Quá trình thực thi tượng trưng của chương trình phát hiện lỗi truy cập ngoài kích thước của mảng. ................................................................................................................... 60 Hình 4.3.2.c. Cây thực thi tượng trưng của chương trình phát hiện lỗi truy cập ngoài kích thước của mảng. ................................................................................................................... 61 Hình 4.3.2.d. Cây thực thi tượng trưng của chương trình phát hiện lỗi truy cập ngoài kích thước của mảng .................................................................................................................... 62 Hình 4.3.3.a Đoạn mã nguồn có gọi hàm abort() .................................................................. 62 vii Hình 4.3.3.b. Cây thực thi tượng trưng phát hiện lỗi hàm abort() .......................................... 63 Hình 4.3.4.a Đoạn mã nguồn so sánh hai chuỗi .................................................................... 64 Hình 4.3.4.b Thực hiện tượng trưng hóa cho hàm so sánh chuỗi........................................... 64 Hình 4.3.4.c. Cây thực thi tượng trưng kiểm thử hàm so sánh chuỗi ..................................... 65 Hình 4.3.4.d. Mô hình quá trình giải các ràng buộc của các solver ....................................... 67 1 Chƣơng 1. GIỚI THIỆU 1.1. Đảm bảo chất lƣợng phần mềm Máy tính và phần mềm máy tính ngày càng đóng vai trò to lớn trong nhiều lĩnh vực của đời sống xã hội như: kinh tế, giao thông, vũ trụ hay các dịch vụ y tế trong khám chữa bệnh… Thông thường các phần mềm máy tính không đứng riêng lẻ mà chúng được tích hợp hoặc nhúng trong các hệ thống phức tạp. Cho nên, việc đảm bảo chất lượng phần mềm là hết sức cần thiết. Việc đảm bảo chất lượng phần mềm trong các lĩnh vực như dịch vụ y tế hay vũ trụ hàng không lại càng được coi trọng. Bởi chỉ một sai sót nhỏ của hệ thống có thể gây ra những tổn thất to lớn về tính mạng con người cũng như về kinh tế. Trong những năm gần đây, chúng ta cũng đã chứng kiến nhiều thảm họa xảy ra mà nguyên nhân lại nằm ở lỗi phần mềm chẳng hạn ngày 04/06/1996 tàu vũ trụ Ariane -5 đã nổ tung chỉ 36 giây sau khi khởi động [3]. Nguyên nhân là do lỗi chuyển đổi một số dạng dấu phẩy động 64 - bit thành số nguyên dương 16-bit. Sự việc này xảy ra đã lâu, nhưng cho đến nay nó vẫn được nhắc đến như một thảm họa khủng khiếp nhất do lỗi phần mềm gây ra. Rất nhiều kỹ thuật được nghiên cứu và sử dụng để khẳng định tính đúng đắn của hệ thống. Hai kỹ thuật truyền thống đã và đang được sử dụng để đảm bảo chất lượng phần mềm là kiểm thử phần mềm và kiểm chứng phần mềm (Software verification). Tuy nhiên, việc sử dụng các phương pháp kiểm thử chỉ làm giảm bớt lỗi của hệ thống mà không thể chứng minh được hệ thống không có lỗi. Các phương pháp kiểm chứng đang được quan tâm số một trong việc chứng minh tính đúng đắn của hệ thống. Phương pháp kiểm chứng mô hình (model checking) là sự lựa chọn hiệu quả trong việc chỉ ra hệ thống hoạt động đúng. Nhưng phương pháp này lại gặp phải vấn đề bùng nổ trạng thái khi thực hiện với các hệ thống lớn, phức tạp trong thực tế. 2 Luận văn trình bày phương pháp kiểm chứng dựa trên SMT (SAT Modulo Theories) sử dụng thực thi tượng trưng (symbolic execution) là phương pháp khác thay thế cho phương pháp kiểm chứng mô hình khi thực hiện với các hệ thống phức tạp. 1.2. Mục tiêu của luận văn Mục tiêu của luận văn là tìm hiểu và trình bày về phương pháp kiểm chứng dựa trên SMT. Một phương pháp có nhiều ưu điểm cho vấn đề bùng nổ trạng thái của kiểm chứng mô hình. Luận văn sẽ trình bày về công cụ KLEE, một công cụ kiểm chứng tự động sử dụng thực thi tượng trưng kết hợp với ba SMT solver được đánh giá là hiệu quả đó là Z3, Boolector và STP. Tiếp theo luận văn sẽ trình bày về ứng dụng của KLEE trong kiểm chứng một số thuộc tính của chương trình như phát hiện lỗi chia cho 0, lỗi tràn vùng đệm, lỗi truy cập ra ngoài kích thước của mảng, … 1.3. Nội dung luận văn Luận văn gồm 4 chương, trong đó phần giới thiệu được trình bày trong 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. 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. 2.1. 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. 2.1.1. 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 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.1. Đặc tả (System Specification) Các thuộc tính (Properties) Quy trình thiết kế (Design Process) Sản phẩm hoặc bản thử (product of prototype) Kiểm chứng (Verification) Phát hiện lỗi (bug (s) found) Không tìm thấy lỗi (no bugs found) Hình 2.1. Sơ đồ của hệ thống kiểm chứng [3] 2.1.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 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 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.2. Đặc tả (requirements) Hệ thống (System) (Hình thức hóa) Formalizing Mô hình hóa (Modeling) Đặc tả thuộc tính (Property Specification) Mô hình hóa hệ thống (System model) Kiểm chứng mô hình (Model Checking) Thỏa mãn (Satisfied) Vi phạm + phản ví dụ (Violated + counterexample ) Mô phỏng (Simulation) Lỗi cụ thể (local error) Hình 2.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: 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 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. 2.2. Thực thi tƣợng trƣng Trong phần này luận văn trình bày các vấn đề của thực thi tượng trưng, thực thi tượng trưng động cùng một số giải pháp để giải quyết các vấn đề của thực thi tượng trưng động. 9 2.2.1. Tổng quan về thực thi tƣợng trƣng Trong những năm gần đây, vấn đề thực thi tượng trưng [5] (Symbolic execution) cho kiểm chứng phần mềm rất được quan tâm, do khả năng sinh ra các ca kiểm thử có độ phủ cao và tìm lỗi sâu trong các ứng dụng phức tạp. Thực thi tượng trưng là phương pháp chạy chương trình máy tính bằng cách sử dụng các biến tượng trưng. Thay vì thực thi chương trình với đầu vào cụ thể. Chương trình được thực thi tượng trưng tương ứng một tập các giá trị đầu vào (input). Kiểm chứng mô hình và kiểm thử là hai kỹ thuật phổ biến thường được sử dụng để đảm bảo tính đúng đắn của hành vi chương trình. Các phương pháp kiểm thử chỉ khẳng định được chương trình tốt đối với các ca kiểm thử (test case) cụ thể. Kiểm chứng mô hình cung cấp một giải pháp toàn diện hơn để xác định độ tin cậy của chương trình. Tuy nhiên, nhược điểm của phương pháp này là bùng nổ không gian trạng thái. Thực thi tượng trưng cung cấp một cách để làm giảm bớt vấn đề bùng nổ trạng thái. Bằng cách thực thi với đầu vào tượng trưng thay vì vét cạn các giá trị cụ thể của đầu vào. Trong kiểm chứng, thực thi tượng trưng được sử dụng để sinh ra giá trị đầu vào kiểm thử (test input) cho mỗi đường thực thi (execution path) của chương trình. Một đường thực thi là một chuỗi các giá trị đúng (true) hoặc sai (false) tương ứng. Trong đó, một giá trị là đúng ở vị trí thứ i nghĩa là tại vị trí thứ i điều kiện nhận giá trị đúng và đi theo hướng đúng. Hoặc ngược lại đi theo hướng sai. Tập hợp các đường thực thi của một chương trình tạo thành cây thực thi. Mục đích của thực thi tượng trưng là sinh ra tất cả các đầu vào có thể có cho toàn bộ các đường thực thi. Xét ví dụ hình 2.3 (đoạn mã nguồn chứa câu lệnh điều điều kiện) để thấy được cách thức thực hiện của thực thi tượng trưng. 10 1. int twice ( int v) { 2 . return 2∗v; 3. } 4. void testme ( int x, int y) { 2*y = x 6. z = twice (y); False True 7 . if (z = x) { 8 . if (x > y+10) 9 . ERROR;// giả sử một lệnh phát sinh lỗi ở đây 10 x=0 y =1 x > y+10 } True False 11 } 12 } 13. int main() { 14 . x = sym input(); x=2 y=1 x = 30 y = 15 ERROR 15 . y = sym input(); 16 . testme(x, y); 17 . return 0; } Hình 2.3. Một đoạn mã nguồn C++ và thực thi tượng trưng tương ứng Thực thi tƣợng trƣng với câu lệnh điều kiện (if): Xét đoạn mã nguồn chứa câu lệnh điều kiện hình 2.3, quá trình thực thi tượng trưng được thực hiện qua các bước sau:  Tạo đầu vào tượng trưng cho các biến x và y bằng 2 lệnh tại dòng 14, 15 của đoạn mã hình 2.3. Sau hai câu lệnh này một ánh xạ vào hàm trạng thái tượng trưng φ được bổ sung. Kết quả của hàm φ là φ = {x x0, y y0}.  Thực hiện câu lệnh gọi hàm ở dòng 16. Tiếp theo, thực hiện câu lệnh gán ở dòng 6 được thực hiện. Sau lệnh này kết quả của hàm φ trở thành φ = {x x0, y y0, z 2y0}.  Thực hiện câu lệnh điều kiện ở dòng 7. Lúc này xuất hiện đường điều kiện rẽ nhánh (path condition), tùy thuộc vào giá trị của biểu thức điều kiện sẽ 11 quyết định chương trình thực thi theo nhánh đúng hay nhánh sai. Từ đó, hình thành 2 tập hợp chứa các điều kiện rẽ nhánh khác nhau kí hiệu là PC và PC’. Sau dòng 7 tập PC1=(x0 = 2y0) và PC2 = (x0 = 2y0).  Thực hiện câu lệnh điều kiện tại dòng 8. Thực hiện tương tự câu lệnh điều kiện ở dòng 7 ta được 3 tập điều kiện rẽ nhánh PC2 = (x0 = 2y0), PC1= ((x0 = 2y0)˄ (x0 > y0 + 10)) và PC1’= ((x0 = 2y0) ˄ (x0  y0 + 10)).  Giả sử một lỗi được phát sinh ở câu lệnh tại dòng 9. Lỗi ở đây có thể là chương trình bị treo hoặc vi phạm một hàm đánh giá (assert). Trường hợp này xuất hiện một phản ví dụ (counter example). Một phép gán được chỉ ra để chương trình thực thi theo nhánh này. Kết thúc câu lệnh ở dòng 9 cả 3 nhánh của chương trình đều đã được duyệt với 3 tập ràng buộc sau: PC2 = (x0 = 2y0) PC1=((x0 = 2y0)˄(x0 > y0 + 10)) PC1’=((x0 = 2y0)˄(x0  y0 + 10)).  SMT solver sẽ giải lần lượt từng tập ràng buộc này để sinh ra các test case tương ứng. Giả sử kết quả được giải bởi SMT solver lần lượt là {x = 0, y = 1}, {x = 2, y = 1} và {x = 30, y = 15}. Trong kiểm chứng tự động nếu áp dụng kỹ thuật sinh đầu vào ngẫu nhiên thì khi áp dụng với chương trình có chứa vòng lặp có thể sẽ gặp phải vấn đề thực hiện vô hạn. Nhưng trong thực thi tượng trưng vấn đề này sẽ được giải quyết. Phần tiếp theo luận văn sẽ trình bày về thực thi tượng trưng cho chương trình chứa vòng lặp. Thực thi tƣợng trƣng cho chƣơng trình chứa vòng lặp: Xét một ví dụ khác trong hình 2.4 để hiểu rõ hơn quá trình thực hiện của kỹ thuật thực thi tượng trưng, gồm các bước sau:  Thực thi tượng trưng với thuộc tính đầu vào nằm trong điều kiện vòng lặp. Xét câu lệnh lặp while (N > 0) ở dòng 4 hình 2.4 ta thấy điều kiện kết thúc vòng lặp này phụ thuộc vào giá trị của biến N. Mà biến N lại là đầu vào tượng trưng. Cho nên, chương trình có thể sẽ sinh ra một lượng vô hạn các