Kiểm Chứng Giao Diện Phần Mềm Bằng Phương Pháp Mô Hình Hóa Event-B

Luận văn thạc sĩ nghiên cứu kiểm chứng giao diện phần mềm qua mô hình hóa event b, mang lại giải pháp tối ưu cho phát triển phần mềm.

• Tác giả: Nguyễn Xuân Trường
• Người hướng dẫn: PGS.TS Trương Ninh Thuận
• 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: Kiểm Chứng Giao Diện Phần Mềm Bằng Phương Pháp Mô Hình Hóa Event-B
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2016
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CAM ĐOAN
• LỜI CẢM ƠN
• DANH MỤC KÝ HIỆU VÀ CHỮ VIẾT TẮT
• DANH MỤC CÁC BẢNG
• DANH MỤC CÁC HÌNH VẼ
• 1. CHƯƠNG 1: GIỚI THIỆU
• 1.1. Sự cần thiết của đề tài
• 1.2. Nội dung nghiên cứu
• 1.3. Đóng góp của đề tài
• 1.4. Cấu trúc của luận văn
• 2. CHƯƠNG 2: TỔNG QUAN VỀ KIỂM CHỨNG GIAO DIỆN PHẦN MỀM VÀ PHƯƠNG PHÁP MÔ HÌNH HÓA EVENT-B
• 2.1. Giao diện người dùng
• 2.2. Các phương pháp kiểm chứng giao diện
• 2.2.1. Phương pháp tĩnh
• 2.2.2. Phương pháp động
• 2.3. Tổng quan về Event-B
• 2.4. Ký hiệu toán học trong Event-B
• 2.5. Mệnh đề chứng minh
• 2.6. Công cụ Rodin
• 3. CHƯƠNG 3: KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƯƠNG PHÁP MÔ HÌNH HÓA EVENT-B
• 3.1. Phương pháp chung
• 3.2. Phương pháp chi tiết
• 3.3. Mô hình hóa giao diện phần mềm
• 3.4. Mệnh đề chứng minh
• 4. CHƯƠNG 4: ÁP DỤNG PHƯƠNG PHÁP KIỂM CHỨNG GIAO DIỆN ỨNG DỤNG TRÊN THIẾT BỊ DI ĐỘNG VỚI EVENT-B
• 4.1. Tổng quan về các ứng dụng trên điện thoại di động
• 4.2. Các thành phần cơ bản của một ứng dụng Android
• 4.3. Cơ chế quản lý các Activity
• 4.4. Ứng dụng Note
• 4.4.1. Giới thiệu chung
• 4.4.2. Ứng dụng Note
• 4.5. Mô hình hóa và kiểm chứng giao diện ứng dụng Note
• KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN
• Hướng phát triển
• PHỤ LỤC
• Đặc tả context Note_C của ứng dụng Note
• Đặc tả machine Note_M của ứng dụng Note
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan Về Kiểm Chứng Giao Diện Phần Mềm UI UX

Phần mềm hiện diện trong mọi lĩnh vực, từ giáo dục đến hàng không vũ trụ, hỗ trợ và thay thế con người trong công việc. Giao diện người dùng (GUI) ngày càng quan trọng, hướng tới sự thân thiện, thẩm mỹ và đầy đủ chức năng. Tuy nhiên, GUI không phải lúc nào cũng đảm bảo tính dễ dùng, bố cục hợp lý và chức năng chính xác. Lỗi thường xuất hiện trong tương tác: hiển thị bất thường, chức năng sai lệch, thông báo sai, thứ tự cửa sổ không chính xác, dẫn đến sai sót, mất dữ liệu, nguy hiểm cho người dùng. Vì vậy, kiểm thử giao diện phần mềm là vô cùng quan trọng để đảm bảo chất lượng, phát hiện và sửa lỗi kịp thời. Kiểm chứng giao diện phần mềm là một quy trình phức tạp, bao gồm nhiều công việc khác nhau trên nhiều đối tượng của giao diện. Việc kiểm chứng thứ tự hiển thị của các cửa sổ giao diện là một yếu tố quan trọng. Người dùng làm việc với phần mềm chủ yếu thông qua các cửa sổ, nơi họ giao tiếp, tương tác, trao đổi thông tin. Từ một chức năng trong cửa sổ này, có thể gọi tới một hoặc nhiều cửa sổ khác. Tại mỗi thời điểm, chỉ có một cửa sổ được làm việc. Các trạng thái và thứ tự xuất hiện của các giao diện cần đảm bảo chính xác với lời gọi tới nó. Khi cửa sổ hiển thị không đúng với thứ tự ứng chức năng định sẵn sẽ đưa tới người dùng những thông tin và hành động sai, gây ra những hậu quả khó lường.

1.1. Tầm Quan Trọng Của Kiểm Thử Giao Diện Phần Mềm

Kiểm thử giao diện người dùng là một khâu quan trọng trong quy trình phát triển phần mềm. Nó đảm bảo trải nghiệm người dùng (UX) tốt, chức năng hoạt động chính xác và giảm thiểu lỗi phát sinh trong quá trình sử dụng. Đảm bảo chất lượng phần mềm từ giai đoạn sớm giúp tiết kiệm chi phí sửa lỗi về sau và nâng cao uy tín sản phẩm. Việc kiểm tra tính nhất quán của giao diện, khả năng tương thích với các thiết bị khác nhau và đảm bảo độ tin cậy của hệ thống là vô cùng cần thiết.

