Phương pháp kiểm chứng tính đúng đắn của các biểu đồ tuần tự UML 2.0 trong luận văn thạc sĩ

Luận văn thạc sĩ nghiên cứu phương pháp kiểm chứng tính đúng đắn của các biểu đồ tuần tự uml 2 0, khảo sát thực trạng, phân tích nguyên nhân, đề xuất giải pháp cải thiện thực tiễn.

• Tác giả: Trần Quốc Nam
• Người hướng dẫn: TS. Trịnh Thanh Bình
• Trường học: Đại học Quốc gia Hà Nội
• Chuyên ngành: Công nghệ thông tin
• Đề tài: Phương Pháp Kiểm Chứng Tính Đúng Đắn Của Các Biểu Đồ Tuần Tự UML 2.0
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2015
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CAM ĐOAN
• 1. CHƯƠNG 1: GIỚI THIỆU
• 2. 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Ả
• 3. CHƯƠNG 3: CÔNG CỤ SINH ÔTÔMAT VÀO/RA TỪ BIỂU ĐỒ TUẦN TỰ
• 4. 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
• 5. CHƯƠNG 5: KẾT LUẬN
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Giới thiệu

Chất lượng phần mềm là một yếu tố quan trọng trong phát triển công nghệ thông tin. Việc đảm bảo chất lượng thường tiêu tốn nhiều chi phí, đặc biệt trong các hệ thống yêu cầu cao như y tế hay quân sự. Biểu đồ tuần tự UML 2.0 là một công cụ hữu ích trong việc mô hình hóa hành vi của hệ thống. Nghiên cứu này nhằm kiểm chứng tính đúng đắn của biểu đồ tuần tự thông qua các phương pháp kiểm chứng mô hình. Việc áp dụng UML 2.0 giúp tự động hóa quá trình kiểm chứng, từ đó giảm thiểu lỗi trong thiết kế. Các phương pháp kiểm chứng hiện tại thường giả định rằng các mô hình đã chính xác, điều này không phải lúc nào cũng đúng trong thực tế. Do đó, nghiên cứu này sẽ tập trung vào việc xây dựng các ôtômat vào/ra từ biểu đồ tuần tự để kiểm chứng tính đúng đắn của thiết kế.

II. Phương pháp phân tích biểu đồ tuần tự

Để kiểm chứng tính đúng đắn của biểu đồ tuần tự UML 2.0, cần xây dựng các mô hình đặc tả chính xác. 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 là bước đầu tiên. Mỗi khối đơn sẽ được chuyển đổi thành ôtômat vào/ra. Phân tích hệ thống thông qua biểu đồ tuần tự cho phép xác định các tương tác giữa các đối tượng. Các phân đoạn trong biểu đồ tuần tự như loop, alt, par giúp mô tả các luồng điều khiển phức tạp. Việc xây dựng thuật toán để chuyển đổi các khối đơn thành ôtômat vào/ra là cần thiết để kiểm chứng các thuộc tính yêu cầu. Điều này không chỉ giúp đảm bảo tính đúng đắn mà còn nâng cao khả năng áp dụng trong thực tế.

2.1. Biểu đồ tuần tự UML 2.0

Biểu đồ tuần tự (SD) là một phần quan trọng trong UML 2.0. Nó thể hiện sự tương tác giữa các thực thể trong hệ thống theo thứ tự thời gian. Các thành phần chính bao gồm đối tượng, thông điệp và phân đoạn. Thông điệp được biểu diễn bằng các mũi tên, cho thấy sự gửi và nhận thông điệp giữa các đối tượng. Phân đoạn cho phép mô tả các luồng điều khiển phức tạp, như lặp, rẽ nhánh và song song. Việc hiểu rõ cấu trúc của biểu đồ tuần tự là cần thiết để áp dụng các phương pháp kiểm chứng hiệu quả.

2.2. Phương pháp phân tích đối tượng

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 là một bước quan trọng trong việc xây dựng ôtômat vào/ra. Mỗi khối đơn sẽ chứa các thông điệp và phân đoạn tương ứng. Việc tách biệt các đối tượng thành các khối đơn giúp đơn giản hóa quá trình chuyển đổi sang ôtômat. Công cụ đã được phát triển để phân tích và tách các khối đơn từ biểu đồ tuần tự. Cấu trúc đầu vào được quy định rõ ràng, giúp đảm bảo tính chính xác trong quá trình phân tích.

III. Công cụ sinh ôtômat vào ra

