chương 1 luận văn đã trình bày tổng quan về phân tích chương trình, các ý tưởng chính cần thiết cho việc nghiên cứu kỹ thuật giải thích trừu tượng và vai trò của kỹ thuật này trong phân tích chương trình tĩnh. Khảo sát tình hình nghiên cứu ở trong và ngoài nước, các xu hướng đang được ứng dụng của kỹ thuật này trong việc nâng cao chất lượng phần mềm. Về cơ sở lý thuyết nền tảng của kỹ thuật này như: ngữ nghĩa chương trình, ngữ nghĩa vết, các phương thức trừu tượng, biểu diễn trừu tượng của các ngữ nghĩa, …, sẽ được nghiên cứu sâu trong chương 2. 16 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Chương 2 - CỞ SỞ LÝ THUYẾT CỦA KỸ THUẬT GIẢI THÍCH TRỪU TƯỢNG 2.
Khái niệm về kỹ thuật giải thích trừu tượng Kỹ thuật giải thích trừu tượng (Abstract interpretation): Là một kỹ thuật trong phân tích chương trình, kỹ thuật này giúp giải thích về ngữ nghĩa của một chương trình với những hàm đơn điệu trên các tập hợp đã được xếp thứ tự. Lý thuyết giải thích trừu tượng nghiên cứu về ngữ nghĩa của chương trình, phương pháp trừu tượng hóa ngữ nghĩa của chương trình, và tính đủ (sound) cũng như tính chính xác (precise) của phương pháp xấp xỉ để tạo ra ngữ nghĩa trừu tượng. Kỹ thuật giải thích trừu tượng được hiểu theo nghĩa trực giác là việc thực thi một phần của một chương trình để lấy thông tin về nó: sơ đồ luồng điều khiển, sơ đồ luồng dữ liệu, … [8]. + Hình thức hóa: Tất cả những gì đã được chuẩn tắc hóa và được chứng minh chặt chẽ bằng toán học.
+ Phi hình thức hóa: dựa kinh nghiệm, thử nghiệm, mà không thể chứng minh được bằng toán học. Ứng dụng của kỹ thuật giải thích trừu tượng: Phân tích trừu tượng được ứng dụng trong phân tích cú pháp, trình biên dịch, gỡ lỗi chương trình. Ứng dụng của kỹ thuật giải thích trừu tượng Kỹ thuật giải thích trừu tượng được ứng dụng rộng rãi và là một phần không thể thiếu trong lĩnh vực kiểm thử phần mềm. Kỹ thuật giải thích trừu tượng được dùng để chứng minh tính đầy đủ, tính chính xác, tính đúng đắn cục bộ, tính đúng đắn toàn cục của hệ thống.
Một số ứng dụng của giải thích trừu tượng như [8]: + Phân tích cú pháp của dòng lệnh: phân tích thuộc tính và cú pháp của các dòng lệnh bằng việc giải thích trừu tượng các thuộc tính và cú pháp. 17 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com + Phân tích tĩnh chương trình: đây là lĩnh vực được ứng dụng nhiều nhất của giải thích trừu tượng. Phương pháp này phân tích mã nguồn của chương trình bằng cách trừu tượng hóa các thực thi của chương trình đó. Từ đó chứng minh tính đủ, tính đúng đắn, tính chính xác của chương trình.
+ Ẩn thông tin: trong các ngôn ngữ dựa trên các phần mềm bảo mật, các thông tin được ẩn đi để tránh sự theo dõi, phát hiện bằng cách sử dụng việc trừu tượng hóa các thông tin của chương trình đó. + Ngoài ra giải thích trừu tượng còn nhiều ứng dụng quan trọng khác trong các ngành công nghiệp như xe hơi, hàng không, vũ trụ,. Một số khái niệm cơ bản 2. Ngữ nghĩa cụ thể của chương trình Ngữ nghĩa cụ thể của một chương trình được hình thức hóa (là một mô hình toán học của) mô tả tất cả các hành vi (quĩ đạo các đường thực thi) có thể của chương trình thực hiện trong tất cả các môi trường phù hợp, các thực thi có thể của chương trình được thể hiện trong hình 2.1 Sơ đồ hành vi có thể của chương trình.
Ngữ nghĩa cụ thể của chương trình là vô hạn (tức là có vô số các đường thực thi như hình trên) các đối tượng toán học, do đó không thể thực hiện các tính toán trên miền ngữ nghĩa cụ thể của một chương trình. Tất cả các câu hỏi 18 LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Thuộc tính an toàn của chương trình Thuộc tính an toàn (Safety properties) của một chương trình là việc không xuất hiện lỗi khi thực hiện các thực thi của chương trình đó trong bất kỳ một môi trường nào. Các hành vi của chương trình không vượt quá phạm vi của môi trường cho phép minh họa trong hình 2.2: Quĩ đạo an toàn của các thực thi Trong hình 2.2 biểu diễn về tính an toàn của chương trình.
Bằng chứng cho tính an toàn bao gồm chứng minh rằng giao giữa miền ngữ nghĩa cụ thể của chương trình và vùng cấm (forbidden zone) là tập rỗng. Mặt khác, ngữ nghĩa cụ thể của chương trình là vô hạn, đây chính là vấn đề không giải quyết được (ngữ nghĩa cụ thể là không tính toán được). Lý do này dẫn đến không thể xác minh hoàn toàn tự động tính an toàn của chương trình với nguồn tài nguyên phần cứng máy tính là hữu hạn hoặc không có sự tương tác của con người. Trong khi đó các phương pháp kiểm thử phổ biến hiện nay như kiểm thử và gỡ lỗi (Testing/Debugging) chỉ xem xét một tập con của tập tất cả các hành vi có thể của chương trình, vì vậy kỹ thuật này không phải là một chứng minh tối ưu cho tính đúng đắn của chương trình.
Độ phủ hạn chế là vấn đề 19 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com chính của các kỹ thuật dạng này. Tức là một chương trình sẽ xuất hiện lỗi nếu các hành vi của nó vượt quá giới hạn cho phép của chương trình, có nghĩa là giao của quỹ đạo các hành vi với vùng cấm là khác rỗng [3].3: Quĩ đạo không an toàn đối với kiểm thử/gỡ lỗi Trong hình 2.3 biểu diễn cơ chế của kỹ thuật kiểm thử/gỡ lỗi, chỉ một số thực thi (đường nét liền) của chương trình được kiểm thử, các thực thi còn lại (nét đứt) thì không được kiểm tra và các lỗi của chương trình được mô tả trong hình là vi phạm vào vùng cấm (có thể xảy ra). Miền trừu tượng Miền trừu tượng là một đại số trừu tượng, được biểu diễn dưới dạng một thư viện các modul, cung cấp các mô tả về tính chất trừu tượng, các toán tử và các lệnh của chương trình trên các tập thuộc tích trừu tượng của chương trình đó (ví dụ như thuộc tính trừu tượng các chuyển dịch biểu diễn hiệu quả các toán tử của các lệnh chương trình và các lệnh trừu tượng, …). Miền trừu tượng thường là một dàn đầy đủ, là sự trừu tượng hóa của tập lũy thừa [8].
Có hai loại miền trừu tượng hữu hạn và vô hạn. Miền trừu tượng hữu hạn được sử dụng như là một thư viện đầy đủ cung cấp các mô tả về tính chất trừu tượng của một ngôn ngữ. Miền trừu tượng vô hạn về cơ bản giống như miền trừu tượng hữu hạn, nó khác miền trừu tượng hữu hạn ở chỗ nó có thể cung cấp các mô tả về tính chất trừu tượng của các đối tượng vô hạn [3]. 20 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Ví dụ về miền trừu tượng Trừu tượng hóa theo khoảng (không liên kết): ⟹ [ , ], ⟹ [ ′, ′],.
Trừu tượng hóa theo đa diện (có liên kết): + − 2 ≤ 10,. Trừu tượng hóa chênh lệch-ràng buộc (liên kết mạnh): − ≤ 5, − ≤ 10, .4: Biểu diễn miền trừu tượng 2. Độ phủ của kỹ thuật giải thích trừu tượng Do quá trình phân tích của kỹ thuật giải thích trừu tượng và nó được xem xét trên ngữ nghĩa trừu tượng của chương trình. Có thể nói rằng ngữ nghĩa trừu tượng được xem xét là tập cha của tập ngữ nghĩa cụ thể của chương trình, do đó các ngữ nghĩa trừu tượng bao gồm tất cả các trường hợp có thể [3].
Mục đích chính của kỹ thuật giải thích trừu tượng chuyển chứng minh bài toán phân tích chương trình về dạng: nếu ngữ nghĩa trừu tượng của thỏa mãn đặc tả (tập các quĩ đạo hành vi có thể của chương trình giao với vùng vi phạm là tập rỗng) thì ngữ nghĩa cụ thể của cũng thỏa mãn đặc tả.5 biểu diễn cơ chế trừu tượng hóa ngữ nghĩa cụ thể của giải thích trừu tượng. Từ miền ngữ nghĩa cụ thể của chương trình được trừu tượng hóa thành miền ngữ nghĩa trừu tượng (màu xanh) bao trọn toàn bộ quĩ đạo hành vi có thể của 21 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com chương trình. Khi đó, nếu miền ngữ nghĩa trừu tượng thỏa mãn đặc tả thì miền ngữ nghĩa cụ thể cũng thỏa mãn đặc tả [3].5: Trừu tượng hóa quĩ đạo hành vi của chương trình 2. Các phương pháp hình thức Các phương pháp hình thức chính là giải thích trừu tượng, trong đó có sự khác biệt theo nhiều cách khác nhau để có được ngữ nghĩa trừu tượng từ ngữ nghĩa cụ thể của chương trình.
Kiểm chứng mô hình (Model checking) + Ngữ nghĩa trừu tượng của chương trình được đưa ra thủ công (bằng tay) bởi người sử dùng; + Được biểu diễn dưới hình thức của một mô hình hữu hạn của các thực thi chương trình; + Ngữ nghĩa trừu tượng có thể được tính toán tự động bằng các kỹ thuật có liên quan tới phân tích tĩnh. Phương pháp suy diễn (Deductive methods) + Ngữ nghĩa trừu tượng được xác định bởi các điều kiện kiểm chứng (verification conditions); + Người sử dùng phải cung cấp các ngữ nghĩa trừu tượng theo hình thức lập luận qui nạp (ví dụ như bất biến); 22 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com + Ngữ nghĩa trừu tượng có thể được tính toán tự động bằng các kỹ thuật có liên quan tới phân tích tĩnh. Phân tích tĩnh (Static Analysis): Ngữ nghĩa trừu tượng được tính toán tự động từ mã nguồn chương trình theo quy định các khái niệm trừu tượng định nghĩa trước (mà đôi khi có thể được thay đổi tự động/bằng tay bởi người sử dụng) [3]. Tính chất cần thiết của ngữ nghĩa trừu tượng Để đảm bảo tính chính xác của kết quả phân tích, miền ngữ nghĩa trừu tượng phải thỏa mãn một số thuộc tính cơ bản sau đây [3]: + Tính đủ: tất cả các lỗi đều không được bỏ qua, nếu trong miền ngữ nghĩa cụ thể chứa thông tin về lỗi (giao với vùng vi phạm khác rỗng) thì miền ngữ nghĩa trừu tượng cũng phải chứa thông tin về lỗi đó; + Tính chính xác: quá trình trừu tượng hóa để tạo ra miền ngữ nghĩa trừu tượng phải đủ chính xác để tránh cảnh báo sai (false alarm); + Đơn giản: Miền ngữ nghĩa trừu tượng phải đơn giản nhất có thể (tránh hiện tượng bùng nổ tổ hợp) Biểu diễn tính đủ trong hình 2.6: Miền ngữ nghĩa trừu tượng không đảm bảo tính đủ nên bỏ sót lỗi/miền trừu tượng vi phạm vùng cấm.
23 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.