tailieunhanh - Báo cáo "Kiểm chứng tính đúng đắn hệ thống tính toán của chương trình bằng kiểm duyệt mô hình "

Trình bày về cơ sở lý thuyết của kiểm duyệt mô hình (Model checking): khái niệm và ý nghĩa của kiểm duyệt mô hình, quy trình hoạt động của kiểm duyệt mô hình, đặc trưng của kiểm duyệt mô hình, điểm mạnh và điểm yếu của kiểm duyệt dựa trên mô hình sử dụng logic thời gian (Temporal Logic) mô tả các thuộc tính cần kiểm chứng. Nghiên cứu về công cụ Spin, giao diện Xspin, và ngôn ngữ mô hình hóa Promela, máy trạng thái hữu hạn. Tiến hành xây dựng tiến trình đồng hồ, mô hình hóa. | TT Ẳ 1 J 1 -4- 4- 1 j1 Ấ J 1 J r 1 Kiêm chứng tính đúng đăn hệ thông tính toán của 1 J 1 1 1 Ẳ 1 A V 1 1 chương trình băng kiêm duyệt mô hình Nguyễn Thị Loan Trường Đại học Công nghệ Luận văn ThS ngành Công nghệ phần mềm Mã sô 60 48 10 Cán bộ hướng dẫn khoa học TS. Đặng Văn Hưng Năm bảo vệ 2012 Abstract. Trình bày về cơ sở lý thuyết của kiêm duyệt mô hình Model checking khái niệm và ý nghĩa của kiêm duyệt mô hình quy trình hoạt động của kiêm duyệt mô hình đặc trưng của kiêm duyệt mô hình điêm mạnh và điêm yếu của kiêm duyệt dựa trên mô hình sử dụng logic thời gian Temporal Logic mô tả các thuộc tính cần kiêm chứng. Nghiên cứu về công cụ Spin giao diện Xspin và ngôn ngữ mô hình hóa Promela máy trạng thái hữu hạn. Tiến hành xây dựng tiến trình đồng hồ mô hình hóa hệ thông báo động báo cháy kết hợp tiến trình đồng hồ với kỹ thuật kiêm duyệt mô hình đê kiêm chứng tính đúng đăn của hệ thông đó. Keywords Công nghệ phần mềm Hệ thông tính toán Kiêm chứng mô hình Content. MỞ ĐẦU 1. Đặt vấn đề Ngày nay chúng ta phụ thuộc rất nhiều vào hệ thông máy tính cả trong sản xuất lẫn đời sông hàng ngày. Các hệ thông này cần phải đảm bảo sự tin cậy và an toàn khi sử dụng. Do đó chúng cần phải được kiêm duyệt kỹ càng ngay từ mô hình của hệ thông đê đảm bảo hệ thông hoạt động chính xác tránh gây thiệt hại cả về con người lẫn tiền của. Kỹ thuật kiêm chứng mô hình đã được sử dụng đê kiêm chứng cho các mô hình hệ thông trong thực tế. Các công cụ kiêm chứng đi kèm hiện nay hay dùng như Spin Kronos NuSMV . 2. Nội dung nghiên cứu Nội dung đề tài nghiên cứu về kỹ thuật kiêm chứng mô hình Model Checking dùng công cụ Spin đê thực hiện kiêm chứng mô hình hệ thông báo động báo cháy sử dụng ngôn ngữ mô hình hóa Promela đê mô hình hóa hệ thông báo động báo cháy và mô tả các thuộc tính cần kiêm chứng qua Logic thời gian tuyến tính đê kiêm chứng tính đúng đăn của hệ thông báo động báo cháy qua mô hình của nó. 3. Phương pháp nghiên cứu Phương pháp thu thập tài liệu. Phương pháp phân tích. 4. Cấu trúc .