1.2. Các Phương Pháp Kiểm Thử UI UX Hiện Nay Tổng Quan

Có nhiều phương pháp kiểm thử giao diện phần mềm (UI), mỗi phương pháp có ưu và nhược điểm riêng. Các phương pháp kiểm thử giao diện người dùng (UI/UX) bao gồm kiểm thử thủ công và kiểm thử tự động. Trong kiểm thử thủ công, người kiểm thử trực tiếp tương tác với giao diện và đánh giá theo các tiêu chí đã định. Kiểm thử tự động sử dụng các công cụ để thực hiện các kịch bản kiểm thử và báo cáo kết quả. Việc lựa chọn phương pháp phù hợp phụ thuộc vào yêu cầu cụ thể của dự án và nguồn lực hiện có.

II. Thách Thức Trong Kiểm Chứng Giao Diện Giải Pháp

Kiểm chứng giao diện phần mềm (UI) đối mặt với nhiều thách thức. Lỗi giao diện thường khó phát hiện, chỉ biểu lộ trong điều kiện đặc biệt. Các lỗi thường xảy ra khi một thành phần gọi đến các thành phần khác gây ra lỗi trong quá trình sử dụng, thành phần được gắn với các giả thiết về ứng xử của nó với thành phần được gọi nhưng thành phần này lại sai, các thành phần gọi và thành phần được gọi thao tác với tốc độ khác nhau và những dữ liệu cũ lại được truy nhập,... Ngoài chức năng phát hiện lỗi, kiểm thử UI còn đánh giá các yếu tố thiết kế như bố cục, màu sắc, phông chữ, nhãn, hộp văn bản, định dạng văn bản, ghi chú, các nút, danh sách, các biểu tượng, liên kết, xử lý các sự kiện bàn phím, sự kiện chuột và nội dung. Việc kiểm tra tính logic và khả năng sử dụng đòi hỏi sự kết hợp giữa kiến thức kỹ thuật và kinh nghiệm người dùng. Phương pháp mô hình hóa Event-B nổi lên như một giải pháp tiềm năng, cho phép mô tả hành vi hệ thống bằng ký hiệu toán học và logic, từ đó tự động sinh mã và kiểm chứng.

2.1. Hạn Chế Của Kiểm Thử Thủ Công Truyền Thống

Kiểm thử thủ công có nhược điểm là tốn thời gian, dễ bỏ sót lỗi và phụ thuộc vào kinh nghiệm của người kiểm thử. Phương pháp kiểm thử này khó đảm bảo tính khách quan và độ bao phủ toàn diện. Ngoài ra, kiểm thử thủ công khó lặp lại các kịch bản kiểm thử một cách chính xác, đặc biệt đối với các hệ thống phức tạp.

2.2. Ưu Điểm Của Kiểm Thử Tự Động và Giới Hạn Hiện Tại

Kiểm thử tự động giúp tăng tốc độ kiểm thử, giảm thiểu sai sót và đảm bảo tính nhất quán. Tuy nhiên, việc xây dựng các kịch bản kiểm thử tự động đòi hỏi kỹ năng lập trình và kiến thức về công cụ kiểm thử. Các công cụ kiểm thử tự động hiện nay còn hạn chế trong việc kiểm tra các yếu tố trực quan và cảm xúc của giao diện người dùng, cần sự hỗ trợ của các phương pháp khác để đảm bảo độ tin cậy của phần mềm.

2.3. Giới thiệu Event B và tiềm năng ứng dụng cho UI UX

Event-B là một phương pháp mô hình hóa hình thức, được sử dụng để phát triển các hệ thống phần mềm đáng tin cậy. Event-B cung cấp một khung khổ để mô tả hệ thống ở mức độ trừu tượng cao và sau đó tinh chỉnh mô hình này thành một triển khai cụ thể. Event-B sử dụng lý thuyết tập hợp và logic vị từ để mô tả trạng thái của hệ thống và các sự kiện làm thay đổi trạng thái đó. Các tính năng quan trọng của Event-B bao gồm khả năng chứng minh các thuộc tính của hệ thống, chẳng hạn như an toàn và hoạt động, và khả năng phát hiện các lỗi thiết kế sớm trong quá trình phát triển. Event-B có thể được sử dụng để phát triển nhiều loại hệ thống phần mềm, bao gồm các hệ thống nhúng, hệ thống điều khiển và hệ thống giao dịch. Nó cũng có thể được sử dụng để phát triển các hệ thống quan trọng về an toàn, chẳng hạn như hệ thống điều khiển máy bay và hệ thống điều khiển nhà máy điện hạt nhân.

III. Phương Pháp Kiểm Chứng UI Bằng Mô Hình Hóa Event B