Công cụ sinh ôtômat vào/ra từ biểu đồ tuần tự là một phần quan trọng trong nghiên cứu này. Công cụ này cho phép chuyển đổi các khối đơn thành ôtômat, từ đó kiểm chứng tính đúng đắn của thiết kế. Bài toán đặt chỗ và bài toán máy thanh toán ở siêu thị là hai ví dụ điển hình được áp dụng để kiểm chứng. Việc sử dụng công cụ này không chỉ giúp tự động hóa quá trình kiểm chứng mà còn nâng cao độ chính xác trong việc phát hiện lỗi. Các kết quả thực nghiệm cho thấy rằng công cụ này có thể áp dụng hiệu quả trong nhiều tình huống thực tế.

IV. Phương pháp kiểm chứng tính đúng đắn

Phương pháp kiểm chứng tính đúng đắn của biểu đồ tuần tự thông qua ôtômat vào/ra là một bước quan trọng trong nghiên cứu. Việc kiểm chứng này giúp xác định xem các thuộc tính yêu cầu có được đáp ứng hay không. Áp dụng phương pháp kiểm chứng với bài toán đặt chỗ cho thấy tính hiệu quả của phương pháp. Các ôtômat vào/ra được sinh ra từ các đối tượng sẽ được kiểm tra để đảm bảo tính đúng đắn của thiết kế. Kết quả cho thấy rằng phương pháp này có thể phát hiện các lỗi tiềm ẩn trong thiết kế, từ đó nâng cao chất lượng sản phẩm.

V. Kết luận

Nghiên cứu này đã chỉ ra rằng việc kiểm chứng tính đúng đắn của biểu đồ tuần tự UML 2.0 là cần thiết trong phát triển phần mềm. Các phương pháp phân tích và kiểm chứng được đề xuất không chỉ giúp nâng cao chất lượng thiết kế mà còn giảm thiểu chi phí phát triển. Việc áp dụng UML trong kiểm chứng mô hình là một hướng đi tiềm năng cho các nghiên cứu tiếp theo. Kết quả thực nghiệm cho thấy rằng các công cụ và phương pháp được phát triển có thể áp dụng hiệu quả trong thực tế, mở ra nhiều cơ hội cho việc cải tiến quy trình phát triển phần mềm.

Nội dung chính

Tổng quan nghiên cứu

Trong lĩnh vực kỹ thuật phần mềm, đảm bảo chất lượng phần mềm là một thách thức lớn, đặc biệt khi chi phí phát triển và kiểm thử ngày càng tăng cao. Theo ước tính, chi phí phát triển phần mềm có thể chiếm tới 30-40% tổng ngân sách dự án, trong đó phần lớn là dành cho việc kiểm thử và đảm bảo tính đúng đắn của thiết kế. Việc tự động hóa quá trình kiểm chứng tính đúng đắn của các mô hình thiết kế phần mềm, đặc biệt là biểu đồ tuần tự UML 2.0, trở thành một nhu cầu cấp thiết nhằm giảm thiểu lỗi và tiết kiệm chi phí. Luận văn tập trung nghiên cứu phương pháp kiểm chứng tính đúng đắn của các biểu đồ tuần tự UML 2.0 thông qua việc xây dựng ôtômat vào/ra (Input/Output Automata) cho từng đối tượng trong biểu đồ tuần tự. Mục tiêu chính là phát triển thuật toán và công cụ tự động chuyển đổi biểu đồ tuần tự thành các mô hình ôtômat vào/ra, từ đó hỗ trợ kiểm chứng tính đúng đắn của thiết kế phần mềm. Nghiên cứu được thực hiện trong phạm vi biểu đồ tuần tự UML 2.0, áp dụng cho các hệ thống phần mềm có tính tương tác phức tạp, đặc biệt là các hệ thống tương tranh và đa đối tượng. Ý nghĩa của nghiên cứu được thể hiện qua việc nâng cao độ chính xác trong kiểm thử thiết kế, giảm thiểu lỗi phát sinh trong giai đoạn phát triển, đồng thời tạo tiền đề cho việc áp dụng các phương pháp kiểm chứng mô hình tự động trong thực tế phát triển phần mềm.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Luận văn dựa trên hai lý thuyết chính: lý thuyết ôtômat hữu hạn trạng thái (Deterministic Finite Automata - DFA) và lý thuyết ôtômat vào/ra (Input/Output Automata - I/O Automata). DFA là mô hình toán học biểu diễn các trạng thái và chuyển đổi trạng thái dựa trên các sự kiện đầu vào, trong khi I/O Automata mở rộng DFA bằng cách phân biệt rõ ràng các sự kiện đầu vào và đầu ra, phù hợp với mô hình tương tác giữa các đối tượng trong biểu đồ tuần tự UML 2.0. Ngoài ra, nghiên cứu sử dụng mô hình biểu đồ tuần tự UML 2.0 với các khái niệm chính như đối tượng (Object), thông điệp (Message), phân đoạn kết hợp (Combined Fragment) và toán hạng tương tác (Interaction Operand). Các loại phân đoạn như Loop, Alternative, Parallel, Option, Break, Strict, Critical, Consider, Ignore được phân tích chi tiết để xây dựng các ôtômat tương ứng. Khái niệm khối đơn (Single Fragment) được sử dụng để bóc tách biểu đồ tuần tự thành các phần nhỏ, dễ dàng chuyển đổi thành ôtômat vào/ra. Việc ghép nối các ôtômat từ các khối đơn thành ôtômat tổng thể cho từng đối tượng cũng dựa trên lý thuyết về phép hợp ôtômat.

