Đăng ký Đăng nhập
Trang chủ Phân tích tĩnh chương trình bằng phương pháp giải thích trừu tượng...

Tài liệu Phân tích tĩnh chương trình bằng phương pháp giải thích trừu tượng

.PDF
65
97
94

Mô tả:

ĐẠI HỌC THÁI NGUYÊN TRƯỜNG ĐẠI HỌC CÔNG NGHỆ THÔNG TIN VÀ TRUYỀN THÔNG NGUYỄN THANH BẰNG PHÂN TÍCH TĨNH CHƯƠNG TRÌNH BẰNG PHƯƠNG PHÁP GIẢI THÍCH TRỪU TƯỢNG LUẬN VĂN THẠC SĨ KHOA HỌC MÁY TÍNH Thái Nguyên, năm 2013 ĐẠI HỌC THÁI NGUYÊN TRƯỜNG ĐẠI HỌC CÔNG NGHỆ THÔNG TIN VÀ TRUYỀN THÔNG NGUYỄN THANH BẰNG PHÂN TÍCH TĨNH CHƯƠNG TRÌNH BẰNG PHƯƠNG PHÁP GIẢI THÍCH TRỪU TƯỢNG Chuyên ngành : KHOA HỌC MÁY TÍNH Mã số : 60.48.01 NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. Nguyễn Trường Thắng Thái Nguyên, năm 2013 LỜI CAM ĐOAN Tôi xin cam đoan tất cả những nội dung đƣợc trình bày trong nội dung luận văn đều do tôi nghiên cứu và viết ra dƣới sự hƣớng dẫn của TS. Nguyễn Trƣờng Thắng – Viện Công nghệ thông tin – Viện Khoa học và công nghệ Việt Nam hƣớng dẫn. Không hề có bất cứ sự sao chép nào ngoài việc tham khảo từ các tài liệu nhƣ đã trình bày trong phần tài liệu tham khảo. Nếu có một hình thức gian lận nào tôi xin hoàn toàn chịu trách nhiệm. Thái Nguyên, tháng 01 năm 2013 Học viên cao học khóa 9. Chuyên ngành: Khoa học máy tính. Trƣờng đại học Công nghệ thông tin và truyền thông Đại học Thái Nguyên MỤC LỤC LỜI CAM ĐOAN ........................................................................................... 2 MỤC LỤC ...................................................................................................... 3 DANH MỤC CÁC KÝ HIỆU, CÁC CHỮ VIẾT TẮT ................................. 5 DANH MỤC CÁC THUẬT NGỮ................................................................. 6 DANH MỤC CÁC HÌNH .............................................................................. 7 MỞ ĐẦU ........................................................................................................ 8 CHƢƠNG I. TỔNG QUAN......................................................................... 10 1.1. Công nghệ phần mềm và các vấn đề liên quan ................................. 10 1.1.1. Khái niệm về công nghệ phần mềm ........................................... 10 1.1.2. Quy trình phát triển phần mềm .................................................. 11 1.2 Các kỹ thuật trong công nghệ phần mềm nhằm nâng cao chất lƣợng phần mềm ................................................................................................. 13 1.2.1. Kiểm chứng phần mềm .............................................................. 14 1.2.2. Phân tích mã nguồn tĩnh ............................................................. 15 1.2.3. Kiểm thử phần mềm ................................................................... 17 1.2.4. So sánh giữa kiểm chứng mô hình và kiểm thử phần mềm ....... 18 1.3 Kết luận chƣơng 1. ............................................................................. 18 CHƢƠNG II. PHƢƠNG PHÁP GIẢI THÍCH TRỪU TƢỢNG ................ 19 2.1. Khái niệm giải thích trừu tƣợng ....................................................... 19 2.2. Ứng dụng của giải thích trừu tƣợng. ................................................ 19 2.3. Một số khái niệm cơ bản. ................................................................. 20 2.3.1. Ngữ nghĩa ................................................................................... 20 2.3.2. Tính an toàn: .............................................................................. 20 2.3.3. Giải thích trừu tƣợng:................................................................. 21 2.3.4. Tiêu chuẩn trừu tƣợng hóa: ........................................................ 22 2.3.5. Miền trừu tƣợng: (Abstract domains): ....................................... 22 2.3.6. Vết thực thi ................................................................................. 23 2.3.7. Thu thập ngữ nghĩa: ................................................................... 25 2.4. Nền tảng toán học của giải thích trừu tƣợng. ................................... 26 2.4.1. Liên kết nhị phân........................................................................ 26 3 2.4.2. Tập có thứ tự từng phần (Poset)................................................. 26 2.4.3. Cấu trúc dàn (Lattices) ............................................................... 27 2.4.4. Sơ đồ Hasse ................................................................................ 28 2.4.5. Điểm cố định (Fixpoint)............................................................. 28 2.4.6. Bƣớc lặp ..................................................................................... 29 2.4.7. Kết nối Galois ............................................................................ 29 2.5. Giải thích trừu tƣợng. ....................................................................... 29 2.5.1. Đối tƣợng trừu tƣợng (Abstract objects) ................................... 30 2.5.2. Thuộc tính trừu tƣợng................................................................ 31 2.5.3. Giải thích trừu tƣợng trong phân tích tĩnh chƣơng trình: .......... 32 2.5.4. Kết luận chƣơng 2. .................................................................... 34 CHƢƠNG III. CHƢƠNG TRÌNH THỰC NGHIỆM .................................. 35 3.1. Giới thiệu về TVLA ......................................................................... 35 3.2. Nền tảng toán học của TVLA .......................................................... 36 3.2.1. Giá trị 3-logic ............................................................................. 37 3.2.2. Phƣơng pháp .............................................................................. 39 3.3. Phân tĩnh tĩnh chƣơng trình sử dụng TVLA. ................................... 43 3.3.1. Bài toán 1 ............................................................................... 43 3.3.2. Bài toán 2 ............................................................................... 48 3.4. Kết luận chƣơng 3. ........................................................................... 53 KẾT LUẬN VÀ HƢỚNG PHÁT TRIỂN ................................................... 54 TÀI LIỆU THAM KHẢO ............................................................................ 55 PHỤ LỤC ..................................................................................................... 56 1. Thuật toán phân tích mối quan hệ vô hạn thông qua lặp tiến/lùi chi tiết . .............................................................................................................. 56 2. Các định nghĩa chức năng trừu tƣợng trong action.tvp. ...................... 57 3. Các định nghĩa chức năng trừu tƣợng trong predicates.tvp. ................ 62 4. Dữ liệu đầu vào của TVLA phân tích chức năng tạo danh sách liên kết creat.tvp .................................................................................................... 64 4 DANH MỤC CÁC KÝ HIỆU, CÁC CHỮ VIẾT TẮT STT Từ viết tắt 1 EASL 2 CM 3 PTTGTT 4 CFG Viết đầy đủ Nghĩa Engineering Analysis and Kỹ thuật Phân tích và Simulation Language ngôn ngữ mô phỏng Summary nodes Nút đại diện Phân tích tĩnh chƣơng trình bằng giải thích trừu tƣợng. Control Flow Graphc 5 Sơ đồ luồng điều khiển. DANH MỤC CÁC THUẬT NGỮ STT Ý nghĩa Thuật ngữ Tập hợp các dấu vết về quá trình 1 Vết thực thi (Trace semantics) chuyển đổi trạng thái của chƣơng trình. 2 Tập có thứ tự từng phần (Poset Là một tập hợp các phần tử có - Partial Ordered Set) thứ tự Là một tập hợp các phần tử có 3 thứ tự từng phần có điểm chặn Cấu trúc dàn (Lattice) dƣới lớn nhất và trặn trên nhỏ nhất 6 DANH MỤC CÁC HÌNH Hình sử dụng STT 1 Hình 1.1: Mô hình tổng quát quy trình sản xuất phần mềm trong xe hơi 2 Hình 1.2: Tổng quan phân tích mã nguồn tĩnh 3 Hình 1.3: MISRA-C là “Subset”-Tập con của ngôn ngữ C 4 Hình 1.4: Hai cuốn MISRA-C:1998 và MISRA-C:2004 5 Hình 2.1 Sơ đồ hành vi của chƣơng trình 6 Hình 2.2 Quỹ đạo an toàn 7 Hình 2.3 Quỹ đạo không an toàn 8 Hình 2.4 Quỹ đạo hành vi trừu tƣợng của chƣơng trình. 9 Hình 2.4 Phát hiện lỗi với giải thích trừu tƣợng 10 Hình 2.5 Các bƣớc chuyển trạng thái của chƣơng trình 11 Hình 2.6 Vết thực thi của chƣơng trình 12 Hình 2.7 Thu thập ngữ nghĩa của chƣơng trình 13 Hình 2.8 Đồ thị liên kết nhị phân 14 Hình 2.9 Thuật toán giải thích trừu tƣợng tổng quát 15 Hình 3.1 Bảng giá trị phép giao 3-logic 16 Hình 3.2 Bảng giá trị phép hợp 3-logic 17 Hình 3.3 Bảng giá trị phép hợp 3-logic. 18 Hình 3.4 Bảng trừu tƣợng hóa bằng logic vị từ 19 Hình 3.5 Mô phỏng trạng thái bộ nhớ cấu trúc con trỏ. 20 Hình 3.6 Trạng thái chƣơng trình sử dụng 2-logic 21 Hình 3.7 Trạng thái chƣơng trình sử dụng nút đại diện (3-logic) 22 Hình 3.8 Tiến trình làm việc của một quá trình PTTGTTT 23 Hình 3.9 Thực hiện phân tích tĩnh chƣơng trình bằng TVLA. 24 Hình 3.10. Kết quả phân tích chức năng tạo danh sách liên kết 25 Hình 3.11. Trạng thái tổng thể chƣơng trình thêm một nút vào cây nhị phân 7 MỞ ĐẦU Ngày nay, phần mềm xuất hiện ở khắp mọi nơi và trong hầu hết các thiết bị điện tử đều sử dụng phần mềm trong đó. Phần mềm không đơn giản là chƣơng trình trên máy tính mà nó bao gồm cả tƣ liệu lƣu trữ và thông tin vận hành giúp chƣơng trình có thể hoạt động đƣợc. Vì những ứng dụng to lớn của phần mềm trong các ngành sản xuất, tài chính ngân hàng, y tế, bệnh viện, trƣờng học, nhà nƣớc,...nên yêu cầu rất lớn đặt ra đó là xây dựng, phát triển và ứng dụng công nghệ phần mềm. Trong luận văn này tôi xin giới thiệu một phƣơng pháp kiểm tra đánh giá chất lƣợng phần mềm mới đó là phân tích tĩnh chƣơng trình. Với mục tiêu: Đƣa ra một cách nhìn nhận mới về việc lập xây dựng và kiểm tra sự đúng đắn của chƣơng trình đó là sử dụng phƣơng pháp phân tích tĩnh chƣơng trình. Áp dụng các công cụ để phân tích chƣơng trình, kiểm tra sự đúng đắn của chƣơng trình bằng giải thích trừu tƣợng (Abstract Interpretation). Vì đây là một kỹ thuật phân tích chƣơng trình chƣa đƣợc nghiên cứu rộng rãi ở Việt Nam, nên luận văn này mang tính giới thiệu ban đầu về khái niệm cơ bản và nền tảng lý thuyết dựa trên tài liệu gốc [2], là giáo trình đƣợc sử dụng trong đào tạo thạc sỹ của Học viện Công nghệ Massachussette (MIT) – Hoa Kỳ, trong chƣơng 2. Phần thử nghiệm trong chƣơng 3 tập trung vào việc cài đặt và thử nghiệm bộ công cụ TVLA (3Valued Logic Analysis Engine) của trƣờng đại học Khoa Học Máy Tính Tel Aviv (School of Computer Science Tel Aviv University), thành phố Tel Aviv, Isarel[6]. Công cụ này phân tích chƣơng trình sử dụng giải thích trừu tƣợng. Nội dung luận văn gồm 3 chƣơng: CHƢƠNG I. TỔNG QUAN Đƣa ra các khái niệm liên quan, sự cần thiết của việc phân tích tĩnh chƣơng trình, giới thiệu các phƣơng pháp phân tích tĩnh chƣơng trình. CHƢƠNG II. PHƢƠNG PHÁP GIẢI THÍCH TRỪU TƢỢNG 8 Trình bày nền tảng lý thuyết, thuật toán, ứng dụng, ƣu nhƣợc điểm của phƣơng pháp giải thích trừu tƣợng.[2] CHƢƠNG III. CHƢƠNG TRÌNH THỰC NGHIỆM Cài đặt phƣơng pháp phân tích tĩnh bằng giải thích trừu tƣợng, đƣa ra kết quả thực nghiệm và kết luận[6] 9 CHƢƠNG I. TỔNG QUAN 1.1. Công nghệ phần mềm và các vấn đề liên quan 1.1.1. Khái niệm về công nghệ phần mềm Công nghệ phần mềm là một quá trình tích hợp quy trình, các phƣơng pháp và các công cụ nhằm tạo ra một phần mềm hiệu quả. Công nghệ phần mềm là một ngành công nghệ tập trung vào tất cả các mặt trong sản xuất phần mềm, từ những bƣớc khởi đầu trong định dạng hệ thống đến bƣớc bảo trì hệ thống sau khi phần mềm đã đƣợc đƣa vào sử dụng. Các kỹ sƣ phần mềm không chỉ cần tập trung vào các mảng kỹ thuật trong phát triển phần mềm mà còn vào cả các hoạt động nhƣ quản lý dự án, phƣơng pháp làm phần mềm, đảm bảo chất lƣợng phần mềm, định dạng cấu hình phần mềm, và phát triển các công cụ hỗ trợ cho sản xuất phần mềm. Các chƣơng trình khoa học máy tính hầu hết đều tập trung vào lý thuyết và phƣơng pháp của máy tính và các cơ sở về lập trình. Chƣơng trình công nghệ phần mềm thay vào đó tập trung cho các mặt thực tiễn trong sản xuất phần mềm có chất lƣợng và mối quan hệ của nó với công việc kinh doanh. Vì lẽ đó, các kỹ sƣ phần mềm phải có kiến thức về khoa học máy tính và hơn thế nữa vì họ sẽ phải đối mặt với các vấn đề về sản xuất và ứng dụng phần mềm mà khoa học máy tính thƣờng chỉ thuần túy tiếp cận bằng các lý thuyết và thuật toán. Các lý thuyết của khoa học máy tính thƣờng trừu tƣợng nhƣ toán học phức tạp và luôn không thể áp dụng cho các bài toán phức tạp trong thực tế, vốn đòi hỏi một giải pháp công nghệ phần mềm. Khoa học máy tính thƣờng tập trung vào việc chuyển đổi các công thức toán học thành các thuật toán lập trình, vì thế toán học thƣờng là nền tảng cơ bản. Công nghệ phần mềm cần tập trung cho các hoạt động liên quan đến việc sản xuất sản phẩm phần mềm vì yếu tố quy trình là nền tảng quan trọng nhất. 10 1.1.2. Quy trình phát triển phần mềm Quá trình phát triển phần mềm là tập hợp các thao tác và các kết quả tƣơng quan để sản xuất ra một sản phẩm phần mềm. Hầu hết các thao tác này đƣợc tiến hành bởi các kỹ sƣ phần mềm. Các công cụ hỗ trợ máy tính về kỹ thuật phần mềm có thể đƣợc dùng để giúp trong một số thao tác. Có 4 thao tác là nền tảng của hầu hết các quá trình phần mềm là: - Đặc tả phần mềm: Các chức năng của phần mềm và điều kiện để nó hoạt động phải đƣợc định nghĩa. - Sự phát triển phần mềm: Để phần mềm đạt đƣợc đặc tả thì phải có quá trình phát triển này. - Đánh giá phần mềm: Phần mềm phải đƣợc đánh giá để chắc chắn rằng nó làm những gì mà khách hàng muốn. - Sự tiến hóa của phần mềm: Phần mềm phải tiến hóa để thỏa mãn sự thay đổi các yêu cầu của khách hàng 1.1.3. Phân loại phần mềm Đối tƣợng chính của công nghệ phần mềm là sản xuất ra các sản phẩm phần mềm. Sản phẩm phần mềm đƣợc phân loại theo 3 cách đó là theo mức độ hoàn thiện, theo chức năng, và theo lĩnh vực ứng dụng, cụ thể nhƣ sau: Theo mức độ hoàn thiện : - Phần mềm hệ thống : Điều hành các hoạt động của hệ thống - Phần mềm nghiệp vụ : Hỗ trợ tốt các hoạt động nghiệp vụ khác nhau với sự đa dạng và số lƣợng lớn Theo chức năng : Phần mềm công cụ (Tools, CASE) : Trợ giúp cho quá trình phát triển phần mềm, nhƣ công cụ kiếm soát mã nguồn tĩnh - “TVLA” đƣợc giới thiệu ở Chƣơng 3. Theo lĩnh vực ứng dụng : 11 - Phần mềm hệ thống: Đây là phần mềm tƣơng tác trực tiếp với phần cứng, sử dụng cho các chƣơng trình khác nhau, và nhiều đối tƣợng ngƣời dùng khác nhau. - Phần mềm thời gian thực : Thu thập, xử lý các dữ kiện thời gian thực và đáp ứng yêu cầu chặt chẽ về thời gian. - Phần mềm nghiệp vụ : Xử lý thông tin nghiệp vụ, gắn với cơ sở dữ liệu, nhƣ là : xử lý các giao tác ( mạng bán hàng,…), hệ điều khiển vũ trụ. - Phần mềm khoa học kỹ thuật : Sử dụng các thuật toán phức tạp ( vật lý, mô phỏng,…). Đây là phần mềm có năng lực tính toán cao. - Phần mềm nhúng: Là sự kết hợp giữa hệ thống và thời gian thực. Ngoài ra, còn có các phần mềm khác nhƣ : Phần mềm trí tuệ nhân tạo, phần mềm dựa trên nền Web, phần mềm máy tính cá nhân,.v.v.. 1.1.4. Chất lƣợng của phần mềm Ngành công nghiệp phần mềm đang phát triển rất nhanh và trở thành ngành khổng lồ. Nhƣng bên cạnh sự phát triển đó cũng có rất nhiều khó khăn đặt ra nhƣ năng suất lập trình vẫn còn thấp, sự phát triển vẫn mang tính thủ công, giá thành đắt,…Vì vậy, vấn đề bảo đảm chất lƣợng phần mềm đang trở thành trọng tâm. Chất lƣợng của phần mềm theo quan điểm lập trình đó chính là chất lƣợng của chƣơng trình. Vấn đề là làm thế nào để chƣơng trình chạy giống nhƣ thiết kế, đây chính là chất lƣợng theo nghĩa cần thiết. Chất lƣợng của phần mềm theo quan điểm ngƣời sử dụng phần mềm đó là chất lƣợng thiết kế. Vấn đề là làm thế nào để thiết kế đáp ứng đúng nhu cầu của ngƣời sử dụng. Ngƣời ta cũng nói đó là chất lƣợng theo nghĩa hấp dẫn. Một phần mềm tốt không những đáp ứng nhu cầu của ngƣời phát triển mà phải thoả mãn ngƣời sử dụng: có độ tin cậy cao về chất lƣợng và mức độ thoả mãn của ngƣời sử dụng đối với sản phẩm hay dịch vụ . Một phần mềm đáp ứng đƣợc yêu cầu thì cần có các tính chất sau: Chạy đúng: đây là yếu tố cốt lõi, không thể thiếu của một chƣơng trình. Nó phải thực hiện chính xác công việc mà nó đảm nhiệm. 12 Tính bảo trì đƣợc: Nó có khả năng thực hành những tiến triển để thỏa mãn yêu cầu của khách hàng. Tính an toàn: Khả năng tin cậy của phần mềm bao gồm một loạt các đặc tính nhƣ là độ tin cậy, an toàn, và bảo mật. Phần mềm tin cậy không thể tạo ra các thiệt hại vật chất hay kinh tế trong trƣờng hợp hƣ hỏng. Tính hiệu quả: Phần mềm không thể phí phạm các nguồn tài nguyên nhƣ là bộ nhớ và các chu kì vi xử lý. Tính tiện dụng: Phần mềm nên có một giao diện tƣơng đối dễ cho ngƣời dùng và có đầy đủ các hồ sơ về phần mềm Giá thành rẻ,... 1.2 Các kỹ thuật trong công nghệ phần mềm nhằm nâng cao chất lƣợng phần mềm Công nghệ phần mềm là lĩnh vực rất rộng lớn. Tuy nhiên, một trong những mảng chính của nó là kiểm soát chất lƣợng phần mềm. Trong mảng này, có nhiều loại kỹ thuật khác nhau để nâng cao chất lƣợng phần mềm. Các loại cơ bản: kiểm chứng mô hình , phân tích tĩnh, kiểm thử động,.... 13 Hình 1.1: Mô hình tổng quát quy trình sản xuất phần mềm trong xe hơi 1.2.1. Kiểm chứng phần mềm Kiểm chứng mô hình là phƣơng pháp để xem thiết kế phần cứng và phần mềm có đúng theo đặc tả và thiết kế ban đầu hay không. Kiểm chứng mô hình là một kỹ thuật kiểm chứng tự động các hệ thống hữu hạn trạng thái. Kiểm chứng mô hình xác minh tính đúng đắn của một mô hình bằng việc xác định xem các thuộc tính ngƣời dùng mong muốn có đƣợc thỏa mãn bởi mô hình đó hay không. Về nguyên tắc hoạt động, hệ thống cần kiểm chứng sẽ đƣợc mô hình hóa. Công cụ kiểm chứng sẽ kiểm tra mô hình có 14 thỏa mãn các thuộc tính đƣợc cho hay không. Nhờ khả năng duyệt qua tất cả các trạng thái trong mô hình mà tính đúng đắn của kết quả kiểm chứng mô hình luôn đƣợc đảm bảo. Kiểm chứng mô hình bao gồm 3 bƣớc: Mô hình hóa, đặc tả và kiểm chứng. Ở bƣớc mô hình hóa, kết quả tạo ra là một mô hình mà các công cụ kiểm chứng có thể sử dụng đƣợc. Đầu vào của bƣớc này có thể là bản thiết kế phần mềm hoặc là các dòng mã lập trình. Trong bƣớc tiếp theo, các thuộc tính mà bản thiết kế cần thỏa mãn đƣợc đặc tả. Các thuộc tính này thƣờng đƣợc diễn đạt bằng các biểu thức logic. Kết quả của hai bƣớc mô hình hóa và đặc tả chính là đầu vào của kiểm chứng mô hình. Trong bƣớc cuối cùng, kiểm chứng, công cụ kiểm chứng sẽ tự động thực hiện và trả về kết quả là thỏa mãn nếu mô hình thỏa mãn các thuộc tính, hoặc đƣa ra một phản ví dụ nếu mô hình không thỏa mãn. Dựa vào phản ví dụ, ngƣời ta có thể tìm ra đƣợc lý do vì sao mô hình không thỏa mãn các thuộc tính đặt ra. Tóm lại, kiểm chứng mô hình là một kĩ thuật giúp kiểm tra một chƣơng trình hoặc một bản thiết kế có thỏa mãn các tính chất đặt ra hay không một cách tự động. Đầu vào của nó là một mô hình cần kiểm chứng và các thuộc tính mà nó cần thỏa mãn. Đầu ra là kết luận một mô hình thỏa mãn các tính chất hoặc đƣa ra một phản ví dụ nếu mô hình không thỏa mãn. 1.2.2. Phân tích mã nguồn tĩnh Phân tích mã nguồn tĩnh, hay còn gọi là kiểm thử mô hình là một phƣơng pháp dùng để tìm lỗi hay đảm bảo sự phù hợp để mã hóa các nguyên tắc, không làm chỉnh sửa trực tiếp mã nguồn chƣơng trình đó và nó thực hiện các thuật toán kiểm tra mã nguồn đƣa vào dƣới dạng cây cú pháp trừu tƣợng rồi đánh dấu phân tích ở những nơi mà các lỗi từ vựng, cú pháp và thậm chí một số lỗi ngữ nghĩa có thể xảy ra. Nói cách khác, các công cụ phân tích tĩnh phát hiện trong mã nguồn chƣơng trình những nơi có chứa hoặc có khả năng chứa lỗi, bị lỗi hoặc sở hữu định dạng xấu. Đoạn mã nhƣ vậy sẽ đƣợc xem xét cẩn thận của lập trình viên và có thể quyết định sửa đổi 15 phần này chƣơng trình hay không. Các lợi thế chính của việc sử dụng phân tích mã tĩnh nằm ở khả năng tiết kiệm chi phí đáng kể của các loại bỏ khuyết tật trong một chƣơng trình. Error Report Suocre Code Static Analysis Quality Report Software Metric Tools Hình 1.2: Tổng quan phân tích mã nguồn tĩnh Công cụ phân tích mã nguồn tĩnh là một “phần mềm công cụ” đƣợc xây dựng để kiểm chứng mã nguồn cho phép phát hiện một số lƣợng lớn các lỗi ở giai đoạn xây dựng, và điều này làm giảm đáng kể chi phí của việc phát triển toàn bộ dự án. Phân tích tĩnh chƣơng trình có các phƣơng pháp nhƣ sau: - Kiểm tra mô hình: Trong kiểm tra mô hình, một mô hình của hệ thống đƣợc tạo ra để hỗ trợ phân tích mọi sự thực thi có thể trong mô hình. Kiểm tra mô hình có thể kiểm chứng đƣợc rằng mô hình của hệ thống hoạt động chính xác trong tất cả trƣờng hợp có thể. Kiểm tra mô hình phân tích hết mọi khía cạnh thực thi của chƣơng trình và chỉ ra những sự vi phạm nhƣng không chứng minh đƣợc chƣơng trình sẽ đƣợc thực thi chính xác mà không có lỗi. Hạn chế của kiểm tra mô hình đó là không gian trạng thái của mô hình thƣờng quá lớn do đó việc thám hiểm tất cả các trạng thái không phải lúc nào cũng thực hiện đƣợc. 16 - Phân tích luồng dữ liệu: Là một kỹ thuật cổ điển trong phân tích tĩnh, nó đƣợc sử dụng để tìm ra các thuộc tính quan trọng của các chƣơng trình đƣợc phân tích, giúp các kỹ sƣ phần mềm tối ƣu hóa chƣơng trình của mình. Trong lập trình hiện đại kỹ thuật phân tích tĩnh dựa trên luồng dữ liệu đƣợc các kỹ sƣ phần mềm dùng để hoàn thiện các chức năng chính của chƣơng trình; - Giải thích trừu tƣợng: Diễn giải về các ngữ nghĩa của một chƣơng trình phần mềm máy tính, với những hàm đơn điệu trên các tập hợp đã đƣợc xếp thứ tự. Đây là nội dung nghiên cứu chính của đề tài, sẽ đƣợc trình bày chi tiết trong chƣơng 2 và chƣơng 3. Phần lớn những kết quả lý thuyết của 2 chƣơng này đƣợc trích dẫn từ tài liệu [2][6]. 1.2.3. Kiểm thử phần mềm Việc tạo ra một sản phẩm thì không phải chỉ do một tổ chức đứng ra làm từ đầu đến cuối, mà đòi hỏi sự liên kết, tích hợp của rất nhiều sản phẩm, thƣ viện lập trình,…của nhiều tổ chức khác nhau…Để chứng tỏ rằng các chức năng phần mềm có làm theo đúng đặc tả và các yêu cầu về hiệu năng hay không ta phải tiến hành một quá trình gọi là kiểm thử. Kiểm thử phần mềm là hoạt động khảo sát thực tiễn sản phẩm hay dịch vụ phần mềm trong đúng môi trƣờng chúng dự định sẽ đƣợc triển khai nhằm cung cấp cho ngƣời có lợi ích liên quan những thông tin về chất lƣợng của sản phẩm hay dịch vụ phần mềm ấy. Kiểm thử là một quá trình thực thi chƣơng trình với mục đích là tìm ra các lỗi hay khiếm khuyết của phần mềm nhằm đảm bảo hiệu quả hoạt động tối ƣu của phần mềm trong nhiều ngành khác nhau. Thông tin đầu vào đƣợc cung cấp cho quá trình kiểm thử bao gồm: - Thông tin cấu hình của phần mềm. - Thông tin cầu hình về kiểm thử. 17 1.2.4. So sánh giữa kiểm chứng mô hình và kiểm thử phần mềm Cả kiểm chứng mô hình và kiểm thử phần mềm đều thực hiện vai trò đảm bảo chất lƣợng phần mềm bằng việc tìm ra các lỗi nếu có của phần mềm. Tuy nhiên giữa kiểm chứng mô hình và kiểm thử phần mềm có một số điểm khác nhau quan trọng sau: Kiểm thử phần mềm đòi hỏi phải có chƣơng trình để thực hiện, còn kiểm chứng mô hình thì ngoài kiểm thử trên mã nguồn còn có thể dùng để kiểm chứng bản thiết kế, nghĩa là khi chƣơng trình vẫn còn trên giấy. Kiểm thử phần mềm chỉ có thể khẳng định đƣợc chƣơng trình không gặp lỗi đối với các trƣờng hợp kiểm thử đã kiểm tra tức không tìm thấy lỗi chứ không khẳng định đƣợc là chƣơng trình hoàn toàn không còn lỗi. Ngƣợc lại, kiểm chứng phần mềm cho phép ta kết luận đƣợc chƣơng trình hoàn toàn không còn lỗi. Nhƣ vây, ta cũng có thể kiểm thử phần mềm có ƣu điểm rất lớn là dễ thực hiện. Một ngƣời bình thƣờng cũng có thể thực hiện đƣợc. Trong khi đó, kiểm chứng mô hình đòi hỏi phải mô hình hóa và đặc tả, kỹ thuật này rất khó và yêu cầu ngƣời thực hiện có trình độ kinh nghiệm và kiến thức nhất định Do đó, về bản chất phân tích tĩnh chƣơng trình và kiểm thử chƣơng trình bằng các bộ dữ liệu cụ thể là hai mặt bổ sung cho nhau. Phân tích tĩnh chƣơng trình tập trung cho sự đúng đắn của thuật toán, cấu trúc chƣơng trình trong khi kiểm thử phần mềm tập trung cho sự đúng đắn của ngôn ngữ lập trình. 1.3 Kết luận chƣơng 1. Trong chƣơng này, tôi đã giới thiệu các khái niệm liên quan đến công nghệ phần mềm, quy trình phát triển phần mềm, kỹ thuật kiểm thử phần mềm, phân tích tĩnh chƣơng trình. Chƣơng 2 sẽ tìm hiểu sâu hơn về giải thích trừu tƣợng và phân tích tĩnh chƣơng trình bằng giải thích trừu tƣợng. 18 CHƢƠNG II. PHƢƠNG PHÁP GIẢI THÍCH TRỪU TƢỢNG 2.1. Khái niệm giải thích trừu tƣợng Giải thích trừu tƣợng (Abstract interpretation): Là một kỹ thuật trong phân tích tích chƣơng trình máy tính, kỹ thuật này diễn giải về ngữ nghĩa của một chƣơng trình phần mềm máy tính, với những hàm đơn điệu trên các tập hợp đã đƣợc xếp thứ tự. Giải thích trừu tƣợng đƣợc hiểu là việc thực thi một phần một chƣơng trình máy tính để lấy thông tin về nó: luồng điều khiển, luồng dữ liệu + Hình thức: cái tất cả những gì đã đƣợc chuẩn tắc hóa, đã đƣợc chứng minh bằng toán học. + Phi hình thức: 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 chƣơng trình dịch và trong gỡ rối chƣơng trình. 2.2. Ứng dụng của giải thích trừu tƣợng. 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 ngành khoa học máy tính. Giải thích trừu tƣợng đƣợc dùng để chứng minh tính đầy đủ và tính đúng đắn của hệ thống. Một số ứng dụng của giải thích trừu tƣợng nhƣ: - 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. - 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 bƣớc thực hiện lệnh của chƣơng trình đó. Từ đó chứng minh tính đúng đắn 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 đó. 19
- Xem thêm -

Tài liệu liên quan