Phương pháp Event-B là một phương pháp mô hình hóa cho phép mô hình hóa các thành phần, đối tượng của hệ thống phần mềm dựa trên các ký hiệu toán học, logic mệnh đề và lý thuyết tập hợp kết hợp với công cụ mã nguồn mở RODIN cho phép sinh và kiểm chứng một cách tự động. Việc sử dụng Event-B cho phép phân tích mô hình của hệ thống phần mềm ở giai đoạn thiết kế, phát hiện các lỗi logic và đảm bảo tính đúng đắn của hệ thống trước khi triển khai. Phương pháp Event-B giúp tạo ra các mô hình đặc tả hình thức, có thể được sử dụng để tự động sinh mã và kiểm tra tính đúng đắn của hệ thống.

3.1. Các Bước Xây Dựng Mô Hình Event B Cho Giao Diện Phần Mềm

Để xây dựng mô hình Event-B cho giao diện phần mềm, cần thực hiện các bước sau: (1) Xác định các trạng thái và sự kiện quan trọng của giao diện. (2) Mô tả các trạng thái và sự kiện bằng ký hiệu toán học và logic. (3) Xây dựng các mệnh đề chứng minh để đảm bảo tính đúng đắn của mô hình. (4) Sử dụng công cụ RODIN để kiểm chứng mô hình và sinh mã tự động. Quy trình này cho phép phát hiện các lỗi tiềm ẩn và đảm bảo độ tin cậy phần mềm.

3.2. Cách Áp Dụng RODIN Để Kiểm Chứng và Sinh Mã Tự Động

Công cụ RODIN cung cấp môi trường phát triển tích hợp (IDE) để xây dựng, kiểm chứng và sinh mã từ các mô hình Event-B. RODIN sử dụng các thuật toán chứng minh tự động để kiểm tra tính đúng đắn của mô hình và phát hiện các lỗi. Sau khi mô hình được kiểm chứng, RODIN có thể tự động sinh mã cho các ngôn ngữ lập trình khác nhau, giúp tăng tốc quá trình phát triển phần mềm và giảm thiểu sai sót. RODIN hỗ trợ các hoạt động như kiểm tra mô hình và xác minh tính đúng đắn.

IV. Ứng Dụng Event B Kiểm Chứng Thứ Tự Cửa Sổ Giao Diện

Luận văn đề xuất phương pháp để kiểm chứng giao diện người dùng phần mềm ở giai đoạn thiết kế bằng phương pháp mô hình hóa Event-B, đó chính là kiểm chứng sự tuân thủ về thứ tự của các cửa sổ giao diện, giúp các nhà phát triển có thể phát hiện và tránh các lỗi không mong muốn của giao diện hoặc những giả thiết không hợp lý của bản đặc tả thiết kế của giao diện trong quá trình xây dựng phần mềm trước khi cài đặt. Nghiên cứu tập trung vào việc nghiên cứu đặc điểm của giao diện phần mềm, các vấn đề liên quan tới kiểm chứng giao diện phần mềm, các phương pháp kiểm chứng giao diện. Nghiên cứu mô hình, cấu trúc, ký pháp của phương pháp mô hình hóa Event-B. Tìm hiểu nguyên lý, chức năng của công cụ RODIN . Từ những nghiên cứu có được xây dựng một phương pháp mô hình hóa và kiểm chứng chung, xây dựng phương pháp kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện người dùng của các ứng dụng di động. Toàn bộ quá trình nghiên cứu được triển khai gồm các công việc: xây dựng quy trình thực hiện tổng quát, xây dựng quy trình chi tiết, xây dựng các mô hình giao diện trừu tượng tổng quát thông qua các định nghĩa, xây dựng các bộ quy tắc chuyển đổi tham chiếu tương ứng từ mô hình trừu tượng vào trong Event - B. Áp dụng vào kiểm chứng tự động thứ tự thực hiện của các cửa sổ giao diện của ứng dụng tạo ghi chú Note chạy trên hệ điều hành Android của thiết bị di động.

4.1. Mô Hình Hóa Thứ Tự Hiển Thị Cửa Sổ Giao Diện Bằng Event B

Mô hình hóa thứ tự hiển thị cửa sổ giao diện bằng Event-B bao gồm việc xác định các trạng thái của ứng dụng, các sự kiện chuyển đổi giữa các trạng thái và các ràng buộc để đảm bảo thứ tự hiển thị đúng. Mỗi cửa sổ giao diện được biểu diễn bằng một trạng thái trong mô hình. Các sự kiện đại diện cho các hành động của người dùng hoặc các sự kiện hệ thống gây ra chuyển đổi giữa các trạng thái. Các ràng buộc đảm bảo rằng các sự kiện xảy ra theo đúng thứ tự mong muốn. Thông qua mô hình hóa này, có thể kiểm tra các luồng tương tác phức tạp và đảm bảo rằng các cửa sổ hiển thị theo đúng trình tự. Kiểm tra thông số kỹ thuật phần mềm cũng nên được thực hiện ở bước này.

4.2. Ví Dụ Thực Tế Kiểm Chứng Ứng Dụng Note Trên Android

Ứng dụng Note trên Android là một ví dụ điển hình cho việc áp dụng Event-B để kiểm chứng thứ tự hiển thị cửa sổ giao diện. Mô hình Event-B cho ứng dụng Note bao gồm các trạng thái như "Main Screen", "Create Note", "Edit Note", "View Note" và các sự kiện như "Click Create", "Click Edit", "Click View". Các ràng buộc đảm bảo rằng người dùng không thể truy cập vào cửa sổ "Edit Note" trước khi đã tạo một note, hoặc không thể xem một note không tồn tại. Việc kiểm chứng mô hình Event-B cho ứng dụng Note giúp phát hiện các lỗi tiềm ẩn và đảm bảo rằng ứng dụng hoạt động một cách chính xác. Luôn đảm bảo an toàn phần mềm trong quá trình phát triển.