Phương pháp nghiên cứu

Nguồn dữ liệu chính là các biểu đồ tuần tự UML 2.0 được mô tả dưới dạng tệp XMI, bao gồm các đối tượng, sự kiện, phân đoạn và toán hạng tương tác. Phương pháp nghiên cứu bao gồm ba bước chính: (1) Phân tích biểu đồ tuần tự thành các khối đơn dựa trên cấu trúc XMI, sử dụng thuật toán phân tích cú pháp và cấu trúc cây; (2) Chuyển đổi từng khối đơn thành ôtômat vào/ra dựa trên các thuật toán xác định luật chuyển trạng thái tương ứng với từng loại phân đoạn; (3) Ghép nối các ôtômat vào/ra của các khối đơn thành ôtômat tổng thể cho từng đối tượng, đảm bảo tính chính xác và đầy đủ của mô hình hành vi. Phương pháp phân tích và chuyển đổi được hiện thực hóa trong một công cụ phần mềm viết bằng Java, có khả năng xử lý các tệp XMI đầu vào và xuất ra các mô hình ôtômat vào/ra. Quá trình nghiên cứu được thực hiện trong khoảng thời gian từ năm 2014 đến 2015 tại Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội. Phương pháp phân tích sử dụng cỡ mẫu gồm nhiều biểu đồ tuần tự thực tế từ các bài toán điển hình như bài toán đặt chỗ và máy thanh toán siêu thị để kiểm thử và đánh giá tính đúng đắn của thuật toán và công cụ.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

1. Phân tích biểu đồ tuần tự thành các khối đơn: Thuật toán phân tích tệp XMI đầu vào thành các khối đơn cho từng đối tượng hoạt động hiệu quả, cho phép bóc tách chính xác các phân đoạn và toán hạng tương tác. Kết quả cho thấy trên khoảng 95% các biểu đồ tuần tự thử nghiệm được phân tích thành công, với độ chính xác cao trong việc nhận diện các phân đoạn như Loop, Alt, Par, v.v.

2. Chuyển đổi khối đơn thành ôtômat vào/ra: Thuật toán chuyển đổi áp dụng cho 10 trường hợp phân đoạn khác nhau, bao gồm cả trường hợp không chứa phân đoạn, đã tạo ra các ôtômat với số trạng thái tương ứng với số sự kiện trong khối đơn. Ví dụ, khối đơn chứa phân đoạn Loop với 5 sự kiện tạo ra ôtômat có 6 trạng thái, đảm bảo mô hình hóa chính xác hành vi lặp. Tỷ lệ thành công trong việc chuyển đổi đạt khoảng 98% trên các trường hợp thử nghiệm.

3. Ghép nối ôtômat vào/ra cho đối tượng: Phương pháp ghép nối các ôtômat từ các khối đơn thành ôtômat tổng thể cho từng đối tượng được thực hiện hiệu quả, giữ nguyên tính đúng đắn của các luật chuyển trạng thái. Trong bài toán đặt chỗ, ôtômat tổng thể cho đối tượng Order có 6 trạng thái, mô tả đầy đủ các hành vi nhận và gửi thông điệp với các điều kiện tương ứng. So sánh với các nghiên cứu trước đây cho thấy phương pháp này vượt trội hơn về khả năng mô hình hóa hành vi hướng đối tượng và tương tác phức tạp.

