Luận án tiến sĩ về kiểm chứng phần mềm qua biểu đồ tuần tự - Lê Chí

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ LÊ CHÍ LUẬN LUAN AN TIEN Si NGANH CONG NGHE THONG TIN Hà Nội — 2018 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ LÊ CHÍ LUẬN Chuyên ngành: Kỹ thuật Phan mềm Mã số: 62.03 LUẬN ÁN TIEN SI NGANH CÔNG NGHỆ THONG TIN NGUOI HUONG DAN KHOA HOC: 1. Pham Ngoc Hùng 2. Hồ Sĩ Dam Hà Nội - 2018 Mục lục Trang Chương 1. Đặt vấn dé.

cece cree ence een nhu ng kh ng vn va 1 1. Các đóng góp chính của luận ấn. B6 cục của luận ấn. KIÊN THUC NEN TẢNG.

Mô hình của thành phần phần mềm. Hệ thống chuyển trạng thái được gán nhãn. Vet ccc cence cence tee beet e bene k vn k vs. Phép ghép nối song song.

LTS an toàn, thuộc tính an toàn, tính thỏa mãn và LTS lỗi. Ôtômát hữu hạn trạng thái đơn định. OtOmat VàO/Tâ. cece cece tee e eee cette teen enna 21 2.

Kiểm chứng giả định - đảm bao (Assume - Guarentee Verification) 22 2. Lý thuyết giả định.cc c2 teen eee 22 2. Bộ công cụ LTSA (Labelled Transition Systems Analyzer). ccc cece eee e eee e beeen nh nà va 24 Chương 3.

PHƯƠNG PHÁP SINH MO HÌNH VA KIEM CHUNG TÍNH DUNG DAN THIET KE CHO CAC PHAN MEM DUA TREN THÀNH PHAN 2. ccccccecc cece teense cease enseeeneeenas 25 3. Q0 Q Q n n ng een ee ete x. Các nghiên cứu liên quan.

Phân tích biểu đồ tuần tự. Định dạng của đầu vào biểu đồ tuần tự. Sinh biểu thức chính quy cho phân đoạn Option. Sinh biểu thức chính quy cho phân đoạn Break/Critical/Strict.

Sinh biểu thức chính quy cho phân đoạn Alternative. Sinh biểu thức chính quy cho phân đoạn Loop. Sinh biểu thức chính quy cho phân đoạn Consider. Sinh biểu thức chính quy cho phân đoạn Ïgnore.

Sinh biểu thức chính quy cho phan đoạn Parallel và Sequencing 37 3. Sinh biểu thức chính quy cho biểu đồ tuần tự. Sinh mô hình cho thành phần sử dụng thuật toán CNNFA. Tổng quan về CNNEA.

Sinh biểu diễn CNNFA cho các biểu thức chính quy thành phan 40 3. Phương pháp duyệt biểu thức chính quy. Sinh các mô hình cho các thành phần. Tối wu hóa mô hình.

Ví dụ sinh mô hình cho thành phần phần mềm bằng thuật toán CNNEA. nen ent ng ng kh kg ng vn và 48 3. Kiểm chứng tính đúng đắn của biểu đồ tuần tự. Công cụ hỗ trợ và thực nghiệm.

Kiến trúc công CỤ. 22222022 ete eee eee eens 57 3. Thực nghiệm và đánh giá phần sinh mô hình. Thực nghiệm va đánh giá phần kiểm chứng giả định - đảm bảo 61 3.

cece bennett eee ky. cece cece eee eee cece nen ng ng kh va 63 Chương 4. PHƯƠNG PHÁP SINH MO HÌNH VÀ KIEM CHUNG TÍNH DUNG DAN CUA CÁC BIÊU DO TUAN TU UML 2.0 SỬ DUNG ÔTÔMÁT VÀO/RA. Q0 ng nh vn ene e eee x xà 65 4.

Các nghiên cứu liên quan. Phân tích biểu đồ tuần tự thành các khối đơn. Định dạng của đầu vào biểu đồ tuần tự. Phân tích biểu đồ tuần tự thành các khối đơn.

Sinh mô hình từ các khối đơn của biểu đồ tuần tự. Thuật toán xác định tập các luật chuyển 5 cho ôtômát vao/ra từ khối đơn không chứa phân đoạn nào. Thuật toán xác định tập các luật chuyển 6 cho ôtômát vao/ra từ khối đơn chỉ chứa phân đoạn ÓpfiØn. Thuật toán xác định tập các luật chuyển 6 cho ôtômát vao/ra từ khối đơn chỉ chứa phân đoạn AlfernaliU€.

