e_nhin_ji_anh
New Member
Download miễn phí Luận văn 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
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
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 TemporalLogic - 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
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
Để tải bản Đầy Đủ của tài liệu, xin Trả lời bài viết này, Mods sẽ gửi Link download cho bạn sớm nhất qua hòm tin nhắn.
Ai cần download tài liệu gì mà không tìm thấy ở đây, thì đăng yêu cầu down tại đây nhé:
Nhận download tài liệu miễn phí
Tóm tắt nội dung tài liệu:
thống. Một vấn đề nữa đó là những trạng thái củacác hệ thống con chỉ được thoả mãn chỉ khi các giả định được đặt ra trên môi
trường đó. Một cách tiếp cận cho vấn dề này là sử dụng giao diện các tiến
trình để mô hình hoá môi trường của các hệ thống con. [2]
Một số lượng lớn các nghiên cứu đều dành cho xác thực kết cấu, đưa
lại những hi vọng khả quan về việc ngăn chặn sự bùng nổ không gian trạng
thái. Giải thuật rút gọn cục bộ có thể coi như một phương pháp xác thực kết
cấu đơn giản vì nó sẽ chứng minh các thuộc tính của hệ thống tổng thể bằng
cách kiểm tra xem nó có thoả mãn một số các thành phần của hệ thống. Thuận
lợi của việc rút gọn cục bộ đó là nó có thể tự động được.
Nhìn chung, đó là một nhiệm vụ phức tạp để phân rã các thuộc tính của
một hệ thống tổng thể thành các thuộc tính cục bộ của các thành phần của hệ
thống. Hơn nữa, nó phải chứng minh rằng sự phân rã đó là đúng đắn, đó là:
phải thoả mãn các thuộc tính cục bộ của các hệ thống con và các thuộc tính
tổng thể của hệ thống. Cách tiếp cận này được hỗ trợ bởi các công cụ tự động
ở mức độ cao để được sử dụng một cách rộng rãi bởi các kỹ sư phần mềm.
Theo các kết quả nghiên cứu, tìm ra một heuristic có ích để quyết định sự
36
phân rã các thuộc tính của hệ thống tổng thể thành các thuộc tính cục bộ của
các hệ thống con là một trong những vấn đề mở trước tiên của lĩnh vực này.
2.6 KẾT LUẬN CHƯƠNG
Để kiểm tra mô hình phần mềm, các kỹ thuật đưa ra đều tuân theo một
nguyên tắc chung đó là phải trừu tượng hoá mô hình hệ thống và thuộc tính hệ
thống cần thoả mãn. Sau đó, sử dụng bộ kiểm tra mô hình để kiểm tra xem hệ
thống có thoả mãn thuộc tính đó hay không. Nếu thoả mãn, đưa ra thông báo
thành công, nếu không thoả mãn, đưa ra các vết lỗi để thiết kế lại. Điểm khác
nhau cơ bản giữa 4 kỹ thuật đề xuất: biểu diễn ký hiệu, duyệt nhanh, rút gọn,
xác thực kết cấu đó là cách xử lý để tránh sự bùng nổ không gian trạng thái
của hệ thống. Trong 4 kỹ thuật trên, điều khiển không gian trạng thái hiệu quả
nhất là kỹ thuật duyệt nhanh (On the fly). Bằng cách thức sử dụng hàm băm
để lưu trữ toàn bộ không gian trạng thái, nhưng quá trình duyệt và tìm kiếm
trạng thái lại rất nhanh. Mặt khác kỹ thuật duyệt nhanh không yêu cầu phải
lưu trữ các chuyển trạng thái, sử dụng kỹ thuật bộ nhớ cache để tiết kiệm
dung lượng bộ nhớ, tăng tốc độ tìm kiếm. Đồng thời với việc dựa trên các ưu
điểm lưu trữ của kỹ thuật duyệt nhanh, luận văn sẽ đi sâu nghiên cứu tìm ra
giải thuật để giải quyết bài toán kiểm tra mô hình phần mềm sử dụng kỹ thuật
duyệt nhanh sẽ được đề cập ở chương 3 tiếp theo.
37
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
3.1. BÀI TOÁN KIỂM TRA MÔ HÌNH PHẦN MỀM
Bài toán đặt ra: Cho một hệ thống chuyển trạng thái T và một thuộc tính f.
Cần kiểm tra xem hệ thống T có thoả mãn thuộc tính f hay không?
Ý tưởng giải quyết: [5]
- Chuyển đổi hệ thống chuyển trạng thái T về dạng Ôtômat Buchi, ký
hiệu AT
- Đặc tả thuộc tính f dưới dạng Logic thời gian tuyến tính (LTL – Linear
Temporal Logic)
- Lấy phủ định của thuộc tính LTL f là ¬f và chuyển ¬f sang dạng
Ôtômat Buchi A¬f
- Kiểm tra giao của các ngôn ngữ được đoán nhận bởi AT và A¬f có là
rỗng hay không, tức là:
o L(AT) ∩ L(A¬f) = ∅
o Nếu L(AT) ∩ L(A¬f) ≠ ∅ chứng tỏ hệ thống chuyển trạng thái T
đã vi phạm thuộc tính f, đưa ra vết lỗi.
- Chú ý:
o L(AT) ∩ L(A¬f) = ∅ nếu và chỉ nếu L(AT) ⊆ L(A¬f)
o Cho hai Ôtômat Buchi AT và A¬f, xây dựng tích chập của hai
Ôtômat AT × A¬f như sau:
L(AT × A¬f ) = L(AT) ∩ L(A¬f)
38
o Sau đó, ta kiểm tra ngôn ngữ được đoán nhận bởi Ôtômat Buchi
AT × A¬f có bằng rỗng (empty) hay không.
3.2. MÔ HÌNH HOÁ HỆ THỐNG PHẦN MỀM
3.2.1 Vấn đề đặt ra
Ta luôn mong muốn tìm được cách biểu diễn mô hình phần mềm để đáp ứng
các vấn đề đặt ra:
Có khả năng biểu diễn tuơng tranh: Làm thế nào để mô hình hoá các
hệ thống trong đó phép chuyển trạng thái có thể được thực hiện bởi các
tiến trình khác nhau, các tiến trình tương tranh. Chuyển trạng thái có
thể chỉ là một phép chuyển tại một thời điểm hay có thể có rất nhiều
khả năng chuyển trạng thái tại một thời điểm.
Các phép chuyển được mô tả ở mức độ nào là thích hợp nhất?
Mỗi phép chuyển được mô tả bởi một vài câu lệnh
Mỗi phép chuyển được mô tả bởi một phép gán hay một xác
định chắc chắn và cụ thể
Mỗi phép chuyển được mô tả bởi một câu lệnh mã máy
Mỗi phép chuyển được mô tả bởi một sự thay đổi vật lý
Lựa chọn mô hình thực thi: Mô hình tuyến tính hay mô hình phân
nhánh?
Mô hình tuyến tính: Tập hợp tất cả các phép thực thi hoàn chỉnh
(còn gọi là vết) của hệ thống
Mô hình phân nhánh: Phân biệt các cách khác nhau tại mọi điểm
trong khi thực thi hệ thống. oftware Model Checking Summer term 2006 4
Các trạng thái hệ thống: Sử dụng các trạng thái toàn cục hay cục bộ
cho các hệ thống tương tranh hay phân tán?
39
Các trạng thái toàn cục: thể hiện miêu tả tức thì của toàn bộ hệ
thống.
Các trạng thái cục bộ: Thể hiện phép gán các giá trị cho các biến
của một tiến trình xử lý đơn lẻ.
Trạng thái hệ thống: Trạng thái để mô tả hệ thống một cách hình thức,
để cung cấp một số thông tin tại một thời điểm bất kỳ trong quá trình thực thi
hệ thống.
Trạng thái hệ thống sử dụng một trong các thành phần sau: các thực thể
trừu tượng như đợi tín hiệu vào (waiting for input) hay đang chạy (running),
giá trị của các biến chương trình, giá trị của các bộ đếm chương trình, nội
dung của dãy các thông điệp, các cờ tiến trình, thông tin lập lịch…
Từ đó, yêu cầu phải có những mô hình toán học để làm cơ sở định
nghĩa ngữ nghĩa của logic thời gian, đó chính là hệ thống đánh nhãn dịch
chuyển (LTS – Label Transition System)
3.2.2. Hệ thống đánh nhãn dịch chuyển
3.2.2.1 Các định nghĩa
Với mục đích thoả mãn các vấn đề đặt ra như trên, ta sẽ biểu diễn các
hành vi của hệ thống bằng đồ thị hữu hạn hay vô hạn trong đó các nút là các
trạng thái của hệ thống và các cạnh để biểu thị sự dịch chuyển trạng thái.
Định nghĩa hệ thống đánh nhãn dịch chuyển: [1] Hệ thống đánh nhãn dịch
chuyển bao gồm bộ bốn : K = (S, S0, L, →)
trong đó:
S: tập các trạng thái
S0: tập các trạng thái khởi đầu
L: tập các nhãn
→: một quan hệ dịch chuyển ⊆ S ×L×S
40
Nếu (s, l, s’) ∈ → thì sẽ viết là: s ⎯→l s’
Định nghĩa phép thực thi trong LTS: [1]
Một phép thực thi của LTS (S, S0, L, →) là một đường đi vô hạn hay hữu
hạn có dạng:
...3210 321 ssss lll ⎯→⎯⎯→⎯⎯→⎯
với s0 ∈ S0 và (si, li, si+1) ∈ → với mọi i
Chú ý:
- Các trạng thái có thể được đánh nhãn bằng một tập các biến, mỗi biến
biểu thị cho một thuộc tính trạng thái...