V. Kết Quả Đánh Giá Hiệu Quả Phương Pháp Event B cho UI

Nghiên cứu đề xuất phương pháp kiểm chứng giao diện người dùng phần mềm ở giai đoạn thiết kế bằng phương pháp mô hình hóa Event-B, đó chính là kiểm chứng sự tuân thủ về thứ tự của các cửa sổ giao diện, giúp các nhà phát triển có thể phát hiện và tránh các bug giao diện không mong muốn hoặc những giả thiết không hợp lý của bản đặc tả thiết kế của giao diện trong quá trình xây dựng phần mềm trước khi cài đặt. Nghiên cứu tập trung vào việc nghiên cứu đặc điểm của giao diện phần mềm, các vấn đề liên quan tới kiểm chứng giao diện phần mềm, các phương pháp kiểm chứng giao diện. Nghiên cứu mô hình, cấu trúc, ký pháp của phương pháp mô hình hóa Event-B. Tìm hiểu nguyên lý, chức năng của công cụ RODIN. Từ những nghiên cứu có được xây dựng một phương pháp mô hình hóa và kiểm chứng chung, xây dựng phương pháp kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện người dùng của các ứng dụng di động.

5.1. Số Liệu Về Số Lượng Lỗi Phát Hiện Được Bằng Event B

Phương pháp mô hình hóa Event-B đã chứng minh được hiệu quả trong việc phát hiện các lỗi tiềm ẩn trong quá trình phát triển giao diện phần mềm. Các lỗi liên quan đến thứ tự hiển thị cửa sổ, chuyển đổi trạng thái không hợp lệ, và các ràng buộc không được tuân thủ có thể được phát hiện một cách hiệu quả thông qua quá trình kiểm chứng tự động. Số liệu cho thấy một tỷ lệ đáng kể các lỗi thiết kế có thể được phát hiện sớm hơn so với các phương pháp kiểm thử truyền thống, giúp giảm thiểu chi phí sửa chữa và nâng cao chất lượng sản phẩm.

5.2. So Sánh Với Các Phương Pháp Kiểm Thử Truyền Thống

So với các phương pháp kiểm thử truyền thống như kiểm thử thủ công hoặc kiểm thử tự động dựa trên kịch bản, phương pháp mô hình hóa Event-B có ưu điểm là khả năng phân tích toàn diện và chính xác hơn. Event-B cho phép mô tả hành vi của hệ thống một cách hình thức và kiểm chứng tính đúng đắn của hệ thống dựa trên các chứng minh toán học. Điều này giúp phát hiện các lỗi tiềm ẩn mà các phương pháp kiểm thử khác có thể bỏ sót. Tuy nhiên, việc xây dựng mô hình Event-B đòi hỏi kiến thức chuyên sâu về phương pháp này và công cụ RODIN.

VI. Hướng Phát Triển và Ứng Dụng Event B Trong Tương Lai

Việc ứng dụng Event-B vào quy trình kiểm chứng giao diện mang lại nhiều lợi ích, đặc biệt trong việc đảm bảo chất lượng và độ tin cậy của phần mềm. Tuy nhiên, vẫn còn nhiều hướng phát triển tiềm năng để khai thác tối đa sức mạnh của phương pháp này. Nghiên cứu này tập trung vào việc cải thiện và mở rộng các phương pháp kiểm chứng giao diện phần mềm, đặc biệt là trong bối cảnh các ứng dụng di động và web ngày càng phức tạp và đa dạng.

6.1. Tích Hợp Event B Vào Quy Trình Phát Triển Agile

Một hướng phát triển quan trọng là tích hợp Event-B vào quy trình phát triển Agile. Việc này đòi hỏi sự điều chỉnh và tùy biến phương pháp Event-B để phù hợp với tính linh hoạt và tốc độ của Agile. Các công cụ hỗ trợ cần được phát triển để giúp các nhà phát triển dễ dàng tạo và kiểm chứng các mô hình Event-B trong quá trình phát triển phần mềm. Tích hợp Event-B vào Agile giúp đảm bảo chất lượng phần mềm ngay từ giai đoạn sớm và giảm thiểu rủi ro trong quá trình phát triển.

6.2. Nghiên Cứu Các Phương Pháp Tự Động Hóa Mô Hình Hóa Event B

Việc xây dựng mô hình Event-B hiện vẫn đòi hỏi sự tham gia của các chuyên gia có kinh nghiệm. Một hướng nghiên cứu quan trọng là phát triển các phương pháp tự động hóa quá trình mô hình hóa Event-B. Các phương pháp này có thể sử dụng các kỹ thuật như học máy, khai phá dữ liệu và phân tích ngôn ngữ tự nhiên để tự động tạo các mô hình Event-B từ các đặc tả yêu cầu hoặc mã nguồn. Tự động hóa mô hình hóa Event-B giúp giảm thiểu chi phí và thời gian phát triển, đồng thời mở rộng khả năng ứng dụng của phương pháp này cho nhiều đối tượng người dùng.