Thuật toán xác định tập các luật chuyển 6 cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn ÙoØ0Đ. Thuật toán xác định tập các luật chuyển 6 cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Öreak. Thuật toán xác định tập các luật chuyển 6 cho ôtômát vao/ra từ khối đơn chỉ chứa phân đoạn Parallel. Thuật toán xác định tập các luật chuyển 6 cho ôtômát vao/ra từ khối đơn chỉ chứa phân đoạn 6Si7iCE.

Thuật toán xác định tập các luật chuyển 6 cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn r?fieal. Thuật toán xác định tập các luật chuyển ð cho ôtômát vào /ra từ khối đơn chỉ chứa phân đoạn Consiđer. Thuật toán xác định tập các luật chuyển 6 cho ôtômát vào/ra từ khối đơn chỉ chứa phân đoạn Ïgnore. Xây dựng ôtômát vào/ra cho đối tượng từ biểu đồ tuần tự.

Sinh đặc tả Promela từ Ôtômát vào/ra. Công cụ hỗ trợ và thực nghiệm. Kiến trúc công GỤ. occ cece cece cece eee eee e bebe bene eee xxx v2 94 4.

cece cece cence eben ene beeteteteteeenenens 94 Chương 5. MOT SỐ CẢI TIEN PHƯƠNG PHAP KIEM CHUNG GIA ĐỊNH - DAM BẢO. Giới thi6u one ng ene ng kg nee ens 96 5. Các nghiên cứu liên quan.

Phương pháp sinh gia định sử dung thuật toán L*. HQ Q Q Q Q Q n n ng ng n1 v2 100 5. Sinh giả định sử dụng thuật toán Ƒ*. Cập nhật bang quan sất.

Cải tiến phương pháp sinh giả định sử dụng thuật toán L*. Một ví dụ về lặp vô hạn. Cải tiến về phân tích phan ví dụ. Cải tiến giảm số truy vấn thành viên.

Công cụ hỗ trợ và thực nghiệm. ng HH nh sa 108 5. Phương pháp sinh giả định nhỏ nhất cục bộ. Kỹ thuật cải tiến cho trả lời truy vấn thành viên.

Sinh giả định nhỏ nhất cục bộ. Cải tiến kỹ thuật cập nhật cho bảng quan sát. Phân tích kết quả truy vẫn ứng viên. Ví dụ minh họa.

Công cụ hỗ trợ và thực nghiệm. HH ng sa 118 5. 0Q 2Q ence beeen ene nu eees 119 Chương 6. Các kết quả đạt được.

Những hạn chế và hướng nghiên cứu tiếp theo. 122 1V Danh sách hình vẽ 1.1 Các đóng góp chính của luận ấn.1 Một hệ thống chuyển trạng thái được gn nhãn.2 Hệ chuyển trạng thái được gan nhãn không đơn định.3 Hệ chuyển trạng thái được gan nhãn đơn định.4 Ghép nối song song hai UT§.5 LTS của thuộc tính p và LTS lỗi tương Ứng.6 Xây dựng LTS ghép nối song song Input||Output||perr.7 Minh họa ôtômát M được mô tả ở Ví dụ 2.8 Phương pháp chuyển một ôtômát M thành LTS M'.1 Biểu diễn của biểu đồ tuần tự bởi tệp XML.2 Biểu đồ tuần tự của thành phần M¡ trong hệ thống Mod2.3 Biểu đồ tuần tự của thành phần M2 trong hệ thống Mod2.4 Tép XML sau khi chuẩn hóa mô tả dit liệu của biểu đồ tuần tự Hinh LH eee 34 3.5 Biểu diễn CNNFA của ôtômát đuôi Mix thành phan J|K theo công thỨc 3.6 Biểu diễn CNNFA của ôtômát đuôi M7, thành phần J.K theo công thức 3Ä.7 Biểu diễn CNNFA của ôtômát đuôi Mf. thành phần J* theo công thite 5 1.8 Ôtômát đuôi dang nén theo thuật toán CNNFA của thành phần M, trong hệ thống Mod2.9 Ôtômát khong đơn định theo thuật toán CNNFA.10 Ôtômát tối thiểu cuối cùng sau khi đã tối thiểu hóa.11 LTS [cex] được tao ra từ phan ví dụ cex.12 Quá trình sinh giả định sử dụng thuật toán 7*.13 Kiến trúc công cụ sinh mô hình và kiểm chứng tính đúng đắn thiết kế cho các phần mềm dựa trên thành phan.1 Biểu diễn của biểu đồ tuần tự bởi tệp XML.2 Biểu đồ tuần tự của hệ thống đặt vé.3 Dinh dạng XML của biểu đồ tuần tự.4 Kiến trúc công cu sinh biểu diễn PROMELA và quy trình kiểm chứng biểu đồ tuần tu.1 Tương tác giữa Learner va Teacher trong quá trình sinh giả định.2 Kiểm tra tính thỏa mãn của mỗi ứng viên tại lần lặp thứ¿.3 Cho hệ thống M = Mj||Mz và thuộc tínhp.4 Các ứng viên tương ứng cho T1, To, T3, và T1.5 Mối quan hệ giữa L(A) và L(Awy).6 Hệ thống minh họa.7 Sinh giả định bởi phương pháp trong [25] và phương pháp đề xuất.8 Kiểm chứng Tl5SSTRONGEST = As||Aorg bang LTSA.9 Kết quả kiểm chứng ISsTRONGEST = As||Aorg bang LTSA. 117 vi Danh sách bảng 3.1 Sinh biểu thức chính quy cho các thành phan trong hệ thống Mod2 .2 Dữ liệu thực nghiệm .3 Kết quả thực nghiệm so sánh phương pháp đề xuất với phương pháp Thompson.4 Kết quả thực nghiệm so sánh phương pháp đề xuất với L*-based method .5 Thời gian sinh các biéu thức chính quy.6 Thời gian sinh mô hinh.7 Kết quả sinh giả định.1 Biểu diễn các thành phần của EDTFA trong PROMELA.2 So sánh kết quả đề xuất va kết qua nghiên cứu trong [90].3 So sánh kết quả của công cụ đề xuất và phương pháp trong [90] .4 Kết quả thực nghiệm với một số biểu đồ tuần tự.1 Bang quan sát 7,7,7», và T¡ trong khi kiểm chứng M.2 Môi trường thực nghiệm .3 Kết quả thực nghiệm .4 Môi trường thực nghiệm .9 Kết quả thực nghiệm.