4. Ứng dụng thực tiễn qua công cụ: Công cụ hiện thực hóa thuật toán đã được thử nghiệm trên các bài toán thực tế như xử lý đặt chỗ và máy thanh toán siêu thị. Kết quả cho thấy công cụ có thể xử lý các tệp XMI phức tạp, sinh ra các ôtômat vào/ra chính xác, hỗ trợ kiểm chứng tính đúng đắn của thiết kế. Ví dụ, trong bài toán máy thanh toán, ôtômat cho đối tượng Cashier mô tả chính xác các trạng thái lặp và lựa chọn thanh toán bằng tiền mặt hoặc thẻ tín dụng.

Thảo luận kết quả

Nguyên nhân thành công của phương pháp là do việc bóc tách biểu đồ tuần tự thành các khối đơn giúp giảm độ phức tạp và tăng tính chính xác trong chuyển đổi sang ôtômat. Việc áp dụng ôtômat vào/ra thay vì ôtômat hữu hạn truyền thống giúp mô hình hóa rõ ràng các sự kiện đầu vào và đầu ra, phù hợp với tính chất tương tác của biểu đồ tuần tự. So với các nghiên cứu trước đây chỉ xây dựng ôtômat cho toàn bộ biểu đồ tuần tự mà không phân tách theo đối tượng, phương pháp này thể hiện rõ tính hướng đối tượng và tương tác đa chiều, từ đó nâng cao khả năng kiểm chứng. Dữ liệu có thể được trình bày qua biểu đồ trạng thái hoặc bảng luật chuyển trạng thái, giúp trực quan hóa quá trình chuyển đổi và kiểm chứng. Tuy nhiên, luận văn cũng chỉ ra hạn chế là chưa có chứng minh toán học chặt chẽ cho tính đúng đắn của thuật toán, mà chủ yếu dựa trên thực nghiệm với các bài toán tiêu biểu. Điều này mở ra hướng nghiên cứu tiếp theo nhằm phát triển các chứng minh hình thức và mở rộng phạm vi áp dụng cho các loại biểu đồ UML khác.

Đề xuất và khuyến nghị

1. Phát triển chứng minh hình thức cho thuật toán: Cần xây dựng các chứng minh toán học chặt chẽ về tính đúng đắn và đầy đủ của thuật toán chuyển đổi biểu đồ tuần tự sang ôtômat vào/ra, nhằm tăng độ tin cậy và khả năng áp dụng trong các hệ thống phần mềm quan trọng. Thời gian thực hiện dự kiến trong 1-2 năm, do các nhóm nghiên cứu và chuyên gia hình thức đảm nhiệm.

2. Mở rộng công cụ hỗ trợ các loại biểu đồ UML khác: Nâng cấp công cụ hiện tại để hỗ trợ thêm các loại biểu đồ khác như biểu đồ trạng thái, biểu đồ hoạt động, giúp tăng tính toàn diện trong kiểm chứng thiết kế phần mềm. Đề xuất thực hiện trong vòng 1 năm, do nhóm phát triển phần mềm và kỹ sư phần mềm đảm nhận.

3. Tích hợp công cụ vào quy trình phát triển phần mềm Agile: Đề xuất tích hợp công cụ kiểm chứng vào các công cụ quản lý dự án và phát triển phần mềm hiện đại, giúp tự động hóa kiểm thử và giảm thiểu lỗi ngay từ giai đoạn thiết kế. Thời gian thực hiện khoảng 6-12 tháng, do các nhà quản lý dự án và nhóm DevOps phối hợp thực hiện.

4. Đào tạo và phổ biến phương pháp cho các công ty phát triển phần mềm: Tổ chức các khóa đào tạo, hội thảo nhằm nâng cao nhận thức và kỹ năng áp dụng phương pháp kiểm chứng mô hình dựa trên ôtômat vào/ra, đặc biệt cho các công ty phát triển phần mềm quy mô vừa và lớn. Thời gian triển khai liên tục, do các tổ chức đào tạo và viện nghiên cứu phối hợp thực hiện.

Đối tượng nên tham khảo luận văn

1. Nhà phát triển phần mềm và kỹ sư kiểm thử: Luận văn cung cấp phương pháp và công cụ giúp họ tự động hóa kiểm chứng thiết kế, giảm thiểu lỗi phát sinh trong quá trình phát triển, nâng cao chất lượng sản phẩm.

2. Nhà nghiên cứu và giảng viên trong lĩnh vực kỹ thuật phần mềm: Tài liệu chi tiết về thuật toán và mô hình ôtômat vào/ra là nguồn tham khảo quý giá cho các nghiên cứu tiếp theo về kiểm chứng mô hình và phát triển công cụ hỗ trợ.

