NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN

➤ Gửi thông báo lỗi ⚠️ Báo cáo tài liệu vi phạm

Loại tài liệu: PDF

Số trang: 57 Trang

Tài liệu: ✅ ĐÃ ĐƯỢC PHÊ DUYỆT

TẢI VỀ

Nội dung chi tiết: NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN

NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN

ĐẠI HỌC Ql Óc GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆTrần Thị Vân DungNGHIÊN CỨU VÉ KIÊM CHỨNG PHÀN MÈM sử DỤNG CÔNG CỤ SPINKHOÁ LUẬN TÓT NGHIỆP ĐẠI HỌC H

NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN HẸ CHÍNH QUYNgành: Công Nghệ Thông TinHÀ NỘI - 2010ĐẠI HỌC QUÓC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC C ÔNG NGHẸTrần Thị Vân DungNGHIÊN CỨU VỀ KIỂM CHỨNG PHẢN MÈM

sử DỤNG CÔNG CỤ SPINKIIOÁ LUẬN TÓT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUYNgành: Công Nghệ Thông TinCán hộ hirớng dần: PGS. TS. Nguyễn Việt HàCán bộ đông hướng d NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN

ẫn: TS. Phạm Ngọc HùngHÀ NỘI-2010Lời cảm ơnl.ời đầu liên, em xin được bày lõ lòng biết

NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN

ng dã tận tinh giúp dờ em làm và hoãn thiện khóa luận trong SUÔI năm học vừa qua.Em xin dược bày to lòng biết ơn tới các thầy, cỏ trong khoa Công Nghệ

NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN ọc tập tại ĐIICN, dặc biệt lã irong thời gian thực hiện khóa luận lôl nghiệp.Tôi xin cám ơn các bạn sinh viền lớp K51CC và K51CNPM Trường Dại học ('ôn

g nghệ, những người bạn dà cùng tôi học tập và rèn luyện trong suốt nhũng năm học dại học.Cuối cùng con xin gứi tới Bố Me vã gia đinh tình thương yêu NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN

và lòng biết ơn. Bố Mẹ đà nuôi dưỗng và luôn là chỗ dựa tinh thần cho con.Hà Nội. ngày 18 tháng 5 năm 2010Trần Thị Vân DungTóm tăt nội dungKiểm chứng

NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN

mô hình (model checking) lã một phương pháp hình thức dùng cho việc kiêm chứng hệ thống. Kiêm chửng mò hình kháo sát tất cả các trạng thái có thê của

NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN hần mèm và Spin Là một trong nhùng bô kiêm chứng (model checker) được sư dung rộng rài. Các bô kiểm chứng không kiêm tra trực tiếp chương trinh mà kiê

m tra một mò hình là thê hiện mức cao cùa hệ thống Mô hình này mô ta hành VI cùa hê thống Đế áp dung được các công cụ kiếm chửng mò hình, việc đẩu tiê NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN

n là phải xây dựng mô hình của hệ thống. Các mô hình này cùng với đặc ta cua thuộc tinh cần kiêm tra Là đâu vào của các bô kiêm chứng.Khóa luân nghiên

NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN

cứu việc kiềm chứng phần mềm sư dụng Spin, cu thế là việc kiếm chửng mô hĩnh máy hữu hạn trạng thái, sau đó đưa ra một công cụ chuyên một mô tả ban đ

NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN .....................................................61.2.Mục tiêu và phạm vi của đề tài.......................................71.3.Cấu trúc khóa luận

...................................................72Sơ lược về Model Checking2.1.Kiếm chứng hè thống................................................. NGHIÊN cứu về KIỂM CHỨNG PHẦN mềm sử DỤNG CÔNG cụ SPIN

.82.2.Model Checking.......................................................9