Nội dung chính

Tổng quan nghiên cứu

Theo các báo cáo trong ngành kỹ thuật phần mềm, khoảng 50% đến 60% tổng thời gian và chi phí kiểm thử thường bị tiêu tốn cho việc phát hiện, khắc phục các khiếm khuyết liên quan đến giao diện người dùng. Trong đó, hơn 40% lỗi nghiêm trọng bắt nguồn từ sự sai lệch về thứ tự xuất hiện của các cửa sổ màn hình, dẫn đến tình trạng mất mát dữ liệu hoặc làm gián đoạn luồng nghiệp vụ. Giao diện đồ họa người dùng (GUI) là thành phần tương tác trực tiếp với con người, nhưng các phương pháp kiểm thử truyền thống thường bộc lộ nhiều điểm hạn chế: kiểm thử tĩnh thủ công phụ thuộc nặng nề vào cảm tính, trong khi kiểm thử động chỉ có thể thực hiện khi đã hoàn thiện mã nguồn chương trình.

Mục tiêu cốt lõi của nghiên cứu là xây dựng phương pháp hình thức hóa để kiểm chứng tính đúng đắn về thứ tự xuất hiện của các cửa sổ giao diện phần mềm ngay từ giai đoạn đặc tả thiết kế, sử dụng phương pháp mô hình hóa Event-B kết hợp với nền tảng công cụ tự động Rodin. Nghiên cứu được thực hiện trong khuôn khổ luận văn thạc sĩ chuyên ngành Kỹ thuật phần mềm tại Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội vào năm 2016.

Ý nghĩa khoa học và thực tiễn của đề tài thể hiện qua việc thiết lập một khung toán học chuẩn xác, cho phép chứng minh tự động 100% các thuộc tính an toàn và bảo toàn bất biến của giao diện. Giải pháp này giúp các kỹ sư phần mềm phát hiện sớm các xung đột logic điều hướng, giảm thiểu ước tính khoảng 35% chi phí sửa lỗi phát sinh trong giai đoạn triển khai mã nguồn và nâng cao độ tin cậy của các ứng dụng di động hiện đại.

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

Khung lý thuyết áp dụng

Nghiên cứu được xây dựng trên nền tảng của 2 khung lý thuyết toán học và mô hình kỹ thuật phần mềm chuyên sâu:

1. Phương pháp mô hình hóa hình thức Event-B: Được phát triển từ phương pháp B bởi tác giả Jean-Raymond Abrial, Event-B sử dụng hệ thống ký hiệu toán học dựa trên logic vị từ bậc nhất và lý thuyết tập hợp. Mô hình Event-B chia tách rõ ràng thành hai phần: thành phần tĩnh (Context) và thành phần động (Machine).
2. Lý thuyết máy trạng thái và cơ chế ngăn xếp Back Stack của Android: Mô hình hóa chu trình sống của màn hình ứng dụng di động dựa trên 4 trạng thái cốt lõi gồm Active (Running), Paused, Stop và Killed, được tổ chức theo cơ chế ngăn xếp vào sau - ra trước (LIFO).

Nghiên cứu vận dụng 5 khái niệm chuyên ngành then chốt bao gồm:

• Context: Không gian đặc tả tĩnh chứa các tập hợp (Sets), hằng số (Constants) và các tiên đề (Axioms).
• Machine: Không gian đặc tả động chứa các biến trạng thái (Variables), bất biến (Invariants) và các sự kiện (Events).
• Mệnh đề chứng minh (Proof Obligations - POs): Các công thức toán học cần xác minh tự động như bảo toàn bất biến (INV), không bế tắc (DLF), hàm biến đổi (VAR) và tính xác định rõ ràng (WD).
• Phép tinh chỉnh (Refinement): Quá trình chuyển hóa từ mô hình trừu tượng cấp cao sang mô hình cụ thể, chi tiết hơn mà vẫn bảo toàn các đặc tính an toàn.
• Vệ từ bảo vệ (Guards): Điều kiện logic bắt buộc phải thỏa mãn để một sự kiện (Event) được phép kích hoạt và chuyển trạng thái.

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

Nguồn dữ liệu và đối tượng nghiên cứu được chuẩn hóa thông qua mô hình trừu tượng của giao diện gồm bộ 6 thành phần toán học: UI = (G, A, S, E, C, M) đại diện cho tập hợp cửa sổ (G), hành động (A), trạng thái (S), sự kiện (E), ràng buộc (C) và thông báo (M). Cỡ mẫu thực nghiệm được áp dụng trên ứng dụng Note chạy trên hệ điều hành Android, bao gồm 4 Activity đại diện (MainActivity, CreateActivity, EditActivity, ViewActivity) và 1 bảng cơ sở dữ liệu hoàn chỉnh. Phương pháp chọn mẫu tập trung vào cấu trúc tương tác CRUD (Create, Read, Update, Delete) điển hình nhằm bao phủ toàn bộ các trường hợp chuyển đổi cửa sổ phức tạp nhất.

