- Lời cảm ơn. - Trước tiên, tôi muốn gửi lời cảm ơn sâu sắc nhất đến thầy giáo, TS. - Phạm Ngọc Hùng, người đã tận tình chỉ bảo và hướng dẫn tôi trong suốt quá trình học tập, nghiên cứu và thực hiện luận văn tốt nghiệp.. - Tôi xin bày tỏ lời cảm ơn sâu sắc đến những thầy cô giáo đã giảng dạy trong hai năm qua, đã tạo cho tôi những điều kiện thuận lợi để học tập và nghiên cứu tại trường Đại Học Công Nghệ.. - Tôi xin chân thành cảm ơn GS. - Giáo sư đã nhiệt tình giải đáp các vấn đề mà tôi gặp phải trong quá trình thực hiện luận văn.. - Xin gửi lời cảm ơn tới bạn Nguyễn Bảo Ngọc, người đã giúp đỡ tôi các vấn đề kỹ thuật liên quan tới luận văn cũng như các vấn đề khác trong cuộc sống.. - Cuối cùng, tôi xin gửi lời cảm ơn chân thành tới phòng thí nghiệm công nghệ phần mềm Toshiba. - Tôi xin chân thành cảm ơn. - Tôi xin cam đoan luận văn này là công trình nghiên cứu của riêng tôi. - Các số liệu, kết quả được trình bày trong luận văn là hoàn toàn trung thực và chưa từng được công bố trong bất kỳ một công trình nào khác. - Ngoại trừ các tài liệu tham khảo này, luận văn hoàn toàn là công việc của riêng tôi.. - Assume-Guarantee Tool (AGTool) là một công cụ sinh giả định, có ý nghĩa quan trọng trong việc giải quyết bài toán "bùng nổ không gian trạng thái". - của phương pháp kiểm chứng mô hình. - Hiện tại, AGTool là một trong những công cụ tiềm năng trong việc hỗ trợ kiểm chứng phần mềm hướng thành phần. - Thay vì kiểm chứng trên toàn bộ hệ thống, công cụ này chia bài toán kiểm chứng thành các bài toán nhỏ hơn ứng với các thành phần phần mềm và kiểm chứng các thành phần này một cách riêng biệt. - Tuy nhiên, công cụ AGTool còn tồn tại nhiều hạn chế để có thể ứng dụng vào trong thực tế và tương tác với các công cụ kiểm chứng phần mềm khác như LTSA. - Với mục đích tăng khả năng tương tác với các công cụ kiểm chứng phần mềm khác, luận văn nghiên cứu sử dụng các tiến trình hữu hạn trạng thái (FSP) thay thế cho kiểu dữ liệu LF của AGTool. - Mục tiêu của luận văn là đưa ra phương pháp chuyển đổi qua lại giữa các kiểu dữ liệu LF-FSP và ứng dụng vào công cụ kiểm chứng AGTool. - Luận văn đề xuất một thuật toán để chuyển từ LF sang FSP. - Dựa trên công cụ LTSA của tác giả Jeff Magee, luận văn đã tiến hành tích hợp giữa AGTool và LTSA để chuyển đổi từ FSP sang LF. - Những cải tiến này sẽ giúp AGTool trở thành một công cụ hiệu quả và tốt hơn trong thực tế.. - AGTool Assume-Guarantee Tool Công cụ hỗ trợ kiểm chứng đảm bảo giả định. - Công cụ đồ họa hỗ trợ kiểm chứng đảm bảo giả định LTS Labeled Transition System Hệ thống dịch chuyển được. - MC Model Checking Kiểm chứng mô hình. - Kiểm chứng đảm bảo giả định. - Công cụ kiểm chứng hệ thống tương tranh. - 2.7.1 Định nghĩa FSP. - 2.7.5 Định nghĩa tiến trình. - 4 Chuyển đổi giữa các dạng biểu diễn của LTS 28 4.1 Chuyển đổi FSP sang LF. - 4.2 Chuyển đổi LF sang FSP. - 2.1 Ví dụ của LTS. - 2.3 Ví dụ của LF. - 2.4 Ví dụ của FSP. - 2.7 Ví dụ định nghĩa hằng số. - 2.8 Ví dụ định nghĩa danh sách đối số. - 2.9 Định nghĩa FSP. - 2.10 Định nghĩa các định danh. - 2.11 Định nghĩa các chữ hoa, thường. - 2.12 Định nghĩa nhãn hành động. - 2.13 Định nghĩa tập các nhãn hành động. - 2.14 Định nghĩa Const, Range, Set. - 2.15 Định nghĩa tiến trình. - 2.16 Định nghĩa tiến trình địa phương. - 2.17 Định nghĩa thành phần tuần tự. - 2.18 Định nghĩa thành phần tuần tự. - 2.19 Định nghĩa tham số. - 2.20 Định nghĩa phép gán lại nhãn. - 2.21 Định nghĩa phép ẩn. - 2.22 Định nghĩa Property. - 2.24 Định nghĩa Menu. - 2.25 Định nghĩa biểu thức. - 2.26 Định nghĩa biểu thức (tiếp. - 2.27 Định nghĩa biểu thức (tiếp. - 2.28 Ví dụ khai báo hàm. - 2.29 Ví dụ gọi hàm. - 2.30 Ví dụ hàm mức cao. - 2.31 Ví dụ hàm nặc danh. - 2.32 Ví dụ hàm đệ quy. - 2.34 Ví dụ so sánh mẫu. - 2.36 Ví dụ tập tin đặc tả từ vựng. - 3.1 Mô hình công cụ kiểm chứng AGTool. - 3.2 Thành phần đầu vào của AGTool. - 4.2 Cấu trúc thành phần chuyển đổi từ FSP sang LF. - 4.5 Cấu trúc thành phần chuyển đổi từ LF sang FSP. - 5.3 Ví dụ FSP đầu vào của AGTool. - 5.4 LTS của thành phần M 1. - URL http://portal.acm.org/citation.cfm?id . - URL http://portal.acm.org/. - URL http://portal.acm.org/citation.cfm?. - doi: http://dx.doi.org/10.. - URL http://dx.doi.org/10.1109/KSE.2010.18. - Xây dựng giao diện cho công cụ agtool. - Chuyển đổi giữa các phương pháp biểu diễn của lts và ứng dụng cho công cụ kiểm chứng phần mềm. - doi: http://doi.acm.org/10.1145/. - URL http://doi.acm.org . - Assume-guarantee testing. - doi: http://doi.acm.org