Tóm tắt Luận văn Kiểm chứng giao diện phần mềm bằng phương pháp mô hình hóa Event – B

1 ĐẠ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.48.01.03 TÓM TẮT LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN HÀ NỘI, 2016 2 Chương 1. GIỚI THIỆU 1.1. Sự cần thiết của đề tài Ngày nay phần mềm có mặt trong hầu hết các lĩnh vực: Giáo dục, truyền thông, ngân hàng, sản xuất chế tạo, quản trị, y tế, khoa học kỹ thuật, Hàng không vũ trụ, giải trí, Giúp con người giải quyết hầu hết các công việc và dần thay thế con người. Đại đa số phần mềm hiện nay được xây dựng với một giao diện đồ họa người dùng Graphical User Interface (GUI) và con người sẽ làm việc thông qua tương tác với giao diện của phần mềm. Người sử dụng thường quan tâm tới giao diện dễ sử dụng và có tính thẩm mỹ đảm bảo được các chức năng. Tuy nhiên không phải lúc nào các GUI của phần mềm khi được xây dựng điều đảm bảo được tính dễ dùng, bố cục hợp lý, các chức năng hoạt động một cách chính xác như dự kiến hay trả lại kết quả như mong muốn. Những lỗi phát sinh trong quá trình tương tác như: Các phần tử trên GUI hiển thị bất thường khó quan sát và thao tác, các chức năng thực hiện không như dự định, các thông báo hiển thị sai, thứ tự xuất hiện của các cửa sổ không chính xác,, dẫn tới thực hiện sai, gây mất mát dữ liệu, gây mất an toàn có thể nguy hại tới tính mạng con người và thiệt hại về kinh tế,... Vì vậy, Cần phải thực hiện kiểm thử giao diện phần mềm để kiểm tra các chức năng, sự nhất quán, khả năng tầm nhìn, khả năng tương thích đảm bảo phù hợp với các thông số trong đặc tả thiết kế, phát hiện và sửa chữa kịp thời các lỗi hoặc bất cứ vấn đề bất thường nào có thể có trước khi đưa ra lưu hành, làm giảm các chi phí sửa chữa và bảo trì. Lỗi hiển thị sai các cửa sổ giao diện là tương đối nghiêm trọng. Các cửa sổ giao diện đại diện cho bộ mặt của ứng dụng phần mềm, là nơi chứa và hiển thị các phần tử giao diện thông qua đó người dùng có thể tương tác, trao đổi nhập xuất 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 một 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 3 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 điều này gây ra những hậu quả khó lường. Nhận thấy được tầm quan trọng của việc kiểm chứng giao diện người dùng của phần mềm mà cụ thể là kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện người dùng, nên tác giả đã mạnh dạn đề xuất đề 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” nhằm nghiên cứu phương pháp kiểm chứng thứ tự của các cửa sổ giao diện phần mềm một cách tự động dựa trên Event-B và thực hiện áp dụng cho giao diện ứng dụng trên thiết bị di động. 1.2. Nội dung nghiên cứu Đề tài tập trung vào việc nghiên cứu 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. Nghiên cứu 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ý, cách sử dụng công cụ Rodin. Từ những nghiên cứu có được đưa ra một phương pháp mô hình hóa và kiểm chứng chung cho kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện người dù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, xây dựng các mô hình 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 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. 1.3. Đóng góp của đề tài 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 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 4 không hợp lý về 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. 1.4. Cấu trúc của luận văn Phần nội dung của luận văn được cấu trúc thành 7 chương chính như sau: Chương 1. GIỚI THIỆU Giới thiệu về các yêu cầu khách quan, chủ quan, cơ sở khoa học, thực tiễn nghiên cứu và xây dựng đề tài. Chương 2. TỔNG QUAN VỀ KIỂM CHỨNG GIAO DIỆN PHẦN MỀM Giới thiệu một cách chi tiết về giao diện phần mềm cũng như các vấn đề về kiểm chứng giao diện phần mềm, các phương pháp kiểm chứng giao diện. Chương 3. PHƯƠNG PHÁP MÔ HÌNH HÓA EVENT-B Bao gồm những kiến thức tổng quan về phương pháp mô hình hóa Event- B, mô tả cấu trúc của mô hình, các thành phần, giải thích ý nghĩa của các thành phần, cấu trúc của mệnh đề chứng minh và phân loại. Nêu rõ tập các ký hiệu toán học trong cú pháp của mô hình. Trình bày cách sử dụng và kiểm chứng tự động với công cụ Rodin. Chương 4: KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƯƠNG PHÁP EVENT-B Tập trung vào việc xây dựng mô hình kiểm chứng chung cho các giao diện ứng dụng như: xây dựng quy trình thực hiện, xây dựng mô hình chung trên các định nghĩa, đưa ra các luật chuyển đổi tổng quát và mệnh đề chứng minh tổng quát chung. Chương 5. ÁP DỤNG PHƯƠNG PHÁP KIỂM CHỨNG GIAO DIỆN ỨNG DỤNG NOTE VỚI EVENT-B 5 Trình bày tổng quan về Android và ứng dụng Note. Áp dụng phương pháp đã nghiên cứu được vào mô hình hóa và kiểm chứng thứ tự các cửa sổ cửa ứng dụng Note. Soạn thảo mô hình thu được và kiểm chứng tự động với công cụ Rodin. Chương 6. KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN Kết luận tổng thể về các kết quả đã đạt được của luận văn và hướng phát triển tiếp theo. Chương 7. PHỤ LỤC Trình bày một cách chi tiết về các mô hình trong Event-B của ứng dụng Note đã chuyển đổi và mô hình hóa 6 Chương 2. TỔNG QUAN VỀ KIỂM CHỨNG GIAO DIỆN PHẦN MỀM 2.1. Giao diện người dùng GUI cung cấp cho người dùng một giao tiếp khác với các chương trình máy, biến các chương trình phức tạp trở nên dễ dùng hơn so với giao diện dòng lệnh. Một ví dụ minh họa về GUI và giao diện dòng lện thể hiện trong Hình 2.3 và Hình 2.4. Hình 2.3 Giao diện đồ họa người dùng Hình 2.4 Giao diện dòng lệnh 2.2. Các phương pháp kiểm chứng giao diện 2.2.1. Kiểm chứng giao diện người dùng bằng tay 2.2.2. Kiểm chứng giao diện người dùng tự động 7 Chương 3. PHƯƠNG PHÁP MÔ HÌNH HÓA EVENT-B 3.1. Tổng quan về Event-B Một mô hình có thể chỉ chứa các contexts hoặc các machines hoặc là cả hai loại. Mối quan hệ và cấu trúc của machines và contexts được thể hiện trong Hình 3.1 [4]. Hình 3.1. Cấu trúc mối và quan hệ của các thành phần mô hình trong Event-B. 3.2 Context Context dùng để đặc tả những phần tĩnh của mô hình, mỗi context trong Event-B có một tên duy nhất. Context được tạo thành từ các mệnh đề được mô tả trong Hình 3.2 [4]: Hình 3.2. Cấu trúc của một context. MACHINE .. REFINES .. SEES . VARIABLES .. INVARIANTS .. VARIANT . EVENTS .. END CONTEXT .. EXTENDS .. SETS .. CONSTANTS . AXIOMS .. THEOREMS .. END Sees CONTEXT .. EXTENDS .. SETS .. CONSTANTS . AXIOMS .. THEOREMS .. END 8 3.3 Machine Một machine trong Event-B phải có một tên duy nhất và khác với tất cả các context và machine trong mô hình. Một machine được cấu tạo bởi các thành phần là các mệnh đề được mô tả trong Hình 3.4 [4]. Hình 3.4. Cấu trúc của machine trong Event-B. Hình 3.5. Cấu trúc của Event trong Event-B. 3.4 Ký hiệu toán học trong Event-B  Các phép toán logic bậc nhất: Bảng 3.1 mô tả các phép toán. Từ các phép toán logic cơ sở tạo nên các biểu thức logic được gọi là các vị từ trong các invariants và trong các ràng buộc (guards) của event trong mô hình của Event-B. Bảng 3.1: Các phép toán logic Tên phép toán Ký hiệu Tuyển  MACHINE .. REFINES .. SEES . VARIABLES .. INVARIANTS .. VARIANT . EVENTS .. END EVENT REFINES ANY WHERE WITH THEN END 9 Hội  Phủ định  Kéo theo  Tương đương  Lượng từ với mọi  Lượng từ tồn tại   Các phép toán tập hợp: phép hợp , phép giao , phép hiệu \, quan hệ bao hàm , quan hệ thuộc .  Các kiểu dữ liệu  Kiểu nguyên là kiểu dữ liệu số được ký hiệu là ℤ.  Kiểu logic ký hiệu là BOOL chỉ nhận một trong 2 giá trị BOOL={TRUE, FALSE}.  Kiểu tập hợp do người dùng định nghĩa.  Kiểu tập con của một tập ký hiệu là ℙ. 3.5 Tinh chỉnh Tinh chỉnh (refinement) là giai đoạn cài đặt hay cụ thể hóa một machine hoặc một context trừu tượng thành một machine hoặc một context cụ thể hơn, chi tiết hơn bằng việc bổ sung vào các yếu tố cụ thể [9] [4]. Hình 3.8 là ví dụ mô tả mối quan hệ giữa machine và context trừu tượng và các tinh chỉnh của chúng. Hình 3.8 Ví dụ về mối quan hệ Refinement trong Event-B M M M C0 1 C0 1 C refines extend see s see s see s see s refines 10 3.6 Mệnh đề chứng minh Mệnh đề cần chứng minh POs (Proof Obligations) là những biểu thức logic mà cần được chứng minh trong mô hình Event-B, việc chứng minh nhằm đảm bảo các machine là an toàn. POs được thực hiện một cách tự động nhờ công cụ Rodin Platform vì vậy người ta còn gọi là chứng minh tự động. Các mệnh đề chứng minh trong Event-B được mô tả thành các luật chứng minh và được định nghĩa thành các loại khác nhau như: Invariant preservation (INV), Variant (VAR), Deadlock Freeness (DLF), Theorem (THM), well-definedness (WD),, chúng được sinh ra tự động trong Rodin. Để xác định các luật theo từng sự kiện thì ta sử dụng hệ thống sơ đồ định nghĩa sự kiện như Hình 3.9 [9] [4]. Hình 3.9 Sơ đồ định nghĩa sự kiện 3.7 Công cụ Rodin Trong luận văn này sử dụng phiên bản Rodin 3.2 cập nhật ngày 22/09/2015 là một IDE dựa trên Eclipse được cung cấp hỗ trợ xây dựng, tinh chỉnh, mô hình hóa và chứng minh các mô hình trong Event-B [9]. Hình 3.11 là ví dụ về giao diện của bộ công cụ này [9]. Hình 3.11. Giao diện đồ họa của công cụ Rodin. 11 Chương 4. KIỂM CHỨNG GIAO DIỆN PHẦN MỀM BẰNG PHƯƠNG PHÁP MÔ HÌNH HÓA EVENT-B 4.1. Phương pháp chung Quy trình mô hình hóa vào kiểm chứng giao diện với phương pháp Event- B là quá trình chuyển đổi các thành phần tương ứng của giao diện như các yêu cầu, thuộc tính, đặc tả, ràng buộc sang các yếu tố, thành phần trong cấu trúc mô hình của Event-B, sau đó biên tập và kiểm chứng tự động bằng công cụ Rodin. Quy trình tổng quát của phương pháp được thể hiện trong sơ đồ Hình 4.1. Hình 4.1. Quy trình kiểm chứng tổng quát Từ quy trình tổng quát của phương pháp trong Hình 4.1 ta đi thực hiện cụ thể hóa nó bằng các bước cụ thể hơn được mô tả trong Hình 4.2. 12 Hình 4.2 Quy trình kiểm chứng chi tiết 4.2. Mô hình hóa giao diện phần mềm Giao diện người sử dụng của một phần mềm nó bao gồm các cửa sổ đối tượng thuộc cửa sổ, trạng thái của các cửa sổ và đối tượng, sự kiện hoặc tập các sự kiện trên các đối tượng cửa sổ, các thông báo. Chúng ta có thể mô hình hóa và định nghĩa một cách trừu tượng các thành phần của giao diện qua một số định nghĩa như sau:  Định nghĩa 1: Một giao điện ứng dụng cơ bản là một bộ 6 UI=<G, A, S, E, C, M> trong đó G là tập các cửa sổ giao điện, A là tập các hành động, S là tập các trạng thái, E là tập các sự kiện, C là tập các ràng buộc, M là tập các thông báo.  Định nghĩa 2: Một cửa sổ giao diện là một bộ 7 g ∈ G, g=<P, A, O, S_g, E_g, C_g, M_g> trong đó P là tập các thuộc tính, A là tập các hành động, O là tập các đối tượng trên giao diện, S_g là tập các trạng thái của cửa sổ, E_g là tập các sự kiện của g, C_g là tập các ràng buộc của g, M_g là tập các thông báo có trong g. 13  Định nghĩa 3: Một đối tượng trên giao diện o ∈ O là một bộ 5 o = <p_o, a_o, s_o, e_o, c_o> trong đó p_o là tập các thuộc tính của đối tượng o, a_o là tập các hành vi có thể có của o, s_o là tập các trạng thái của o, e_o là tập các sự kiện của o, c_o là tập các ràng buộc mà o cần tuân theo. Từ các định nghĩa cơ bản trên đi xây dựng một tập các luật chuyển đổi, để chuyển đổi từ một mô hình giao diện ứng dụng sang một mô hình trong Event- B, chuyển đổi được thể hiện trong Bảng 4.1. Các luật chuyển đổi được mô tả cụ thể như sau:  Luật 1: Giao diện ứng dụng UI= sẽ được chuyển thành một machine và một context trừu tượng trong Event-B: <UM, UC>. Trong đó e ∈ E là một sự kiện của máy UM.  Luật 2: Các thuộc tính của cửa sổ và các đối tượng trên cửa sổ sẽ được chuyển thành các biến VARIABLES.  Luật 3: Các thành phần hằng, tĩnh không thay đổi của giao diện sẽ chuyển thành các CONSTANTS, SET và quy định, quy ước phải tuân theo của chúng tương ứng thành AXIOMS trong context.  Luật 4: Các ràng buộc về thứ tự xuất hiện của cửa sổ sẽ được chuyển thành các INVARIANTS.  Luật 5: Các hành động của các cửa sổ khi sự kiện xảy ra sẽ được chuyển thành các sự kiện EVENT và các Action trong sự kiện của machine trong Event-B. Bảng 4.1. Chuyển đổi từ GUI tới Event-B Tên Mô tả Mô hình hóa Luật 1 UI = UC, UM Luật 2 O, Properties Variables Luật 3 Thành phần tĩnh, hằng Constants, Set, Axiom Luật 4 Ràng buộc Invariant Luật 5 Action, sự kiện Event, Action 14 4.3. Mệnh đề chứng minh Giao diện phần mềm UI = ta có chuyển tương ứng thành máy UM và UC với x ∈ 𝐺 là một biến trạng thái của mô hình thể hiện cửa sổ hiện tại, e ∈ 𝐸 là sự kiện và x’ là cửa sổ mới được chuyển tới khi sự kiện e xảy ra. Trạng thái cửa sổ hiện tại trước và sau khi sự kiện xảy ra có thể mô tả một cách không hình thức x :| E(x, x’) Dựa trên luật 4 ta có ràng buộc bất biến tương ứng I(x) và I(x’). Điều kiện để sự kiện xảy ra được ký hiệu là Grd(x). Ta có thể định nghĩa nhiệm vụ chứng minh POs như sau: Grd(x)  E(x, x’)  I(x’) Hay có thể viết Grd(x), I(x) I(x’) 15 Chương 5. ÁP DỤNG PHƯƠNG PHÁP KIỂM CHỨNG GIAO DIỆN ỨNG DỤNG NOTE VỚI EVENT-B 5.1. Tổng quan về các ứng dụng trên điện thoại di động 5.1.1 Các thành phần cơ bản của một ứng dụng Android Các thành phần tạo nên một ứng dụng Android được chia làm 6 loại bao gồm [10]:  Activity.  Service.  Content Provider.  Intent.  Broadcast Receiver.  Notification. 5.1.2. Cơ chế quản lý các Activity Actitvity là thành phần quan trọng nhất và đóng vai trò chính trong xây dựng ứng dụng Android. Hệ điều hành Android quản lý Activity theo dạng stack. Mỗi lần một Activity mới được khởi chạy thì Activity trước đó bị stop và hệ thống sẽ lưu Activity stop này vào một back stack. Back stack kể trên được mô tả trong Hình 5.1, được tổ chức theo đúng tiêu chí của một stack, đó là “vào sau, ra trước” [10]. Hình 5.1 Cơ chế Back Stack Vòng đời của một Activity được thể hiện qua sơ đồ Activity State Hình 5.2 [10]. 16 Hình 5.2 Activity State 5.2. Ứng dụng Note 5.2.1. Giới thiệu chung 5.2.2 Ứng dụng Note Ứng dụng bao gồm 4 cửa sổ giao diện chính (4 Activity) gồm: MainActivity, EditActivity, CreateActivity, ViewActivity trong đó MainActivity là màn hình giao diện chính xuất hiện đầu tiên khi ứng dụng bắt đầu khởi động được mở [12] các đặc tả của từng giao diện được mô tả như sau:  MainActivity  EditActivity  CreateActivity 17  ViewActivity 5.3. Mô hình hóa và kiểm chứng giao diện ứng dụng Note Áp dụng các bước trong quy trình của phương pháp giao diện ứng dụng được mô hình hóa thành 2 thành phần trong Event-B machine và context: . Dựa vào đặc tả thiết kế giao diện trong mục 5.2.2 và cơ chế hoạt động của một ứng dụng Android trong mục 5.2.1, ta thực hiện xây dựng sơ đồ hoạt động “Activity Diagram” quy trình này mô tả bởi Hình 5.7. Hình 5.7. Quy trình xây dựng Activity Diagram Sơ đồ Activity Diagram cho ứng dụng Note sau khi xây dựng được mô tả trong Hình 5.8 Đặc tả, bản thiết kế GUI của ứng dụng Android Sự kiện & Hành động Activity & Thành phần Vòng đời Activity Mô hình back stack Sơ đồ hoạt động của GUI Chuyển đổi 18 Hình 5.8. Sơ đồ Activity Diagram MainActivity Start CreateActivity Start MainActivity Stop MainActivity Stop MainActivity Stop MainActivity Pause EditActivity Start ViewActivity Start CreateActivity Stop EditActivity Stop ViewActivity Stop [Exit Application] [Select MenuContext] Cancel Save Cancel Save [Create true] [Create false] [Edit true] [Edit false] [View true] [Delete true] [D e lete N o te ] 19 Quá trình mô hình hóa có thể được mô tả một cách khái quát qua Hình 5.9. Hình 5.9 Quá trình mô hình hóa từ Activity Diagram tới Event-B Mô hình hóa và chuyển đổi vào context Note_C ta định nghĩa tập các giao diện G={ main , Create , Edit , View}, tập các trạng thái của các cửa sổ giao diện S={start, active, stop, pause, killed}. Hình 5.10 là đoạn chương trình mô tả context trong Rodin. Event-B Đặc tả, bản thiết kế của GUI Action:  Click  Chagne Properties:  Security Constraints Machine Variables  Invariants Events Context  SET  CONSTANT  AXIOMS EVENT-B Constant  Statuts Properties Object  Window  Controller  stop Mô hình Event-B trừu tượng Mô hình Event-B cho ứng dụng cụ thể Sự kiện & Ràng buộc & thành phần mô hình Tinh chỉnh Luật chuyển đổi 20 Hình 5.10. Context Note_C Mô hình hóa và chuyển đổi vào machine Note_M ta có các biến main_activity, Create_activity, Edit_activity, View_activity, các ràng buộc về thứ tự của các giao diện từ Activity Diagram, các sự kiện sẽ được chuyển đổi thành các INVARIANTS, EVENT, ACTION tương ứng:  INVARIANTS 21  Hình 5.11. Một phần của machine Note_M  EVENT, ACTION  Event thoát ứng dụng.  Event chọn chức năng gọi cửa sổ Create.  Event chọn chức năng gọi cửa sổ Edit.  Event chọn chức năng gọi cửa sổ View.  Event chọn chức năng xóa và chuyển về cửa sổ Main.  Các sự kiện trên trên các đối tượng. của các cửa sổ. MACHINE Note_M SEES Note_C VARIABLES Main_activity Edit_activity View_activity Create_activity Select INVARIANTS inv1 : Main_activity ∈ S inv2 : Edit_activity ∈ S inv3 : View_activity ∈S inv4 : Create_activity ∈ S inv5 : Main_activity=active ∧ Create_activity=stop ∧ Edit_activity=stop ∧ View_activity=stop inv6 : Main_activity=stop ∧ Create_activity=active ∧ Edit_activity=stop ∧ View_activity=stop inv7 : Main_activity=stop ∧ Create_activity=stop ∧ Edit_activity=active ∧ View_activity=stop inv8 : Main_activity=stop ∧ Create_activity=stop ∧ Edit_activity=stop ∧ View_activity=active inv9 : Main_activity=start ⇒ (Create_activity=start) ∧ (Edit_activity=start) ∧ (View_activity=start) inv10 : ¬(Main_activity=start) ⇒¬(Create_activity=start) ∧ ¬(Edit_activity=start) ∧ ¬(View_activity=start) inv11 : Select ∈ Menu EVENTS INITIALISATION ≙ STATUS ordinary BEGIN act1 : Main_activity ≔ start act2 : Edit_activity ≔ start act3 : View_activity ≔ start act4 : Create_activity ≔ start act5 : Select ≔ Null END 22 Thực hiện soạn thảo trong công cụ Rodin, sinh và kiểm chứng tự động các mệnh đề cần chứng minh. Hình 5.18. Cửa sổ sinh kiểm chứng tự động Kết quả của quá trình sinh và kiểm chứng tự động được thể hiện qua bảng Statistics, Hình 5.19 cho thấy toàn bộ các ràng buộc được chứng minh đảm bảo mục tiêu thiết kế thứ tự của các giao diện đã đặt ra. Hình 5.19. Bảng kết quả Statistics 23 Chương 6. KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN 6.1. Kết luận Khi các hệ thống tin học hoá ngày càng đi vào đời sống con người thì vấn đề thiết kế giao diện càng trở nên quan trọng trong việc phát triển phần mềm. Trên cơ sở đó luận văn đã tập trung vào nghiên cứu phương pháp kiểm chứng giao diện ứng dụng bằng phương pháp mô hình hóa Event-B. Có nhiều phương pháp kiểm chứng giao diện đã và đang được người phát triển sử dụng như kiểm thử bằng tay, kiểm thử tự động. Mỗi một phương pháp điều có những ưu nhược điểm riêng. Kiểm thử bằng tay thường sử dụng cho việc thử nghiệm lần đầu, thăm dò nhưng tỏ ra không hiệu quả khi quá trình kiểm thử cần lặp lại ca kiểm thử nhiều lần. Kiểm thử tự động khắc phục được những hạn chế của kiểm thử bằng tay nhưng tốn kém hơn, chi phí đầu tư ban đầu lớn. Kiểm thử thủ công bằng tay là không thể thay thế vì chúng ta không thể tự động hóa mọi thứ. Hiện tại hầu như tất cả các tổ chức, công ty phát triển phần mềm đều lựa chọn kiểm thử thủ công cho mọi sản phẩm. Tuy nhiên các công cụ kiểm thử tự động cũng có những điểm mạnh nhất định mà kiểm thử thủ công bằng tay không có, nên cần xem xét hoàn cảnh để có thể áp dụng kiểm thử tự động cho quá trình kiểm thử phần mềm. Trong quá trình nghiên cứu luận văn đã tập trung vào tìm hiểu về giao diện phần mềm, các cơ chế, đặc điểm, các phương pháp kiểm chứng hiện có. Nghiên cứu phương pháp mô hình hóa Event-B và công cụ kiểm chứng tự động Rodin. Xây dựng một quy trình tổng quát để mô hình hóa và kiểm chứng thứ tự xuất hiện của giao diện ứng dụng phần mềm, xây dựng các định nghĩa, luật chuyển đổi từ mô hình giao diện trừu tượng sang Event-B tổng quát. Áp dụng vào kiểm chứng giao diện của ứng dụng Note trên thiết bị di động. Nghiên cứu bước đầu dừng lại ở việc kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện mà chưa thể kiểm chứng các ràng buộc trên các đối tượng của từng cửa sổ giao diện. 24 6.2. Hướng phát triển Từ những quy trình, mô hình, phương pháp tổng quát đã xây dựng và áp dụng kiểm chứng tự động trên ứng dụng cụ thể với công cụ Rodin. Với những nghiên cứu đạt được của luận văn. Có thể nghiên cứu phát triển để xây dựng thêm và bổ sung thêm các mô hình quy trình tổng quát và áp dụng để kiểm chứng không chỉ thứ tự của cửa sổ giao diện mà còn trên nhiều thành phần khác nhau của giao diện ứng dụng và trên nhiều loại giao diện ứng dụng hơn không chỉ là mobile mà có thể là Window Form hoặc là giao diện Web. Chương 7. PHỤ LỤC 7.1. Đặc tả context Note_C của ứng dụng Note 7.2. Đặc tả machine Note_M của ứng dụng Note 25 TÀI LIỆU THAM KHẢO [1] GUI Testing Techniques: A Survey Imran Ali Qureshi an AamerNadeem, International Journal of Future Computer and Communication, Vol. 2, No. 2, April 2013. [2] Cem Kaner, James Bach, Bret Pettichord, Lessons Learned in Software Testing. A Context-Driven Approach, John Wiley & Sons, 2001. [3] [BEI90] Beizer, B., Software Testing Techniques, 2d ed., Van Nostrand Reinhold, 1990. [4] J.-R. Abrial, Modeling in Event-B: System and Software Engi-neering. Cambridge University Press, 2010. [5] A.F. Memon, GUI testing pitfalls and process, Computer, University of Maryland, 2002. [6] D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, 2006. [7] Christophe M´etayer, Laurent Voisin, the Event-B Mathematical Language, 2007. [8] [9] [10] [11] lap-trinh-android-voi-database-sqlite. [12]