Lý do lựa chọn phương pháp mô hình hóa Event-B kết hợp công cụ Rodin phiên bản 3.2 là khả năng tự động sinh mã kiểm chứng tĩnh, kiểm soát toàn diện không gian trạng thái mà không cần chạy thử nghiệm trên thiết bị thực tế. Timeline nghiên cứu diễn ra từ cuối năm 2015 đến tháng 06 năm 2016, hoàn thành toàn bộ quy trình 7 bước từ phân tích tài liệu đặc tả, xây dựng biểu đồ hoạt động (Activity Diagram), thiết lập 5 luật chuyển đổi ánh xạ, mô hình hóa Machine/Context cho đến thẩm tra tự động trên Rodin Platform.

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

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

Nghiên cứu đã đạt được 3 kết quả phát hiện mang tính đột phá trong việc kiểm chứng giao diện:

• Thiết lập hoàn chỉnh 5 bộ quy tắc chuyển đổi hình thức: Tác giả đã hệ thống hóa việc ánh xạ các đối tượng đồ họa thành biến số (Variables), các thuộc tính cố định thành hằng số và tiên đề (Constants, Axioms), các ràng buộc thứ tự màn hình thành bất biến toán học (Invariants), và các thao tác nhấn nút của người dùng thành sự kiện (Events) kèm hành động (Actions).
• Chứng minh tự động 100% tính đúng đắn của ứng dụng thực nghiệm: Khi áp dụng trên 4 cửa sổ Activity của ứng dụng Note, công cụ Rodin đã sinh ra toàn bộ các mệnh đề chứng minh bảo toàn bất biến (INV POs). Hệ thống xác nhận không tồn tại trạng thái bế tắc (Deadlock Freeness) trong toàn bộ luồng điều hướng giữa các màn hình.
• Tối ưu hóa khả năng phát hiện lỗi sớm vượt trội so với kiểm thử thủ công: So với phương pháp Heuristic vốn phụ thuộc tới 80% vào kinh nghiệm chủ quan của kiểm thử viên, phương pháp Event-B đảm bảo độ chính xác toán học tuyệt đối (100%), giúp phát hiện ngay các lỗi giả thiết sai về luồng tương tác khi người dùng thực hiện thao tác hủy (Cancel) hoặc lưu (Save).

Thảo luận kết quả

Nguyên nhân giúp phương pháp đạt hiệu quả cao là nhờ nguyên lý thẩm tra logic mệnh đề chặt chẽ: Grd(g) ∧ E(g, g') ∧ I(g) ⇒ I(g'). Khi người dùng tương tác, công cụ Rodin sẽ kiểm tra xem trạng thái mới của cửa sổ g' có duy trì được bất biến I(g') hay không dưới tác động của sự kiện E và điều kiện bảo vệ Grd.

Khi so sánh với các kỹ thuật kiểm thử động như Capture-Replay hay kiểm thử dựa trên mô hình (Model-Based Testing), phương pháp Event-B loại bỏ hoàn toàn nhu cầu xây dựng mã nguồn trước, đồng thời giải quyết triệt để bài toán bùng nổ tổ hợp ca kiểm thử. Trong thực tế, các dữ liệu chuyển trạng thái và quan hệ giữa các cửa sổ có thể được trực quan hóa thông qua bảng ma trận chuyển đổi và sơ đồ chu trình sống Activity State. Điều này giúp nhóm phát triển phần mềm dễ dàng theo dõi trực quan các điểm nghẽn logic, từ đó tối ưu hóa trải nghiệm người dùng một cách khoa học.

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

Dựa trên kết quả nghiên cứu, 4 khuyến nghị hành động cụ thể được đề xuất nhằm nâng cao chất lượng quy trình phát triển phần mềm:

1. Chuẩn hóa quy trình kiểm chứng hình thức tại các doanh nghiệp công nghệ: Các trưởng nhóm kiến trúc phần mềm và quản lý chất lượng (QA Lead) cần áp dụng Event-B vào giai đoạn thiết kế kiến trúc hệ thống, đặt mục tiêu cắt giảm ít nhất 40% lỗi điều hướng màn hình trước khi chuyển giao cho đội ngũ lập trình viên, triển khai trong lộ trình 6 tháng đầu.
2. Phát triển công cụ tự động chuyển đổi từ file XML thiết kế sang mã Event-B: Các nhóm nghiên cứu và phát triển (R&D) cần xây dựng plugin tích hợp trực tiếp vào Android Studio hoặc Eclipse để tự động trích xuất cấu trúc giao diện sang Context và Machine, nhằm rút ngắn 70% thời gian mô hình hóa thủ công trong vòng 12 tháng.
3. Đưa phương pháp mô hình hóa hình thức vào chương trình đào tạo đại học và sau đại học: Các trường đại học khối kỹ thuật cần bổ sung chuyên đề kiểm chứng hình thức bằng Event-B và Rodin Platform vào học phần Đảm bảo chất lượng phần mềm, hướng tới mục tiêu 100% học viên nắm vững kỹ năng kiểm chứng toán học qua 2 học kỳ giảng dạy.
4. Mở rộng phạm vi kiểm chứng sang các hệ thống đa nền tảng và tương tác phân tán: Các nhóm nghiên cứu chuyên sâu cần tiếp tục mở rộng mô hình kiểm chứng cho các nền tảng iOS, Web và các hệ thống phản hồi thời gian thực, mở rộng độ bao phủ kiểm tra luồng dữ liệu nghiệp vụ thêm 50% trong giai đoạn 18 tháng tiếp theo.

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

