- TRƯỜNG ĐẠI HỌC KHOA HỌC TỰ NHIÊN. - NGHIÊN CỨU. - KỸ THUẬT GIẢI THÍCH TRỪU TƯỢNG. - Tôi xin cam đoan đây là công trình nghiên cứu của tôi trong đó có sự giúp đỡ của giáo viên hướng dẫn TS. - Các nội dung và kết quả nghiên cứu trong luận văn này là hoàn toàn trung thực, được tham khảo theo các tài liệu của các tác giả do giáo viên hướng dẫn cung cấp và được liệt kê tại mục tài liệu tham khảo.. - Cuối cùng tôi xin gửi lời cảm ơn tới các thành viên trong gia đình đã tạo điều kiện tốt nhất cho tôi, động viên, cổ vũ tôi trong quá trình học tập và nghiên cứu để tôi hoàn thành luận văn này.. - Tổng quan về phân tích chương trình. - Ý tưởng của bài toán phân tích chương trình. - Phân tích chương trình tĩnh. - Tổng quan về kỹ thuật giải thích trừu tượng. - Tổng quan về tình hình nghiên cứu. - Chương 2 - CỞ SỞ LÝ THUYẾT CỦA KỸ THUẬT GIẢI THÍCH TRỪU TƯỢNG. - Khái niệm về kỹ thuật giải thích trừu tượng. - Ứng dụng của kỹ thuật giải thích trừu tượng. - Ngữ nghĩa cụ thể của chương trình. - Thuộc tính an toàn của chương trình. - Miền trừu tượng. - Độ phủ của kỹ thuật giải thích trừu tượng. - Tính chất cần thiết của ngữ nghĩa trừu tượng. - Lý thuyết điểm cố định. - Điểm cố định. - Mở rộng ký hiệu điểm cố định. - Phân tích luồng dữ liệu (Data Flow Analysis. - Thuật toán tìm điểm cố định. - Tiếp cận kết nối Galois cho kỹ thuật giải thích trừu tượng. - Trừu tượng hàm (Functional Abstraction. - Trừu tượng hóa ngữ nghĩa chương trình. - Ngữ nghĩa vết (Trace semantics. - Biểu diễn ngữ nghĩa vết dưới dạng điểm cố định. - Bao đóng phản xạ bắc cầu (RTC - reflexive transitive closure) là trừu tượng hóa của ngữ nghĩa vết. - Biểu diễn ngữ nghĩa RTC dưới dạng điểm cố định. - Ngữ nghĩa tới được là trừu tượng hoá của ngữ nghĩa RTC. - Biểu diễn ngữ nghĩa tới được dưới dạng điểm cố định. - Phân tích trong TVLA. - Cấu trúc 3-valued Logic. - Biểu diễn trạng thái bộ nhớ Heap qua cấu trúc Logic. - Trừu tượng heap. - Biểu diễn ngữ nghĩa và chương trình. - Ví dụ về phân tích chương trình. - Thuật toán sinh hệ ràng buộc Coerce và thuật toán giải hệ ràng buộc tìm điểm cố định Focus. - Ngữ nghĩa. - Đặc tả hệ thống trong TVLA. - Kết quả phân tích. - 1 Abstract domain Miền trừu tượng. - 2 Abstract semantics Ngữ nghĩa trừu tượng. - 4 Concrete semantics Ngữ nghĩa cụ thể. - 6 Control Flow Graphs - CFG Đồ thị luồng điều khiển 7 Data Flow Analysis - DFA Phân tích luồng dữ liệu. - 8 Fixpoint - fix Điểm cố định. - 9 Fixpoint approximation Xấp xỉ điểm cố định. - 11 Interval semantics Ngữ nghĩa khoảng. - 17 Reachability semantics Ngữ nghĩa tới được. - Ngữ nghĩa bao đóng phản xạ bắc cầu. - Ngữ nghĩa vết, Tập hợp các dấu vết về quá trình chuyển đổi trạng thái của chương trình.. - 1 Hình 1.1: Bài toán phân tích chương trình tổng quát 12. - 2 Hình 1.2: Trừu tượng hóa theo điểm cố định 14. - 3 Hình 1.3: Các thành phần chính của phân tích chương trình 14 4 Hình 2.1 Sơ đồ hành vi có thể của chương trình 18. - 5 Hình 2.2: Quĩ đạo an toàn của các thực thi 19. - 6 Hình 2.3: Quĩ đạo không an toàn đối với kiểm thử/gỡ lỗi 20. - 7 Hình 2.4: Biểu diễn miền trừu tượng 21. - 8 Hình 2.5: Trừu tượng hóa quĩ đạo hành vi của chương trình 22 9 Hình 2.6: Trừu tượng hóa quĩ đạo hành vi không đảm bảo tính đủ 24 10 Hình 2.7: Lỗi trừu tượng hóa quĩ đạo hành vi không chính xác 24 11 Hình 2.8: Tiêu chuẩn trừu tượng hóa theo khoảng 25. - 12 Hình 2.9: Biểu đồ Hasse của dàn (2 A. - 13 Hình 2.10: Biểu diễn ngữ nghĩa của một chương trình thành dàn 28 14 Hình 2.11: Biểu diễn điểm cố định của hàm cosx = x 30. - 15 Hình 2.12: Tính toán điểm cố định trên dàn 30. - 16 Hình 2.13: Phép cộng dàn 32. - 17 Hình 2.14: Phép nâng dàn 31. - 18 Hình 2.15: Dàn phẳng 32. - 19 Hình 2.16: CFG cho các lệnh đơn giản 34. - 20 Hình 2.17: CFG cho cấu trúc tuần tự 34. - 21 Hình 2.18: CFG cho cấu trúc rẽ nhánh 34. - 22 Hình 2.19: CFG cho cấu trúc lặp 35. - 23 Hình 2.20: CFG của hàm tính n! 35. - 24 Hình 2.21: ¯F(¯x) là một xấp xỉ của F(x) 41. - 25 Hình 2.22: Biểu diễn quan hệ chuyển tiếp ngữ nghĩa chương trình 42 26 Hình 2.23: Hệ chuyển dịch quĩ đạo thực thực thi của chương trình 42. - 27 Hình 2.24: Biểu diễn ngữ nghĩa vết thực thi 43. - 28 Hình 2.25: Biểu diễn ngữ nghĩa vết dưới dạng điểm cố định 44 29 Hình 2.26: Trừu tượng hóa đến ngữ nghĩa tới được 48 30 Hình 3.1: Các toán tử 3-valued logic của Kleene 52. - 31 Hình 3.2: Biểu diễn heap cụ thể 53. - 32 Hình 3.3: Trừu tượng hóa heap 55. - 33 Hình 3.4: Kết quả heap trừu tượng đầu ra 56. - 34 Hình 3.5: Trạng thái của chương trình sử dụng cấu trúc 2-valued logic 58 35 Hình 3.6: Trạng thái của chương trình sử dụng 3-valued logic 58 36 Hình 3.7: Biểu diễn quá trình làm việc của phân tích chương trình 59 37 Hình 3.8: Ứng dụng của giải thích trừu tượng cho phân tích lệnh 62 38 Hình 3.9: Kết quả phân tích hàm tạo danh sách liên kết 77. - Ngày nay, các hệ thống phần mềm được sử dụng một cách phổ biến trên tất cả các lĩnh vực của đời sống, trong sản xuất, kinh doanh như: kinh tế, tài chính, kế toán, y tế, giáo dục, chính phủ. - Đối với những đơn vị, cá nhân và các tổ chức làm phần mềm chuyên nghiệp họ đều hiểu rằng một sản phẩm phần mềm được họ tạo ra không thể nào chạy một cách hoàn hảo ngay từ lúc đầu tiên mà không mắc bất kỳ một lỗi gì. - Trong quá trình phát triển và đưa vào sử dụng một phần mềm bất kỳ, thì hầu hết tất cả các lỗi chỉ được phát hiện sau khi phần mềm đó được đưa vào sử dụng. - Do vậy, các hoạt động kiểm thử đóng góp một vai trò rất quan trọng nhằm đảm bảo chất lượng của các hệ thống phần mềm.. - Các hoạt động kiểm thử này luôn được các nhà phát triển phần mềm tính đến trong suốt quá trình phát triển cho một hệ thống phần mềm. - Hầu hết các hoạt động kiểm thử nhằm mục đích phân tích các thành phần và cấu trúc của phần mềm để xác định số lượng lớn nhất các lỗi trong tiến trình phát triển: từ đặc tả cho đến mã hóa.. - Đối với các hệ thống phần mềm phức tạp, cách giải quyết đưa ra ban đầu với các hệ thống bao giờ cũng là cẩn thận trong từng khâu: phân tích, thiết kế, lập trình, kiểm thử để giảm thiểu một cách tối đa các lỗi phát sinh.. - Vì vậy, việc nghiên cứu các phương pháp nhằm mục đích giảm chi phí trong quá trình kiểm thử đã được đưa ra, nhưng vẫn đảm bảo mục tiêu về tính hiệu quả của phần mềm là một biện pháp hữu hiệu.. - Do vậy, trong luận văn này tôi giới thiệu một phương pháp trong lĩnh vực phân tích chương trình tĩnh. - Cụ thể là nghiên cứu về kỹ thuật giải thích trừu tượng, mục tiêu chính là cập nhật các xu hướng mới của kỹ thuật này ở trên thế giới để nâng cao chất lượng phần mềm.. - Các đề tài nghiên cứu về kỹ thuật giải thích trừu tượng chưa được phổ biến ở trong nước, do vậy trong khuôn khổ của đề tài tôi xin trình bày các khái niệm cơ bản, cơ sở lý thuyết ban đầu dựa trên các báo cáo tại các hội nghị thường niên VMCAI (Verification, Model Checking, and Abstract Interpretation) và các tài liệu nghiên cứu, bài giảng của tác giả Patrick Cousot trong những năm gần đây.. - Chương 1 - TỔNG QUAN: Tập trung vào các khái niệm liên quan đến kiểm chứng phần mềm, phân tích chương trình tĩnh, tiếp cận lý thuyết của kỹ thuật giải thích trừu tượng trong phân tích chương trình tĩnh, tình hình nghiên cứu ở trong và ngoài nước.. - Chương 2 - CƠ SỞ LÝ THUYẾT CỦA KỸ THUẬT GIẢI THÍCH TRỪU TƯỢNG: Tập trung vào cơ sở lý thuyết toán học của kỹ thuật giải thích trừu tượng, các phương pháp trừu tượng hóa ngữ nghĩa chương trình, biểu diễn ngữ nghĩa của chương trình thông qua các kỹ thuật trừu tượng. - và ứng dụng trong kỹ thuật giải thích trừu tượng.. - Chương 3 - THỬ NGHIỆM: Tập trung vào việc cài đặt phương pháp phân tích chương trình tĩnh bằng kỹ thuật giải thích trừu tượng dựa trên bộ công cụ mã nguồn mở TVLA, làm rõ các ứng dụng trong phân tích hình dạng.. - KẾT LUẬN: Trình bày nội dung nghiên cứu đã đạt được, các hạn chế trong quá trình nghiên cứu và định hướng nghiên cứ tiếp theo.. - [7] Patrick Cousot. - [8] Patrick Cousot. - Abstract Interpretation. - [9] Patrick Cousot. - [10] Patrick Cousot