Chương 1: Giới thiệu. 1 Chương 2: Phương pháp phân tích biểu đồ tuần tự nhằm xây dựng các mô hình đặc tả. Biểu đồ tuần tự UML2. Phương pháp phân tích đối tượng của biểu đồ tuần tự thành các khối đơn.
Phương pháp sinh ôtômat vào/ra từ các khối đơn của biểu đồ tuần tự. Trường hợp khối đơn không chứa phân đoạn nào. Trường hợp khối đơn chứa một phân đoạn Option. Trường hợp khối đơn chứa một phân đoạn Alternative.
Trường hợp khối đơn chứa một phân đoạn Loop. Trường hợp khối đơn chứa một phân đoạn Break. Trường hợp khối đơn chứa một phân đoạn Parallel. Trường hợp khối đơn chứa một phân đoạn Strict.
Trường hợp khối đơn chứa một phân đoạn Critical. Trường hợp khối đơn chứa một phân đoạn Consider. Trường hợp khối đơn chứa một phân đoạn Ignore. Phương pháp xây dựng ôtômat vào/ra cho đối tượng của biểu đồ tuần tự.
28 Chương 3: Công cụ sinh ôtômat vào/ra từ biểu đồ tuần tự. 32 LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Giới thiệu về công cụ. Bài toán đặt chỗ.
Bài toán máy thanh toán ở siêu thị. 46 Chương 4: Phương pháp kiểm chứng tính đúng đắn của biểu đồ tuần tự qua ôtômat vào/ra. Kiểm chứng tính đúng đắn của biểu đồ tuần tự qua ôtômat vào/ra. Áp dụng phương pháp kiểm chứng với trường hợp bài toán đặt chỗ.
48 Chương 5: KẾT LUẬN. 50 TÀI LIỆU THAM KHẢO. 51 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com iii LỜI CẢM ƠN Trước tiên tôi xin dành lời cảm ơn chân thành và sâu sắc đến hai thầy giáo, TS. Trịnh Thanh Bình và TS.
Phạm Ngọc Hùng – những người đã hướng dẫn, khuyến khích, chỉ bảo và tạo cho tôi những điều kiện tốt nhất từ khi bắt đầu cho tới khi hoàn thành công việc của mình. Tôi xin dành lời cảm ơn chân thành tới các thầy cô giáo khoa Công nghệ thông tin, trường Đại học Công nghệ, ĐH QGHN đã tận tình đào tạo, cung cấp cho tôi những kiến thức vô cùng quý giá và đã tạo điều kiện tốt nhất cho tôi trong suốt quá trình học tập, nghiên cứu tại trường. Đồng thời tôi xin chân thành cảm ơn những người thân trong gia đình cùng toàn thể bạn bè đã luôn giúp đỡ, động viên tôi trong những lúc gặp phải khó khăn trong việc học tập và nghiên cứu chương trình thạc sĩ tại Đại học Công nghệ, ĐH QGHN. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com iv LỜI CAM ĐOAN Tôi xin cam đoan rằng luận văn thạc sĩ công nghệ thông tin “Phương pháp kiểm chứng tính đúng đắn của các biểu đồ tuần tự UML 2.0” là công trình nghiên cứu của riêng tôi, không sao chép lại của người khác.
Trong toàn bộ nội dung của luận văn, những điều đã được trình bày hoặc là của chính cá nhân tôi hoặc là được tổng hợp từ nhiều nguồn tài liệu. Tất cả các nguồn tài liệu tham khảo đều có xuất xứ rõ ràng và hợp pháp. Tôi xin hoàn toàn chịu trách nhiệm và chịu mọi hình thức kỷ luật theo quy định cho lời cam đoan này. Hà Nội, ngày … tháng … năm 2015 Trần Quốc Nam LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com v DANH MỤC THUẬT NGỮ VIẾT TẮT STT Từ viết tắt Từ đầy đủ Ý nghĩa 1 DFA Deterministic Finite Automata Ôtômat hữu hạn trạng thái 2 I/O Automata Input/Output Automata Ôtômat vào/ra.
3 FG Fragment Phân đoạn 4 SD Sequence Diagram Biểu đồ tuần tự 5 OP Interaction Operand Toán hạng tương tác LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com vi DANH MỤC HÌNH VẼ Hình 2. Phân đoạn Loop. Phân đoạn Alt. Phân đoạn Par và ví dụ thứ tự thực hiện.
Phân đoạn Opt. Phân đoạn Break. Phân đoạn Seq. Phân đoạn Strict.
Phân đoạn Ignore. Phân đoạn Consider. Phân đoạn Critical. Phân đoạn Neg.
Phân đoạn Assert. Khối đơn gồm một phân đoạn opt. Khối đơn không chứa phân đoạn và ôtômát cho đối tượng User. Khối đơn chỉ chứa một phân đoạn Option và ôtômat cho đối tượng User.
Khối đơn chỉ chứa một phân đoạn Alternative và ôtômat cho đối tượng User. Khối đơn chỉ chứa một phân đoạn Loop và ôtômat cho đối tượng User. Khối đơn chỉ chứa một phân đoạn Break và ôtômat cho đối tượng User. Khối đơn chỉ chứa một phân đoạn Paraller và ôtômat cho đối tượng Admin.
Khối đơn chỉ chứa một phân đoạn Strict và ôtômat cho đối tượng User. Khối đơn chỉ chứa một phân đoạn Critical và ôtômat cho đối tượng User.25 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com vii Hình 2. Khối đơn chỉ chứa một phân đoạn Consider và ôtômat cho đối tượng User. Khối đơn chỉ chứa một phân đoạn Ignore và ôtômat cho đối tượng User.
Kiến trúc của công cụ. Biểu đồ lớp của công cụ. Khối Loop đơn giản. Đầu ra của công cụ với khối Loop đơn giản.
Biểu đồ tuần tự xử lý đặt chỗ. Đầu ra mong muốn cho đối tượng Oder. Đầu ra mong muốn cho đối tượng Ticket. Đầu ra mong muốn cho đối tượng Account.
Biểu đồ tuần tự máy thanh toán ở siêu thị. Đầu ra mong muốn cho đối tượng Customer. Đầu ra mong muốn cho đối tượng Cashier. Đầu ra mong muốn cho đối tượng Card Processor.
Đầu ra mong muốn cho đối tượng Cash Register .44 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com viii DANH MỤC BẢNG Bảng 5. Mô phỏng kiểm chứng thuộc tính P với bài toán đặt chỗ.49 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 1 Chƣơng 1: Giới thiệu Đảm bảo chất lượng là một vấn đề quan trọng và tiêu tốn chi phí cao trong quá trình phát triển phần mềm. Tự động hóa quá trình đảm bảo chất lượng là tiêu chí hướng tới của các doanh nghiệp nhằm giảm đi chi phí phát triển ngay từ khâu thiết kế. Ngoài ra, đối với những sản phẩm có yêu cầu chất lượng cao như hệ thống điều khiển máy bay, tàu ga, kỹ thuật quân sự, y tế v.
nhà đầu tư sẽ yêu cầu áp dụng các phương pháp hình thức nhằm đảm bảo tính đúng đắn của thiết kế trước khi triển khai. Giải pháp phố biến nhất hiện nay để giải quyết vấn đề trên là áp dụng các phương pháp kiểm chứng mô hình để tự động hóa quá trình kiểm chứng tính đúng đắn của thiết kế [2], [6], [9]. Để áp dụng những phương pháp này, ta cần phải xây dựng các mô hình đặc tả chính xác hành vi của hệ thống cần kiểm chứng [4], [10], [11]. Tuy nhiên, xây dựng mô hình cho các hệ thống phần mềm là một công việc khó khăn và tiềm ẩn nhiều lỗi.
Các nghiên cứu hiện tại hầu hết giả sử các mô hình này đã có và đúng đắn. Trong thực tế, giả định này rất khó để hiện thực, nhất là từ phía các công ty phát triển phần mềm. Hạn chế trên là một trong những nguyên nhân chính dẫn đến các phương pháp này khó áp dụng trong thực tế. Để giải quyết vấn đề nêu trên, một trong những hướng tiếp cận là sử dụng đầu vào cho các phương pháp kiểm chứng từ biểu đồ thiết kế UML.
Việc đưa ra phương pháp mô hình hóa biểu đồ UML, ở đây là biểu đồ tuần tự UML 2.0, giúp cho việc áp dụng các phương pháp kiểm chứng mô hình hoàn toàn có thể thực hiện được trong thực tế. Nghiên cứu hiện tại được đề cập trong [3] tập trung xây dựng một ôtômat cho cả biểu đồ tuần tự. Phương pháp này chỉ đảm bảo được các thuộc tính an toàn (safety properties) [7], kiểm tra các hành vi một cách tuần tự theo thời gian. Cách tiếp cận này không thể hiện được tính hướng đối tượng vốn có biểu đồ tuần tự là sự tương tác giữa các đối tượng với nhau, gửi và nhận các loại thông điệp, các điểm xuất phát và điểm đến của chúng, đặc biệt đối với các hệ thống tương tranh.
Vì vậy một cách khác ta cần bóc tách xây dựng ôtômat thể hiện hành vi của từng đối tượng trong mối quan hệ với các đối tượng khác từ đó ta có hành vi của hệ thống. Một cách tiếp cận để giải quyết vấn đề trên được đề xuất trong [5]. Ý tưởng chính của phương pháp này là xây dựng một ôtômat vào/ra (Input/Output Automata – I/O LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 2 Automata) [8] cho mỗi đối tượng của biểu đồ tuần tự. Ôtômat vào/ra là sự mở rộng của ôtômat hữu hạn trạng thái (Deterministic Finite Automata - DFA) [1].
Các trạng thái trong ôtômat vào/ra biễu diễn các ánh xạ từ hành vi tới các đối tượng trong biểu đồ tuần tự. Hàm chuyển trạng thái được biểu diễn bởi ánh xạ hai ngôi (điều kiện, hành vi) thể hiện sự tương tác giữa các đối tượng [5]. Luận văn tập trung vào xây dựng thuật toán và công cụ hiện thực hóa việc xây dựng ôtômat vào/ra cho các đối tượng trong biểu đồ tuần tự. Các mô hình ôtômat vào/ra này cùng với việc đưa vào các thuộc tính sẽ là đầu vào cho các công cụ kiểm chứng hỗ trợ ôtômat vào/ra nhằm kiểm chứng tính đúng đắn của thiết kế.
Phần còn lại của luận văn được cấu trúc như sau. Phương pháp sinh mô hình cho các đối tượng của biểu đồ tuần tự UML2.0 được giới thiệu trong chương 2. Chương này trình bày phương pháp bóc tách đối tượng của biểu đồ tuần tự thành các khối đơn, tiếp đó là phương pháp sinh ôtômat vào/ra từ các khối đơn của biểu đồ tuần tự và cuối cùng là phương pháp ghép nối các ôtômat vào/ra được sinh ra từ các khối đơn để được một ôtômat cho cả đối tượng. Chương 3 giới thiệu về công cụ thực nghiệm và kết quả thực nghiệm của phương pháp sinh ôtômat vào/ra cho các đối tượng của biểu đồ tuần tự được trình bày trong chương 2.
Chương 4 nghiên cứu phương pháp để kiểm chứng tính đúng đắn của biểu đồ tuần tự thông qua việc kiểm tra tính đúng đắn của các ôtômat vào/ra được sinh ra từ các đối tượng cùng các thuộc tính yêu cầu. Chương này nghiên cứu phương pháp mô phỏng sự tương tác giữa các ôtômat vào/ra từ các đối tượng, qua đó kiểm chứng tính đúng đắn của biểu đồ tuần tự đối với thuộc tính yêu cầu. Kết luận và định hướng phát triển cho luận văn được trình bày trong chương 5. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 3 Chƣơng 2: Phƣơng pháp phân tích biểu đồ tuần tự nhằm xây dựng các mô hình đặc tả Để áp dụng các phương pháp kiểm chứng tự động dựa trên mô hình, việc đầu tiên cần làm là xây dựng các mô hình đặc tả thiết kế của phần mềm, ở đây là biểu đồ tuần tự UML2.