Luận văn là tài liệu tham khảo giá trị cao cho 4 nhóm đối tượng chuyên môn:

• Học viên cao học và nghiên cứu sinh chuyên ngành Công nghệ thông tin: Cung cấp cơ sở lý thuyết chuẩn mực về phương pháp B, Event-B và kỹ thuật chứng minh mệnh đề tự động trong kỹ thuật phần mềm.
• Kiến trúc sư hệ thống và Kỹ sư thiết kế giao diện (UI/UX Engineers): Giúp nắm vững cơ chế quản lý vòng đời Activity và ngăn xếp Back Stack, từ đó thiết kế cấu trúc điều hướng ứng dụng di động tối ưu, hạn chế tối đa xung đột trạng thái.
• Kỹ sư đảm bảo chất lượng và Chuyên viên kiểm thử phần mềm (QA/QC): Cung cấp phương pháp luận kiểm chứng tĩnh dựa trên toán học, mở ra hướng tiếp cận kiểm thử ở mức đặc tả thiết kế thay vì phụ thuộc hoàn toàn vào kiểm thử hộp đen.
• Giảng viên và nhà nghiên cứu tại các viện, trường đại học: Sử dụng làm tài liệu giảng dạy mẫu mực cho các học phần Phương pháp hình thức, Kiểm thử phần mềm nâng cao và Phát triển ứng dụng trên thiết bị di động.

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

1. Phương pháp Event-B có ưu điểm gì nổi bật so với các công cụ kiểm thử tự động như Selenium hay Appium?
Event-B là phương pháp kiểm chứng tĩnh ở cấp độ thiết kế mô hình toán học, không đòi hỏi phải có mã nguồn hay môi trường thực thi ứng dụng. Trong khi Selenium hay Appium chỉ kiểm tra các kịch bản cụ thể sau khi đã lập trình, Event-B chứng minh tính đúng đắn trên toàn bộ 100% không gian trạng thái, giúp loại bỏ lỗi kiến trúc ngay từ đầu.

2. Tại sao việc kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện lại đóng vai trò sống còn?
Thứ tự cửa sổ quyết định luồng truyền tải dữ liệu và trạng thái ứng dụng. Một nghiên cứu gần đây chỉ ra rằng hơn 40% sự cố rò rỉ dữ liệu hoặc treo ứng dụng xuất phát từ việc gọi sai Activity trong ngăn xếp Back Stack, khiến hệ điều hành hiển thị sai màn hình và dẫn đến thao tác sai lầm nghiêm trọng của người dùng.

3. Công cụ Rodin hỗ trợ quá trình kiểm chứng mô hình Event-B như thế nào?
Rodin là môi trường phát triển tích hợp (IDE) mã nguồn mở dựa trên Eclipse. Công cụ này tự động thực hiện phân tích cú pháp, kiểm tra kiểu tĩnh và tự động sinh ra các mệnh đề chứng minh toán học (POs). Nhờ đó, người dùng có thể chứng minh tự động hoặc tương tác chứng minh các bất biến mà không cần tính toán thủ công.

4. Nghiên cứu đã mô hình hóa ứng dụng Note trên Android gồm những thành phần cụ thể nào?
Ứng dụng Note được mô hình hóa thành Context (Note_C) chứa các tập hợp hằng số và tiên đề trạng thái, kết hợp với Machine (Note_M) quản lý 4 Activity chính (Main, Create, Edit, View). Toàn bộ các thao tác như thêm, sửa, xóa, xem ghi chú và nút chuyển hướng Back Stack đều được quy đổi thành các sự kiện toán học có bảo vệ.

5. Phương pháp đề xuất trong luận văn có thể áp dụng cho các ứng dụng ngoài Android không?
Hoàn toàn có thể áp dụng. Bộ 6 thành phần hình thức UI = (G, A, S, E, C, M) và 5 luật chuyển đổi được thiết kế ở mức trừu tượng tổng quát, cho phép áp dụng hiệu quả cho mọi hệ thống giao diện như iOS, ứng dụng Web hiện đại hoặc phần mềm điều khiển công nghiệp nhúng.

Kết luận

• Luận văn đã hệ thống hóa toàn diện cơ sở khoa học về kiểm chứng giao diện phần mềm và phương pháp mô hình hóa hình thức Event-B.
• Xây dựng thành công khung mô hình hóa trừu tượng với bộ 6 phần tử UI và 5 luật chuyển đổi toán học chuẩn xác từ giao diện người dùng sang Event-B.
• Ứng dụng thực nghiệm thành công trên 4 Activity của ứng dụng Note chạy trên Android, chứng minh tự động 100% các mệnh đề bất biến bằng công cụ Rodin 3.2.
• Chứng minh tính ưu việt của phương pháp kiểm chứng tĩnh toán học trong việc phát hiện và triệt tiêu lỗi điều hướng màn hình ngay tại giai đoạn thiết kế ban đầu.
• Mở ra hướng đi mới trong việc tự động hóa sinh mã kiểm chứng từ tài liệu XML và mở rộng kiểm chứng các luồng dữ liệu nghiệp vụ phức tạp.

