Kiểm chứng chương trình dựa trên SMT

Nội dung bài viết

Đảm bảo chất lượng phần mềm

Máy tính và phần mềm máy tính ngày càng đóng vai trò to lớn trong nhiều lĩnh vực của đời sống xã hội như: kinh tế, giao thông, vũ trụ hay các dịch vụ y tế trong khám chữa bệnh… Thông thường các phần mềm máy tính không đứng riêng lẻ mà chúng được tích hợp hoặc nhúng trong các hệ thống phức tạp. Cho nên, việc đảm bảo chất lượng phần mềm là hết sức cần thiết. Việc đảm bảo chất lượng phần mềm trong các lĩnh vực như dịch vụ y tế hay vũ trụ hàng không lại càng được coi trọng. Bởi chỉ một sai sót nhỏ của hệ thống có thể gây ra những tổn thất to lớn về tính mạng con người cũng như về kinh tế.

Trong những năm gần đây, chúng ta cũng đã chứng kiến nhiều thảm họa xảy ra mà nguyên nhân lại nằm ở lỗi phần mềm chẳng hạn ngày 04/06/1996 tàu vũ trụ Ariane -5 đã nổ tung chỉ 36 giây sau khi khởi động. Nguyên nhân là do lỗi chuyển đổi một số dạng dấu phẩy động 64 – bit thành số nguyên dương 16-bit. Sự việc này xảy ra đã lâu, nhưng cho đến nay nó vẫn được nhắc đến như một thảm họa khủng khiếp nhất do lỗi phần mềm gây ra.

Rất nhiều kỹ thuật được nghiên cứu và sử dụng để khẳng định tính đúng đắn của hệ thống. Hai kỹ thuật truyền thống đã và đang được sử dụng để đảm bảo chất lượng phần mềm là kiểm thử phần mềm và kiểm chứng phần mềm (Software verification). Tuy nhiên, việc sử dụng các phương pháp kiểm thử chỉ làm giảm bớt lỗi của hệ thống mà không thể chứng minh được hệ thống không có lỗi. Các phương pháp kiểm chứng đang được quan tâm số một trong việc chứng minh tính đúng đắn của hệ thống. Phương pháp kiểm chứng mô hình (model checking) là sự lựa chọn hiệu quả trong việc chỉ ra hệ thống hoạt động đúng. Nhưng phương pháp này lại gặp phải vấn đề bùng nổ trạng thái khi thực hiện với các hệ thống lớn, phức tạp trong thực tế.

Luận văn trình bày phương pháp kiểm chứng dựa trên SMT (SAT Modulo Theories) sử dụng thực thi tượng trưng (symbolic execution) là phương pháp khác thay thế cho phương pháp kiểm chứng mô hình khi thực hiện với các hệ thống phức tạp.

Mục tiêu của luận văn

Mục tiêu của luận văn là tìm hiểu và trình bày về phương pháp kiểm chứng dựa trên SMT. Một phương pháp có nhiều ưu điểm cho vấn đề bùng nổ trạng thái của kiểm chứng mô hình.

Luận văn sẽ trình bày về công cụ KLEE, một công cụ kiểm chứng tự động sử dụng thực thi tượng trưng kết hợp với ba SMT solver được đánh giá là hiệu quả đó là Z3, Boolector và STP. Tiếp theo luận văn sẽ trình bày về ứng dụng của KLEE trong kiểm chứng một số thuộc tính của chương trình như phát hiện lỗi chia cho 0, lỗi tràn vùng đệm, lỗi truy cập ra ngoài kích thước của mảng, …

Nội dung luận văn

Luận văn gồm 4 chương, trong đó phần giới thiệu được trình bày trong chương 1.

Chương 2 trình bày về kiểm chứng chương trình, thực thi tượng trưng và một số kỹ thuật thực thi tượng trưng hiện đại đang được áp dụng trong các công cụ kiểm chứng.

Chương 3 trình bày về SMT một công cụ giải các công thức logic trên lý thuyết vị từ cấp I và việc áp dụng SMT, thực thi tượng trưng để kiểm chứng chương trình trên một số lý thuyết cụ thể.

Chương 4 trình bày về công cụ KLEE, thực nghiệm trên công cụ KLEE và các ứng dụng của nó trong việc kiểm chứng và phát hiện những lỗi của chương trình.

Phần kết luận trình bày kết luận quá trình nghiên cứu, đưa ra các kết quả đạt được và hướng nghiên cứu tiếp theo.

Link tải tài liệu: https://tii.la/PMX8poJY8Sg

Lưu ý: Link tải có chứa quảng cáo được rút gọn bằng Shrinkearn.com

Mật khẩu mở tệp PDF: sharetailieu.net

Nghiên cứu chế tạo và khảo sát tính chất vật liệu Polyme Nanocompozit trên cơ sở Polyaniline và Graphit

Nghiên cứu công nghệ chế tạo và tính chất của giả vật liệu Metamaterial

Nghiên cứu chế tạo vật liệu sắt điện BaTiO3 và tổ hợp BaTiO3/Fe3O4 có cấu trúc micro-nano bằng phương pháp thủy phân nhiệt

Tiếp cận các ứng dụng giao thức truyền thông không dây MiWi PRO

Nghiên cứu chế tạo và khảo sát tính chất vật liệu Polyme Nanocompozit trên cơ sở Polyaniline và Graphit

Nghiên cứu công nghệ chế tạo và tính chất của giả vật liệu Metamaterial

Nghiên cứu chế tạo vật liệu sắt điện BaTiO3 và tổ hợp BaTiO3/Fe3O4 có cấu trúc micro-nano bằng phương pháp thủy phân nhiệt

Tiếp cận các ứng dụng giao thức truyền thông không dây MiWi PRO

Đảm bảo chất lượng phần mềm

Mục tiêu của luận văn

Nội dung luận văn

LEAVE A REPLY Cancel reply

Mới Nhất

Nghiên cứu chế tạo và khảo sát tính chất vật liệu Polyme Nanocompozit trên cơ sở Polyaniline và Graphit

Nghiên cứu công nghệ chế tạo và tính chất của giả vật liệu Metamaterial

Nghiên cứu chế tạo vật liệu sắt điện BaTiO3 và tổ hợp BaTiO3/Fe3O4 có cấu trúc micro-nano bằng phương pháp thủy phân nhiệt

Tiếp cận các ứng dụng giao thức truyền thông không dây MiWi PRO

Nâng cao độ chính xác định vị robot bằng phương pháp tổng hợp dữ liệu cảm biến lập mã quang với bộ lọc Kalman...

Cùng Chuyên Mục

Đọc Nhiều Nhất

Áp dụng OSGi trong việc xây dựng hệ thống dựa thành...

Kiến trúc hướng dịch vụ và ứng dụng điện toán đám...

Nghiên cứu tính khả kiểm thử của ứng dụng trên nền...

Kiểm thử đơn vị cho hệ thống

Phát triền phần mềm cho người học tại Đại học Quốc...

Các kỹ thuật phân cụm trong khai phá dữ liệu sử...