S Q 118 vii Thuật ngữ và từ viết tắt Từ viết tắt Từ gốc Giai nghia - Tam dich AGV Assume - Guarentee Verifica- Kiểm chứng giả định - đảm tion bảo CBSD Component-based Software | Phát triển phần mềm dựa Development trên thành phần CBSE Component-based Software | Công nghệ phần mềm dựa Enginnering trén thanh phan cex Counter Example Phan vi du CNNFA Compressed NNFA Tên gọi của một phương pháp chuyển biểu thức chính quy về ôtômát hữu hạn không đơn định CP List Check Point List Danh sách điểm kiểm soát DEA Deterministic Finite State Au- | Ôtômát hữu hạn trang thái tomata đơn định EDTEA Event Deterministic Finite Au- | Ôtômát hướng sự kiện tomata EFSM Extended Finite State Machine | Máy hữu han trang thái mở rộng FA Finite State Automata Ôtômát hữu han trạng thái FSP Finite State Process Tiến trình hữu han trạng thái 1/O Au- | Input/ Output Automata Otomat vao/ra tomata LTL Linear Temporal Logic Logic thời gian tuyến tính LTS Labeled Transition System Hệ thống chuyển trạng thái được gán nhãn LISA Labelled Transition Systems | Công cụ hỗ trợ kiểm chứng Analyzer với đặc tả là hệ thống chuyển trạng thái được gán nhãn MQ Result | Membership Query Result Kết qua truy vấn thành viên MYNNFA McNaughton/Yamada NNFA_ | Tên gọi của một loại ôtômát hữu hạn không đơn định theo McNaughton và Ya- mada nas Non-Accepting States Cac trang thai khong két viii Từ viết tắt Từ gốc Giai nghia -Tam dich NFA Nondeterministic Finite Au- Ôtômát hữu han khong don tomata dinh NNFA Normal Nondeterministic Fi- | Tên gọi của một loại 6t6mat nite Automata hữu hạn không đơn định OT Observation Table Bang quan sat PML Process Meta Language or Pro- | Ngon ngữ kiểm chứng mô tocol Meta Language hinh do Gerard J. Holzmann dé xuat SPIN Simple Promela Interpreter Công cu kiểm chứng tinh đúng đắn của mô hình phần mềm UFSM Unknown Finite State Machine | Máy hữu han trạng thai không xác định UML Unified Modeling Language Ngôn ngữ mô hình hóa thống nhất UNSAT Unsatisfiable Không thỏa mãn XML eXtensible Markup Language | Ngôn ngữ đánh dấu mở rộng ix Lời cam đoan Tôi xin cam đoan day là công trình nghiên cứu do tôi thực hiện dưới sự hướng dẫn của PGS. Phạm Ngọc Hùng và PGS.