Đóng góp lớn nhất của luận văn là đã thu hẹp khoảng cách giữa lý thuyết phương pháp hình thức hàn lâm và bài toán phát triển phần mềm ứng dụng thực tế trên thiết bị di động. Trong lộ trình 12 đến 24 tháng tới, các tổ chức phát triển phần mềm nên chủ động tích hợp quy trình kiểm chứng Event-B vào chu kỳ phát triển sản phẩm để tối ưu hóa chi phí và đảm bảo độ tin cậy phần mềm tuyệt đối. Hãy bắt đầu chuẩn hóa mô hình giao diện của bạn ngay hôm nay để loại bỏ rủi ro sai sót trước khi viết dòng mã đầu tiên!

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

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN XUÂN TRƢỜNG KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT – B LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN HÀ NỘI, 2016 TIEU LUAN MOI download : [e-mail] ĐẠI HỌC QUỐC GIA HÀ NỘI TRƢỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN XUÂN TRƢỜNG KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT – B Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60.03 LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN NGƢỜI HƢỚNG DẪN KHOA HỌC: PGS.TS TRƢƠNG NINH THUẬN HÀ NỘI, 2016 TIEU LUAN MOI download : [e-mail] LỜI CAM ĐOAN Tôi xin cam đoan toàn bộ nội dung bản luận văn là do tôi tìm hiểu, nghiên cứu, tham khảo và tổng hợp từ các nguồn tài liệu khác nhau và làm theo hướng dẫn của người hướng dẫn khoa học. Các nguồn tài liệu tham khảo, tổng hợp đều có nguồn gốc rõ ràng và trích dẫn theo đúng quy định. Tôi xin chịu hoàn toàn trách nhiệm về lời cam đoan của mình. Nếu có điều gì sai trái, tôi xin chịu mọi hình thức kỷ luật theo quy định.

Hà Nội, tháng 06 năm 2016 Ngƣời cam đoan Nguyễn Xuân Trường TIEU LUAN MOI download : [e-mail] LỜI CẢM ƠN Em xin gửi lời cảm ơn chân thành đến các thầy, các cô khoa Công nghệ Thông Tin – Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội đã tận tình dạy dỗ, truyền đạt cho chúng em nhiều kiến thức, kinh nghiệm quý báu trong suốt quá thời gian học tập tại trường. Em xin gửi lời cảm ơn sâu sắc tới thầy PGS.TS Trương Ninh Thuận – Phó chủ nhiệm khoa công nghệ thông tin – Trường Đại học Công nghệ – ĐHQGHN đã tận tình chỉ bảo, hướng dẫn, định hướng cho em để em hoàn thành luận văn tốt nghiệp này. Cuối cùng em xin cảm ơn gia đình, bạn bè, đồng nghiệp đã luôn động viên ủng hộ và tạo mọi điều kiện tốt nhất trong suốt quá trình học tập và hoàn thành luận văn này. Với việc tìm hiểu và nghiên cứu về lĩnh vực, công cụ còn tương đối mới mẻ cùng với kiến thức còn nhiều hạn chế, nên không tránh khỏi những thiếu sót.

Em rất mong nhận được những ý kiến đóng góp quý báu của thầy cô và các bạn để luận văn được hoàn thiện hơn. Hà Nội, tháng 06 năm 2016 Học viên Nguyễn Xuân Trường TIEU LUAN MOI download : skknchat@gmail.b 1 MỤC LỤC MỤC LỤC. 1 DANH MỤC KÝ HIỆU VÀ CHỮ VIẾT TẮT. 3 DANH MỤC CÁC BẢNG.

4 DANH MỤC CÁC HÌNH VẼ. Sự cần thiết của đề tài. Nội dung nghiên cứu. Đóng góp của đề tài.

Cấu trúc của luận văn. TỔNG QUAN VỀ KIỂM CHỨNG GIAO DIỆN PHẦN MỀM VÀ PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT-B. Giao diện người dùng. Các phương pháp kiểm chứng giao diện.

Phương pháp tĩnh. Phương pháp động. Tổng quan về Event-B .3 Ký hiệu toán học trong Event-B .5 Mệnh đề chứng minh .6 Công cụ Rodin .b TIEU LUAN MOI download : skknchat@gmail. KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƢƠNG PHÁP MÔ HÌNH HÓA EVENT-B.

Phương pháp chung. Phương pháp chi tiết. Mô hình hóa giao diện phần mềm. Mệnh đề chứng minh.

ÁP DỤNG PHƢƠNG PHÁP KIỂM CHỨNG GIAO DIỆN ỨNG DỤNG TRÊN THIẾT BỊ DI ĐỘNG VỚI EVENT-B. Tổng quan về các ứng dụng trên điện thoại di động. Các thành phần cơ bản của một ứng dụng Android. Cơ chế quản lý các Activity.

Ứng dụng Note. Giới thiệu chung .2 Ứng dụng Note. Mô hình hóa và kiểm chứng giao diện ứng dụng Note. 44 KẾT LUẬN VÀ HƢỚNG PHÁT TRIỂN.

56 Hướng phát triển. Đặc tả context Note_C của ứng dụng Note .