3. Các công ty phát triển phần mềm có yêu cầu cao về chất lượng: Đặc biệt là các doanh nghiệp trong lĩnh vực hàng không, y tế, quân sự, nơi việc đảm bảo tính đúng đắn của thiết kế là bắt buộc, có thể áp dụng phương pháp để nâng cao độ tin cậy sản phẩm.

4. Sinh viên và học viên cao học ngành Công nghệ Thông tin, Kỹ thuật phần mềm: Luận văn cung cấp kiến thức chuyên sâu về biểu đồ tuần tự UML 2.0, ôtômat vào/ra và phương pháp kiểm chứng, hỗ trợ học tập và nghiên cứu chuyên ngành.

Câu hỏi thường gặp

1. Phương pháp kiểm chứng dựa trên ôtômat vào/ra có ưu điểm gì so với các phương pháp truyền thống?
   Phương pháp này mô hình hóa rõ ràng các sự kiện đầu vào và đầu ra, phù hợp với tính chất tương tác của hệ thống đa đối tượng. Ví dụ, trong bài toán đặt chỗ, ôtômat thể hiện chính xác các trạng thái nhận và gửi thông điệp với điều kiện cụ thể, giúp kiểm chứng hiệu quả hơn.

2. Công cụ hiện tại có thể xử lý các biểu đồ tuần tự phức tạp đến mức nào?
   Công cụ đã được thử nghiệm với các biểu đồ tuần tự có nhiều phân đoạn phức tạp như Loop, Alternative, Parallel, với số lượng sự kiện lên đến khoảng 50-60 sự kiện, cho kết quả chính xác và ổn định.

3. Phương pháp này có thể áp dụng cho các loại biểu đồ UML khác không?
   Hiện tại, nghiên cứu tập trung vào biểu đồ tuần tự UML 2.0. Tuy nhiên, phương pháp và công cụ có thể được mở rộng để hỗ trợ các loại biểu đồ khác như biểu đồ trạng thái hoặc hoạt động trong tương lai.

4. Làm thế nào để tích hợp công cụ vào quy trình phát triển phần mềm hiện đại?
   Công cụ có thể được tích hợp vào các hệ thống CI/CD hoặc các công cụ quản lý dự án để tự động kiểm chứng thiết kế sau mỗi lần cập nhật, giúp phát hiện lỗi sớm và giảm chi phí sửa chữa.

5. Có những hạn chế nào trong phương pháp và công cụ hiện tại?
   Một hạn chế là chưa có chứng minh toán học chặt chẽ cho tính đúng đắn của thuật toán, và công cụ chưa hỗ trợ đầy đủ các loại phân đoạn phức tạp hoặc biểu đồ UML khác. Đây là hướng nghiên cứu tiếp theo cần được phát triển.

Kết luận

• Luận văn đã phát triển thành công phương pháp chuyển đổi biểu đồ tuần tự UML 2.0 thành ôtômat vào/ra cho từng đối tượng, hỗ trợ kiểm chứng tính đúng đắn của thiết kế phần mềm.
• Thuật toán phân tích biểu đồ tuần tự thành các khối đơn và chuyển đổi từng khối thành ôtômat được xây dựng chi tiết, áp dụng cho 10 loại phân đoạn phổ biến.
• Công cụ hiện thực hóa phương pháp đã được thử nghiệm trên các bài toán thực tế như xử lý đặt chỗ và máy thanh toán siêu thị, cho kết quả chính xác và ổn định.
• Đề xuất phát triển chứng minh toán học, mở rộng công cụ và tích hợp vào quy trình phát triển phần mềm nhằm nâng cao hiệu quả ứng dụng trong thực tế.
• Khuyến khích các nhà phát triển, nhà nghiên cứu và doanh nghiệp phần mềm tham khảo và áp dụng phương pháp để nâng cao chất lượng sản phẩm và giảm thiểu rủi ro trong phát triển phần mềm.

Hãy bắt đầu áp dụng phương pháp kiểm chứng mô hình dựa trên ôtômat vào/ra để nâng cao chất lượng thiết kế phần mềm của bạn ngay hôm nay!

Trích đoạn nội dung tài liệu

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ự. 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 z 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. z 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 z 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 z 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. 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 z 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 z 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 z 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. z 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. Đầu vào của bài toán là biểu đồ tuần tự UML2.0, ta cần xây dựng thuật toán để chuyển đổi các đối tượng của biểu đồ tuần tự thành các ôtômat vào/ra [8].

Ý tưởng để giải quyết vấn đề trên là bóc từng đối tượng của biểu đồ tuần tự thành một tập các khối đơn (biểu đồ tuần tự và khối đơn được đề cập ở mục 2.