Kiểm tra mô hình phần mềm sử dụng lý thuyết ôtômat buchi và logic thời gian tuyến tính

  • Số trang: 102 |
  • Loại file: PDF |
  • Lượt xem: 9 |
  • Lượt tải: 0
nganguyen

Đã đăng 34173 tài liệu

Mô tả:

BỘ GIÁO DỤC VÀ ĐÀO TẠO TRƯỜNG ĐẠI HỌC BÁCH KHOA HÀ NỘI ------------------------------- LUẬN VĂN THẠC SỸ KHOA HỌC KIỂM TRA MÔ HÌNH PHẦN MỀM SỬ DỤNG LÝ THUYẾT ÔTÔMAT BUCHI VÀ LOGIC THỜI GIAN TUYẾN TÍNH NGÀNH: CÔNG NGHỆ THÔNG TIN MÃ SỐ: PHẠM THỊ THÁI NINH Người hướng dẫn khoa học: TS. HUỲNH QUYẾT THẮNG HÀ NỘI 2006 1 LỜI CẢM ƠN Trước hết tôi xin gửi lời cảm ơn đặc biệt nhất tới Thầy TS Huỳnh Quyết Thắng, người đã định hướng đề tài và tận tình hướng dẫn chỉ bảo tôi trong suốt quá trình thực hiện bản luận văn cao học này, từ những ý tưởng trong đề cương nghiên cứu, phương pháp giải quyết vấn đề cho đến những lần kiểm tra cuối cùng để hoàn tất bản luận văn. Tôi xin chân thành bày tỏ lòng biết ơn sâu sắc tới Trung tâm Đào tạo Sau đại học và các thầy cô giáo trong khoa Công nghệ thông tin, trường Đại học Bách Khoa Hà Nội đã cho tôi nhiều kiến thức quý báu về các vấn đề hiện đại của ngành công nghệ thông tin, cho tôi một môi trường tập thể, một khoảng thời gian học cao học tuy ngắn ngủi nhưng khó quên trong cuộc đời. Tôi xin bày tỏ lòng cảm ơn chân thành tới tất cả các bạn bè, các đồng nghiệp đã động viên tôi trong suốt thời gian thực hiện bản luận văn này. Cuối cùng tôi xin dành một tình cảm biết ơn sâu nặng tới Bố, Mẹ và gia đình, những người đã luôn luôn ở bên cạnh tôi trong mọi nơi, mọi lúc trong suốt quá trình làm bản luận văn cao học này cũng như trong suốt cuộc đời tôi. Hà nội, tháng 11 năm 2006 Tác giả Phạm Thị Thái Ninh 2 LỜI CAM ĐOAN Tôi xin cam đoan đây là công trình nghiên cứu của riêng tôi. Các kết quả nêu trong bản luận văn này là trung thực và chưa từng được ai công bố trong bất cứ công trình nào khác. TÁC GIẢ LUẬN VĂN PHẠM THỊ THÁI NINH 3 MỤC LỤC LỜI CẢM ƠN ................................................................................................... 1 LỜI CAM ĐOAN ............................................................................................. 2 MỤC LỤC......................................................................................................... 3 DANH MỤC CÁC TỪ VIẾT TẮT .................................................................. 6 DANH MỤC CÁC HÌNH VẼ, ĐỒ THỊ ........................................................... 7 LỜI MỞ ĐẦU ................................................................................................... 8 CHƯƠNG I: TỔNG QUAN VỀ KIỂM TRA MÔ HÌNH PHẦN MỀM ....... 12 1.1 Lịch sử phát triển .................................................................................. 12 1.2 Kiểm tra mô hình phần mềm................................................................. 15 1.2.1 Khái niệm kiểm tra mô hình ........................................................ 15 1.2.2 Kiểm tra mô hình phần mềm ......................................................... 15 1.3 Phân loại hướng tiếp cận kiểm tra mô hình phần mềm ........................ 19 1.3.1 Cách tiếp cận động ......................................................................... 19 1.3.2 Cách tiếp cận tĩnh........................................................................... 19 1.3.4 Kết hợp giữa hai cách tiếp cận tĩnh và động.................................. 19 1.4 Kiểm tra mô hình phần mềm cổ điển và hiện đại ................................. 20 1.5 Kết luận chương .................................................................................... 22 CHƯƠNG 2: CÁC KỸ THUẬT KIỂM TRA MÔ HÌNH PHẦN MỀM ....... 23 2.1 Giới thiệu............................................................................................... 23 2.2 Phương pháp ký hiệu biểu diễn ............................................................ 25 2.3 Phương pháp duyệt nhanh..................................................................... 28 2.4 Phương pháp rút gọn ............................................................................. 30 2.4.1 Rút gọn bậc từng phần ................................................................... 30 2.4.2 Tối thiểu hoá kết cấu ...................................................................... 32 2.4.3 Trừu tượng hoá............................................................................... 33 2.5 Kỹ thuật xác thực kết cấu...................................................................... 35 2.6 Kết luận chương .................................................................................... 36 CHƯƠNG 3: KỸ THUẬT KIỂM TRA MÔ HÌNH PHẦN MỀM SỬ DỤNG LÝ THUYẾT LOGIC THỜI GIAN TUYẾN TÍNH VÀ ÔTÔMAT BUCHI 37 3.1 Bài toán kiểm tra mô hình phần mềm ................................................... 37 4 3.2 Mô hình hoá hệ thống phần mềm.......................................................... 38 3.2.1 Vấn đề đặt ra .................................................................................. 38 3.2.2. Hệ thống đánh nhãn dịch chuyển.................................................. 39 3.2.2.1 Các định nghĩa......................................................................... 39 3.2.2.2 Áp dụng mô hình hoá chương trình ........................................ 40 3.3 Đặc tả hình thức các thuộc tính của hệ thống ....................................... 43 3.3.1. Vấn đề đặt ra ................................................................................. 43 3.3.2. Logic thời gian .............................................................................. 44 3.3.3. Logic thời gian tuyến tính (Linear Temporal Logic - LTL) ......... 44 3.3.3.1 Thuộc tính trạng thái ............................................................... 45 3.3.3.2. Cú pháp LTL .......................................................................... 46 3.3.3.3. Ngữ nghĩa của LTL................................................................ 46 3.3.4 Logic thời gian nhánh (Branching Temporal Logic - BTL) .......... 50 3.4 Ôtômat đoán nhận các xâu vô hạn ....................................................... 51 3.4.1 Một số khái niệm ôtômat cổ điển:.................................................. 51 3.4.2 Ôtômat Buchi ................................................................................. 53 3.5 Chuyển đổi từ LTL sang Ôtômat Buchi............................................... 55 3.5.1 Tổng quan....................................................................................... 55 3.5.2 Chuẩn hoá về dạng LTL chuẩn ...................................................... 56 3.5.3 Biểu thức con ................................................................................. 56 3.5.4 Chuyển đổi từ LTL sang Ôtômat Buchi ........................................ 57 3.5.4.1 Giải thuật chuyển đổi từ LTL sang Ôtômat Buchi ................. 57 3.5.4.2. Ví dụ....................................................................................... 60 3.6 Chuyển từ hệ thống chuyển trạng thái sang Ôtômat Buchi .................. 64 3.7 Tích chập của hai Ôtômat Buchi........................................................... 66 3.7.1 Ôtômat Buchi dẫn xuất .................................................................. 66 3.7.2 Nguyên tắc thực hiện ..................................................................... 66 3.8 Kiểm tra tính rỗng của ngôn ngữ được đoán nhận bởi Ôtômat Buchi.. 68 3.9 Kết luận chương .................................................................................... 70 CHƯƠNG 4: XÂY DỰNG HỆ THỐNG ĐỂ KIỂM TRA MÔ HÌNH PHẦN MỀM ............................................................................................................... 72 4.1 Giới thiệu về mô hình SPIN.................................................................. 72 4.2 Cấu trúc SPIN ....................................................................................... 73 4.3 Ngôn ngữ PROMELA........................................................................... 76 4.3.1 Giới thiệu chung về Promela.......................................................... 76 4.3.2 Mô hình một chương trình Promela............................................... 77 5 4.3.5 Tiến trình khởi tạo.......................................................................... 78 4.3.6 Khai báo biến và kiểu..................................................................... 78 4.3.7 Câu lệnh trong Promela.................................................................. 79 4.3.8 Cấu trúc atomic .............................................................................. 81 4.3.9 Các cấu trúc điều khiển thường gặp............................................... 81 4.3.9.1 Câu lệnh điều kiện IF .............................................................. 81 4.3.9.2 Câu lệnh lặp DO...................................................................... 82 4.3.10 Giao tiếp giữa các tiến trình......................................................... 83 4.3.10.1 Mô hình chung ...................................................................... 83 4.3.10.2 Giao tiếp giữa các tiến trình kiểu bắt tay .............................. 85 4.4 Cú pháp của LTL trong SPIN ............................................................... 86 4.5 Minh hoạ kiểm tra mô hình phần mềm với SPIN ................................. 86 KẾT LUẬN ..................................................................................................... 95 TÀI LIỆU THAM KHẢO............................................................................... 98 6 DANH MỤC CÁC TỪ VIẾT TẮT Số Từ viết tắt Giải nghĩa TT OBDD 1 2 BDD Ordered Binary Decision Diagrams Binary Decision Diagrams 3 LTL Linear Temporal Logic 4 LTS Label Transition System 5 BTL Branching Temporal Logic 6 DFS 7 SPIN Depth First Search Simple Promela Interpreter 8 PROMELA Protocol / Process Meta Language 7 DANH MỤC CÁC HÌNH VẼ, ĐỒ THỊ Hình vẽ, đồ thị Trang Hình 1.1 Mô hình xác thực phần mềm 10 Hình 1.2 Mô hình logic thời gian 11 Hình 1.3 Mô hình của kiểm tra mô hình phần mềm 14 Hình 1.4 Kiểm tra mô hình phần mềm gắn với vòng đời phần 17 mềm Hình 2.1: Các cách tiếp cận kiểm tra mô hình phần mềm 19 Hình 2.2 Các bước cơ bản trong kiểm tra mô hình phần mềm 19 Hình 2.3: Các cách tiếp cận để điều khiển sự bùng nổ không 20 gian trạng thái Hình 2.4 : Cây quyết định nhị phân theo bậc và OBDD cho (a 21 ∧b)∨(c∧d) với thứ tự a - Xem thêm -