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

ng cụ hoặc thực đơn.  Số lượng các thao tác chọn và các thao tác chọn kết hợp.  Các phím tắt và các tùy chọn nâng cao.  Tính logic của giao diện  Phạm vi của vùng dữ liệu vào/ra  Input box.  Check box.  Drop down window list.  Button lựa chọn.   Hành vi của giao diện được cài đặt chặt chẽ với từng bối cảnh  Khi người dùng gọi trình tự các chức năng trên GUI.  Quá trình kiểm chứng giao diện người dùng của ứng dụng để phát hiện nếu ứng dụng có chức năng không chính xác. Kiểm chứng giao diện áp dụng các kỹ thuật kiểm thử, các kỹ thuật kiểm thử này đề cập đến việc thiết lập các nhiệm vụ thực hiện và so sánh kết quả cùng với kết quả dự kiến và khả năng lặp lại cùng một tập các nhiệm vụ nhiều lần với dữ liệu đầu vào khác nhau và cùng một mức độ chính xác. Kiểm chứng giao diện thực hiện kiểm tra cách xử lý ứng dụng bàn phím và chuột sự kiện, làm thế nào các thành phần GUI khác nhau như: menubars, thanh công cụ, hộp thoại, nút nhấn, hình ảnh, sự kiện..., khi người sử dụng tương tác có thực hiện theo đúng cách mong muốn hay không. Thực hiện kiểm chứng giao diện cho ứng dụng sớm trong chu kỳ phát triển phần mềm sẽ tăng tốc độ phát triển, cải thiện chất lượng và giảm thiểu rủi ro về phía 14 cuối của chu kỳ. Kiểm chứng giao diện có nhiều phương pháp khác nhau mỗi phương pháp sẽ có những ưu nhược điểm riêng, có thể được thực theo hướng tĩnh hoặc động và có thể áp dụng tương ứng nhiều kỹ thuật kiểm thử một cách thủ công hoặc có thể được thực hiện tự động với việc sử dụng một chương trình phần mềm. 2.2.1. Phương pháp tĩnh Trong phương pháp này áp dụng kỹ thuật phân tích tĩnh, kiểm thử bằng tay dựa trên kinh nghiệm và kiến thức của người kiểm thử, nó được thực hiện bởi chính người kiểm thử. Phương pháp Heuristic được sử dụng trong kiểm thử bằng tay, trong đó một nhóm các chuyên gia nghiên cứu các phần mềm để tìm ra vấn đề. Màn hình giao diện được kiểm thử bằng tay bởi các người kiểm thử, những hành động và phản hồi của giao diện được so sánh với mục tiêu thiết kế và các yêu cầu của người sử dụng, sự khác biệt giữa mong đợi của người sử dụng và các bước thiết kế thiết kế cần thiết bởi giao diện, khả năng sử dụng của giao diện. Việc kiểm thử bằng tay giúp phát hiện nhiều lỗi qua mỗi ca kiểm thử, lỗi được tìm thấy sẽ cung cấp gợi ý để tìm lỗi khác, có thể tìm được những lỗi mà các phương pháp chứng tự động khó có thể tìm thấy. Kiểm thử bằng tay thường được sử dụng tốt cho kiểm thử giao diện ứng dụng đầu, thăm dò. Mặt khác kiểm chứng bằng tay thường tỏ ra không hiệu quả và gây tốn thời gian khi việc kiểm chứng cần lặp lại ca kiểm thử nhiều lần, phụ thuộc vào kiến thức và khả năng của người kiểm thử [1]. 2.2.2. Phương pháp động Phương pháp thường áp dụng một số kỹ thuật kiểm thử và kiểm thử giao diện tự động như kỹ thuật kiểm thử black-box (hộp đen) với các mô hình black- box được sử dụng để tạo các ca kiểm thử cho kiểm thử giao diện, phương pháp động là quy trình áp dụng nhiều kỹ thuật và công cụ kiểm thử thực hiện một tập hợp các nhiệm vụ kiểm chứng tự động và so sánh kết quả thu được với đầu ra mong đợi. Kỹ thuật kiểm chứng giao diện tự động được áp dụng là một giải 15 pháp khắc phục cho tất cả các vấn đề mà kiểm thử giao diện bằng tay trong kiểm chứng tĩnh còn chưa làm được. Phương pháp áp dụng kiểm thử tự động được thực hiện thông qua các công cụ được xây dựng sẵn miễn phí hoặc mất phí:  Công cụ Capture-Replay: là một công cụ nắm bắt và chạy lại các thử nghiệm đã chụp của phiên làm việc của người sử dụng (đầu vào và các sự kiện) và lưu trữ chúng trong các kịch bản (mỗi phiên) phù hợp sẽ được sử dụng để chạy lại các phiên người dùng. Hoạt động bằng hai chế độ tương tác thực hiện khác nhau và cung cấp lợi thế kiểm tra đầu ra, đầu ra của ca kiểm thử được ghi lại [1].  Unit-Testing frameworks: cung cấp sự linh hoạt, hỗ trợ kiểm tra hướng phát triển và thực hiện công việc kiểm tra tự động.  Model based testing: Một mô hình là một mô tả đồ họa hành vi của hệ thống. Nó giúp người phát triển hiểu và dự đoán các hành vi hệ thống. Mô hình giúp tạo các ca sử dụng kiểm thử hiệu quả các yêu cầu của hệ thống. Theo nhu cầu sử dụng để được xem xét để thử nghiệm mô hình này dựa trên thực thi phiên làm việc của người sử dụng lựa chọn từ một mô hình của giao diện, quá trình này gồm: xây dựng mô hình, xác định đầu vào cho mô hình, tính toán kết quả dự kiến cho các mô hình, chạy thử nghiệm, so sánh kết quả thực tế với kết quả dự kiến, quyết định về hành động khác trên mô hình. 16 2.3. Tổng quan về Event-B Event-B được phát triển bởi tác giả J.R Abrial, là một phương pháp hình thức để mô hình hóa và phân tích hệ thống phân cấp, được phát triển từ phương pháp B. Event-B sử dụng chủ yếu các ký hiệu toán học, logic mệnh đề, lý thuyết tập hợp để mô hình hóa hệ thống. Cho phép tinh chỉnh mô hình hóa hệ thống theo các mức từ trừu tượng tới cụ thể và sử dụng các chứng minh toán học để xác minh tính nhất quán giữa các mức độ tinh chỉnh. Các ký hiệu, cú pháp của Event-B có thể được soạn thảo và chứng minh tự động bằng công cụ Rodin Platfrom được tích hợp trong Eclipse-IDE (Integrated Development Environment), Công cụ Rodin hỗ trợ cho phép soạn thảo các ký hiệu và chứng minh các tính chất toán học một cách hiệu quả, là một công cụ mã nguồn mở được cập nhật liên tục tại trang web Event-B.org [9]. Một mô hình Event-B thường mã hóa các hệ thống chuyển đổi trạng thái trong đó các biến sẽ đại diện cho các trạng thái, các sự kiện event đại diện cho việc chuyển từ trạng thái tới một trạng thái khác của hệ thống. Một mô hình trong Event-B được tạo thành bởi hai loại thành phần cơ bản sau: machines và context. Machines bao gồm các phần đặc tả động của mô hình, trong khi đó contexts chứa các phần đặc tả tĩnh của mô hình. 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. Machines và contexts có các mối quan hệ qua lại với nhau: một machine có thể refined bởi một machine khác và một context có thể extended bởi một context khác, một machine có thể sees một hoặc một vài context. Mối quan hệ và cấu trúc của machines và contexts được thể hiện trong Hình 2.3. [4]. 17 Hình 2.3. Cấu trúc mối và quan hệ của các thành phần mô hình trong Event-B. 2.3.1 Context Context dùng để đặc tả những phần tĩnh của một mô hình, mỗi context trong Event-B có một tên duy nhất. Một context có thể tham chiếu tới các thành phần được định nghĩa trong context mà nó extends. Context được tạo thành từ các mệnh đề được mô tả trong Hình 2.4. các mệnh đề này được định nghĩa như sau [4]:  Mệnh đề “Extends” chỉ ra một danh sách các context mà context hiện tại mở rộng  Mệnh đề “Sets” chỉ một tập hợp các mô tả chìu tượng và liệt kê các loại, kiểu.  Mệnh đề “Constants” là một danh sách các hằng số được đưa vào context. Hằng số trong các context và trong các context mà extends từ nó phải có định danh khác nhau.  Mệnh đề “Axioms” là một danh sách các vị từ (gọi là tiên đề) của các hằng số trong các biểu thức logic. Các axioms sẽ được sử dụng làm giả thuyết trong các mệnh đề chứng minh Pos (Proof obligations).  Mệnh đề “Theorems” là một danh sách các biểu thức logic gọi là định lý và là thành phần cần chứng minh trong context. MACHINE .. REFINES .. SEES . VARIABLES .. INVARIANTS .. VARIANT . EVENTS .. END CONTEXT .. EXTENDS .. SETS .. CONSTANTS . AXIOMS .. THEOREMS .. END Sees refines refines sees extends sees Machine Machine Context Context extends 18 Hình 2.4. Cấu trúc của một context. Hình 2.5 là một ví dụ về một context có tên là Array dùng để tìm kiếm một giá trị trong một mảng có kích thước n và a hằng số đại diện tên mảng, x là giá trị cần tìm. Hình 2.5. Ví dụ context trong Event-B. 2.3.2 Machine Dùng để đặc tả những thành phần động của mô hình, 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 CONTEXT .. EXTENDS .. SETS .. CONSTANTS . AXIOMS .. THEOREMS .. END CONTEXT Array CONSTANTS n //array size a //the array to search in x //value to search in a AXIOMS axm1: n ∈ axm2: a ∈ 1 .. n axm3: x ∈ END 19 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 2.6 và định nghĩa như sau [4]:  Mệnh đề “Refines” gồm các machine trừu tượng mà machine hiện tại tinh chỉnh từ các machine đó.  Mệnh đề “Sees” là một danh sách các context mà machine tham chiếu tới. Machine có thể sử dụng các tập hợp và các hằng số được định nghĩa rõ ràng trong các context mà được khai báo trong mệnh đề sees của nó  Mệnh đề “Variables” là một danh sách các biến khác nhau được sử dụng trong machine, các biến phải không được trùng tên. Tuy nhiên không giống như trong context một số biến có thể trùng tên với các biến trong machine trừu tượng.  Mệnh đề “Invariants” là một danh sách các biểu thức logic toán học khác nhau gọi là các vị từ mà các biến phải thỏa mãn. Mỗi invariants sẽ được gán một nhãn.  Mệnh đề “Events” gồm một danh sách các events của machine. Một event tạo ra một hành động làm thay đổi giá trị và trạng thái của các biến. Một event trong Event-B sẽ được cấu thành bởi một ràng buộc G (t, v) và một hành động A (t, v) với t là một tham số nào đó và v là biến. Hình 2.7 mô tả cấu trúc của event. 20 Hình 2.6. Cấu trúc của machine trong Event-B. Hình 2.7. Cấu trúc của Event trong Event-B.  Các hành động của sự kiện có thể biểu diễn dưới dạng xác định hoặc không xác định, có thể có nhiều hành động trong một sự kiện. Hình 2.8 là một ví dụ về machine và Hình 2.9 là ví dụ về event. Hình 2.8 Ví dụ machine trong Event-B MACHINE .. REFINES .. SEES . VARIABLES .. INVARIANTS .. VARIANT . EVENTS .. END EVENT REFINES ANY WHERE WITH THEN END 21 Hình 2.9 Ví dụ Event trong Event-B 2.3.3 Ký hiệu toán học trong Event-B Phương pháp mô hình hóa Event-B sử dụng ngôn ngữ toán học cơ sở để mô hình hóa gồm logic bậc nhất và lý thuyết tập hợp cơ sở cùng với các kiểu dữ liệu, có thể thấy ngôn ngữ toán học đóng một vai trò vô cùng quan trọng trong mô hình Event-B [4].  Các phép toán logic bậc nhất cơ bản gồm: Phép tuyển , phép hội , phép phủ định , phép kéo theo , tương đương , lượng từ với mọi , lượng từ tồn tại . Bảng 2.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 các event trong mô hình của Event-B. Bảng 2.1: Các phép toán logic Tên phép toán Ký hiệu Tuyển  Hội  Phủ định  Kéo theo  Tương đương  Lượng từ với mọi  Lượng từ tồn tại  22  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à ℙ. 2.3.4 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 đặc tả [9] [4]. Một machine có thể refines một machine trừu tượng, một context có thể extends một context trừu tượng nào đó. Một event trong machine trừu tượng có thể được refines thành một hoặc một số sự kiện trong machine cụ thể. Các thành phần của machine và context trừu tượng được sử dụng trong các machine và context tương ứng refines và extends từ chúng. Hình 2.10 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 2.10 Ví dụ về mối quan hệ Refinement trong Event-B M0 M2 M1 C01 C01 C1 refines extends sees sees sees sees refines extends 23 2.3.5 Mệnh đề chứng minh Mệnh đề chứng minh POs (Proof Obligations) là những biểu thức logic mà cần phải đượ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. Rodin thực hiện kiểm tra tĩnh (bao gồm phân tích từ vựng, phân tích cú pháp, loại kiểm tra) các machine và context và sau đó đưa ra những mệnh đề cần chứng minh và đưa vào trong một file để chứng minh tự động [4]. 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ì có thể sử dụng hệ thống sơ đồ định nghĩa sự kiện như Hình 2.11 [9]. Hình 2.11 Sơ đồ định nghĩa sự kiện  Ví dụ Invariant preservation proof obligation rule (INV): luật chứng minh này đảm bảo rằng mỗi bất biến invariant trong machine được bảo quản bởi một sự kiện event. Nếu cho một sự kiện evt và một bất biến inv(s, c, v) thì mệnh đề chứng minh có tên là “evt / inv / INV” và với sự kiện được định nghĩa như Hình 2.12 thì sẽ có luật tương ứng sẽ được thể hiện trong Bảng 2.2 [4]. evt any x where G(s, c, v, x) then v:| BA(s, c, v, x, v ’ ) end 24 Hình 2.12 Định nghĩa sự kiện evt Bảng 2.2 Luật chứng minh INV với sự kiện evt Axioms và theorems Invariants và theorems Guards của event Vị từ trước và sau khi sự kiện Thay đổi của các bất biến A(s, c) I (s, c, v) G(s, c, v, x) BA(s, c, v, x, v’) inv(s, c, v’) evt/inv/INV 2.3.6 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]. Rodin là bộ cung cụ mã nguồn mở bao gồm trình soạn thảo, thực thi, tự động tạo bộ chứng minh, tài liệu hỗ trợ,, với giao diện đồ họa trực quan trong môi trường Eclipse nó sẽ là công cụ lý tưởng để xây dựng các mô hình của Event-B. Hình 2.13 là ví dụ về giao diện của bộ công cụ này. evt any x where G(s, c, v, x) then v:| BA(s, c, v, x, v ’ ) end 25 Hình 2.13. Giao diện đồ họa của công cụ Rodin.  Menu bar Cung cấp các phương thức hỗ trợ, chỉnh sửa tập tin và các chức năng đặc biệt khác của Event-B. Menu bar Được mô tả trong Hình 2.16 bao gồm một số mục quan trọng trọng [9]: o Event-B menu: khi người dùng mở machine hoặc context sẽ xuất hiện một số trình thuật sĩ cho phép tạo một số yếu tố có sẵn trong mô hình Event-B cho người dùng.  Tool bar: cung cấp các phím tắt cho các lệnh quen thuộc như lưu, in, hủy và phục hồi thao tác. Các thanh công cụ cũng cung cấp các phím tắt cho các trình thuật sĩ để tạo ra các yếu tố như tiên đề, các hằng số, liệt kê bộ,...  Editor View: chứa các hoạt động biên tập của Event-B.  Symbols View: được thiết kế để cung cấp cho người dùng một cách thuận tiện để thêm các biểu tượng toán học cho các biên tập mô hình khác nhau. Nếu một trình biên tập được mở và một file văn bản đang hoạt động (con trỏ nhấp nháy ), nhấp chuột vào một biểu tượng thì sẽ chèn nó ở vị trí hiện tại, Symbols View được mô tả trong Hình 2.14. 26  Event-B Explorer Cửa sổ này cho phép người phát triển quản lý các dự án của mình như truy cập mở, đóng, tạo mới hoặc xóa bỏ. Cửa sổ thường nằm bên trái của màn hình nhưng cũng có thể thay đổi nếu người dùng muốn. Giao diện của Event- B Explorer được mô tả trong Hình 2.15 [9]. Hình 2.14. Symbols View Hình 2.15 Event-B Explorer Hình 2.16. Menu bar 27 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 Giao diện phần mềm nói chung và giao diện của các ứng dụng trên thiết bị di động nói riêng, thường thiết kế gồm các đối tượng để người dùng tương tác lấy thông tin, thao tác của người dùng nên các đối tượng sẽ phát sinh ra các sự kiện và hành động được cài đặt sẵn sẽ thực thi một công việc nào đó sau khi sự kiện xảy ra. Các đối tượng thường là: Cửa sổ, Text Box, Combo Box, List Box, Radio Button/Option Button, Check Box/Tick Box, Report, Sử dụng phương pháp mô hình hóa Event-B để mô hình hóa và kiểm chứng thứ tự xuất hiện của các cửa sổ giao sẽ giúp người phát triển hiểu rõ hơn, kiểm tra được tính đúng đắn và phát hiện ra những lỗi trên các cửa sổ giao diện không mong muốn. Quy trình mô hình hóa và kiểm chứng giao diện tổng quát bằng 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 về thứ tự thực hiện của các cửa sổ sang các yếu tố, thành phần trong cấu trúc mô hình của mô hình trong 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 3.1. Hình 3.1. Quy trình kiểm chứng tổng quát 28 3.2. Phƣơng pháp chi tiết Từ quy trình tổng quát của phương pháp trong Hình 3.1 ta đi thực hiện cụ thể hóa nó bằng các bước chi tiết cụ thể hơn được mô tả trong Hình 3.2 trong đó:  Đặc tả, bản thiết kế của GUI: là những tài liệu đặc tả về thiết kế, những yêu cầu về chức năng mong muốn sẽ xây dựng của giao diện.  Mô hình GUI trừu tƣợng: là mô hình trừu tượng tổng quát cho các giao diện ứng dụng phần mềm, mô hình được xây dựng thông qua các định nghĩa được mô tả trong mục 3.3.  Mô hình Event-B trừu tƣợng: là mô hình trừu tượng chung có được dựa trên chuyển đổi từ các luật được định nghĩa trong mục 3.3 và bảng 3.1.  Sơ đồ hoạt động: là sơ đồ thể hiện thứ tự thực hiện và hoạt động của các cửa sổ giao diện như mong muốn của người thiết kế.  Mô hình Event-B cho ứng dụng cụ thể: là mô hình cụ thể có được khi thực hiện mô hình hóa trên một ứng dụng cụ thể dựa trên các mô hình trừu tượng và các luật chuyển đổi. Tùy theo loại ứng dụng sẽ có cách xây dựng tương ứng.  Mệnh đề chứng minh (POs) tổng quát: là mệnh đề tổng quát chung của giao diện cần phải chứng minh hay xác minh, mệnh đề được xây dựng ở mục 3.4. Các bước thực hiện của quy trình chi tiết trong Hình 3.2 được đánh dấu bằng các số thứ tự và được thực hiện như sau: bước đầu tiên là đi xây dựng một mô hình hóa giao diện một cách trừu tượng chung cho các giao diện ứng dụng bằng cách đưa ra các định nghĩa tổng quát. Bước thứ hai từ những định nghĩa tổng quát đi xây dựng các luật mô hình hóa chuyển đổi tương ứng từ mô hình của giao diện sang mô hình trong Event-B bước này chính là bước tinh chỉnh mô hình trừu tượng, từ kết quả bước một và các luật đưa ra mục tiêu cần chứng minh chung, qua bước 2 ta thu được các quy tắc chuyển đổi tổng quát cho thành phần trong mô hình giao diện vào Event-B kết quả của bước này sẽ được sử 29 dụng để làm khung tham chiếu và kết hợp với kết quả của bước số 4 để tạo ra một bản mô hình hóa đặc tả giao diện hoàn chỉnh trong Event-B. Bước số 3 và số 4 tùy vào giao diện của mỗi ứng dụng cụ thể cần thể cần mô hình hóa cùng với bản đặc tả thiết kế kèm với những giả thuyết về giao diện và chức năng của nó từ đó chuyển đổi thành biểu đồ hoạt động tương ứng của ứng dụng, từ sơ đồ này có thể thấy được nguyên lý hoạt động và các thứ tự mà khi thực thi giao diện theo đặc tả, kết quả thu được sẽ dùng cho bước tiếp theo. Bước số bốn từ sơ đồ hoạt động có được kết hợp thêm đặc tả thiết kế để đem mô hình hóa bằng việc tham chiếu tới các luật chuyển đổi ở bước hai để đặc tả sang các thành phần tương ứng trong Event-B ở bước này thì tùy thuộc vào ứng dụng mà sẽ có những chuyển đổi thích hợp, kết quả của bước này tạo ra một mô hình trong Event-B có thể gồm một hoặc nhiều thành phần machine và context. Bước năm tại đây đem mô hình đã thu được ở bước bốn tham chiếu vào mô hình trừu tượng ở bước hai để đảm bảo tuân thủ các định nghĩa và luật, tinh chỉnh để thu được mô hình cuối cùng là các machine và context cụ thể, đem kết quả đưa vào công cụ Rodin. Bước số 6 sử dụng công cụ Rodin tạo tự động các mục tiêu cần chứng minh Pos và thực hiện kiểm chứng tự động. Bước 7 từ kết quả thu được ở bước 6 sẽ kết hợp với biểu đồ hoạt động ban đầu đưa ra kết quả kiểm chứng để đánh giá sự vi phạm hay không các yêu cầu về giao diện đã đặt ra và từ đó để có những chỉnh sửa phù hợp. 30 Hình 3.2 Quy trình kiểm chứng chi tiết 31 3.3. 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.  Đị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 3.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. 32  Luật 3: Các thành phần như thuộc tính, cửa sổ, đối tượng, trạng thá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 3.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 thuộc tính, trạng thái Constants, Set, Axiom Luật 4 Ràng buộc Invariant Luật 5 Action, sự kiện Event, Action Công đoạn mô hình hóa này là đi thực hiện bước 1 và 2 trong quy trình Hình 3.2. 3.4. Mệnh đề chứng minh Từ những định nghĩa và luật ở mục 3.2 ta đi xác định mục tiêu cần chứng minh POs thông qua các ràng buộc về thứ tự của cửa sổ giao diện của phần mềm. Giao diện phần mềm UI = ta có chuyển đổi tương ứng thành hai thành phần trong mô hình của Event-B là machine và context: với g ∈ là cửa sổ hiện tại, e ∈ là sự kiện và g’ 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 g :| E(g, g’) Dựa trên luật 4 ta có ràng buộc bất biến tương ứng I(g) và I(g’). Điều kiện để sự kiện xảy ra 33 được ký hiệu là Grd(g). Ta có thể định nghĩa nhiệm vụ chứng minh POs như sau: Grd(g)  E(g, g’)  I(g)  I(g’) Hay có thể viết Grd(x), E(g, g’), I(g) I(g’) 34 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 Sự bùng nổ về công nghệ thông tin và việc gia tăng sử dụng điện thoại di động, kèm với sự cạnh tranh mạnh mẽ trong lĩnh vực công nghệ điện thoại di động gần đây đã tạo ra bước phát triển cũng như là những hướng đi mới đó là lập trình trên thiết bị di động đã và đang trở thành một lĩnh vực đầy tiềm năng. Có rất nhiều nền tảng, các hệ điều hành khác nhau mà chúng ta có thể dựa trên đó để xây dựng ứng dụng như IOS, Android, Windows Phone, Nhưng hiện nay đối với những nhà phát triển và các lập trình viên muốn xây dựng một ứng dụng di động một cách nhanh chóng, hiệu quả và có một thị trường tiềm năng thì Android là một lựa chọn tuyệt vời [10]. Android là một trong các hệ điều hành được ưa chuộng nhất hiện nay, có tính bảo mật cao, hỗ trợ nhiều công nghệ tiên tiến, tương thích với nhiều phần cứng và liên tục được cập nhật và phát triển bởi google. Với ưu thế là mã nguồn mở và được đông đảo cộng đồng yêu thích, Android đã thu hút rất nhiều nhà phát triển từ khắp mọi nơi trên thế giới và đang dần khẳng định vị thế. Nhờ Android mà hàng loạt các ứng dụng games, ứng dụng di động gia tăng một cách nhanh chóng. Để phát triển ứng dụng trên nền Android thì người lập trình cần có kiến thức nền tảng về Java cùng với bộ công cụ hỗ trợ đi kèm tương đối mạnh có giao diện đồ họa dễ sử dụng và luôn được cập nhật như Eclipse, Android Studio, Genymotion, các bộ thư viện JDK, Android SDK,, chúng được cung cấp một cách hoàn toàn miễn phí cho người phát triển và tất cả mọi người. 35 4.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 đại diện cho một màn hình duy nhất với một giao diện người dùng mà ở đó người dùng có thể quan sát và tương tác. Ví dụ như một ứng dụng email có một Activity hiển thị danh sách các email, một Activity khác cung cấp một giao diện để soạn thảo email, và một Activity khác nữa cung cấp một giao diện để đọc email,  Service là thành phần chạy ẩn trong Android. Service sử dụng để update dữ liệu, đưa ra các cảnh báo (Notification) và không bao giờ hiển thị cho người dùng thấy.  Content Provider kho dữ liệu chia sẻ. Content Provider được sử dụng để quản lý và chia sẻ dữ liệu giữa các ứng dụng.  Intent nền tảng để truyền tải các thông báo. Intent được sử dụng để gửi các thông báo đi nhằm khởi tạo 1 Activity hay Service để thực hiện công việc mong muốn. VD: khi mở 1 trang web, ta gửi 1 Intent đi để tạo 1 Activity mới hiển thị trang web đó.  Broadcast Receiver thành phần thu nhận các Intent bên ngoài gửi tới. VD: nếu viết 1 chương trình thay thế cho phần gọi điện mặc định của Android, khi đó ta cần 1 Broadcast Receiver để nhận biết các Intent là các cuộc gọi tới.  Notification đưa ra các cảnh báo mà không làm cho các Activity phải ngừng hoạt động. 4.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: khi một Activity mới được khởi tạo, nó sẽ được xếp lên đầu của stack và trở thành running activity, các Activity trước đó sẽ bị tạm dừng và chỉ hoạt động 36 trở lại khi Activity mới được giải phóng. Một Activity có thể khởi chạy các Activity khác. 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. Việc quay lại các Activity trước đó (khi người dùng nhấn vào nút back trên thiết bị chẳng hạn) thì hệ thống chỉ đơn giản lấy các Activity đã lưu trữ trong back stack, và Activity được lấy trong back stack này tiếp tục sẽ được hiển thị lên màn hình người dùng. Back stack kể trên được mô tả trong Hình 4.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 4.1 Cơ chế Back Stack [10]. Activity bao gồm 4 state [10]: - active (running): Activity đang hiển thị trên màn hình (foreground). - paused: Activity vẫn hiển thị (visible) nhưng không thể tương tác (lost focus). - stop: Activity bị thay thế hoàn toàn bởi Activity mới sẽ tiến đến trạng thái stop. - killed: Khi hệ thống bị thiếu bộ nhớ, nó sẽ giải phóng các tiến trình theo nguyên tắc ưu tiên hoặc khi kết thúc ứng dụng. Vòng đời của một Activity được thể hiện qua sơ đồ Activity State Hình 4.2 [10]. 37 Hình 4.2 Activity State [10]. 38 4.2. Ứng dụng Note 4.2.1. Giới thiệu chung Trong cuộc sống hàng ngày chúng ta thường có quá nhiều mối bận tâm và công việc cần phải giải quyết, đôi khi chúng ta không thể nhớ hết những công việc cần làm những sự kiện cần tham gia hay bất cứ một điều gì mà quan trọng mà cần nhớ để khắc phục được điều đó thì ứng dụng tạo ghi chú là một công cụ và lựa chọn hoàn hảo giúp giải quyết những vấn đề đó. Ứng dụng Note là một ứng dụng tạo ghi chú chạy trên nền tảng hệ điều hành Android có chứa những chức năng cơ bản nhất của một ứng dụng tạo ghi chú bao gồm thêm, sửa, xóa, xem các ghi chú [12]. 4.2.2 Ứng dụng Note Được xây dựng nhằm mục đích tạo các ghi chú của người dùng với cấu trúc cơ sở dữ liệu gồm một bảng có tên là Note có cấu trúc được mô tả trong Bảng 4.1 [11]. Bảng 4.1: Bảng CSDL ghi chú Note Tên cột Kiểu dữ liệu Ràng buộc Mô tả Note_Id int Primary Key Khóa chính Note_Title text Ghi chú ngắn Note_Content text Nội dung ghi chú Ứ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ở.  Cửa sổ giao diện MainActivity 39 Cửa sổ giao diện MainActivit chứa các đối tượng khác nhau được mô tả một cách tổng quan như trong Bảng 4.2 và có thể thấy một cách chi tiết hơn thông qua Hình 4.3 là file mã lệnh XML thiết kế của giao diện. Bảng 4.2: Mô tả cửa sổ giao diện MainActivity Component Mô tả Loại Attribute  Name: MainActivity  Type: Activity  Layout: RelativeLayout Status  Active (Running)  Paused  Stop  Killed Object Control ListView ListView Control (hiển thị danh sách các note) BtnCreate Button Control BtnExit Button Control ContextMenu Menu Control Event BtnexitClicked Button_Click BtncreateClicked Button_Click FocusListview ClickContext Menu RefreshListview 40 Hình 4.3. MainActivit.XML  Cửa sổ giao diện CreateActivity Cửa sổ giao diện CreateActivity chứa các đối tượng khác nhau được mô tả một cách tổng quan như trong Bảng 4.3 và có thể thấy một cách chi tiết hơn thông qua Hình 4.4 là file mã lệnh XML thiết kế của giao diện. Bảng 4.3: Mô tả sơ bộ các đối tượng của cửa sổ giao diện CreateActivity Component Mô tả Loại Attribute  Name: CreateActivity  Type: Activity  Layout: RelativeLayout Status  Active (Running)  Paused  Stop 41  Killed Object Control Texttitle Edittext Control Textcontent Edittext Control Btncancel Button Control Btnsave Button Control Event buttonSaveClicked Button_Click buttonCancelClicked Button_Click Hình 4.4 CreateActivit.XML  Cửa sổ giao diện EditActivity Cửa sổ giao diện EditActivit chứa các đối tượng khác nhau được mô tả một cách tổng quan như trong Bảng 4.4 và có thể thấy một cách chi tiết hơn thông qua Hình 4.5 là file mã lệnh XML thiết kế của giao diện. 42 Bảng 4.4: Mô tả sơ bộ các đối tượng của cửa sổ giao diện EditActivity Component Mô tả Loại Attribute  Name: EditActivity  Type: Activity  Layout: RelativeLayout Status  Active (Running)  Paused  Stop  Killed Object Control Texttitle Edittext Control Textcontent Edittext Control Btncancel Button Control Btnsave Button Control Event buttonSaveClicked Button_Click buttonCancelClicked Button_Click Hình 4.5 EditActivit.XML 43  Cửa sổ giao diện ViewActivity Cửa sổ giao diện ViewActivit chứa các đối tượng khác nhau được mô tả một cách tổng quan như trong Bảng 4.5 và có thể thấy một cách chi tiết hơn thông qua Hình 4.6 là file mã lệnh XML thiết kế của giao diện. Bảng 4.5: Mô tả sơ bộ các đối tượng của cửa sổ giao diện ViewActivity Component Mô tả Loại Attribute  Name: ViewActivity  Type: Activity  Layout: RelativeLayout Status  Active (Running)  Paused  Stop  Killed Object Control Texttitle Edittext Control Textcontent Edittext Control BtnBack Button Control Event buttonCancelClicked Button_Click Hình 4.6 ViewActivity.XML 44 4.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 chi tiết trong mục 3.2 ta có giao diện ứng dụng Note được mô hình hóa thành 2 thành phần trong Event-B machine và context: . Dựa trên đặc điểm và cơ chế của ứng dụng di động trong mục 4.1.2 và 4.1.2 ta có quy trình xây dựng sơ đồ hoạt động được mô tả trong Hình 4.7. Hình 4.7. Quy trình xây dựng sơ đồ hoạt động Sơ đồ hoạt động thể hiện thứ tự xuất hiện của các cửa sổ giao diện của ứng dụng Note sau khi xây dựng được mô tả trong Hình 4.8. Đặc tả, yêu cầu thiết kế GUI 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 45 Hình 4.8. Sơ đồ hoạt động 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 elete N o te] 46 Từ đặc tả của ứng dụng Note kết hợp với mô hình giao diện trừu tượng chung, các luật chuyển đổi đã trình bày tại Chương 3 ta đi mô hình hóa, chuyển đổi và tinh chỉnh tương ứng các thành phần vào trong machine và context của Event-B. Các thuộc tính, cửa sổ, trạng thái thì sẽ chuyển thành các biến. Các ràng buộc về thứ tự xuất hiện và điều kiện cần thỏa mãn chuyển thành các bất biến, các tiền điều kiện để sự kiện có thể xảy ra sẽ chuyển thành các bảo vệ, các sự kiện và hành động tương ứng sẽ chuyển thành các event và action trong Event-B. Quá trình mô hình hóa có thể được mô tả qua Hình 4.9. Hình 4.9 Quá trình mô hình hóa từ đặc tả vào trong Event-B Event-B Sơ đồ hoạt động của GUI Action:  Click Properties:  Security Constraints Machine Variables  Invariants Events Context  SET  CONSTANT  AXIOMS EVENT-B Constant  Statuts Properties Object  Window  Controller  stop Đặc tả, thiết kế của GUI 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 47 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 4.10 là đoạn chương trình mô tả context trong Rodin. Hình 4.10. Context Note_C Mô hình hóa và chuyển đổi vào machine Note_M ta có các biến đại diện cho các cửa sổ 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ừ sơ đồ hoạt động, các sự kiện sẽ được chuyển đổi thành các INVARIANTS, EVENT, ACTION tương ứng, các đối tượng nút nhấn chuyển thành các biến ButSave, ButCancel, ButExit và được biểu diễn tương ứng Hình 4.11 là một phần của machine Note_M:  INVARIANTS  (main_activity=start) (Create_activity= start)  (Edit_activity= start)  ( View_activity=start). 48  (main_activity=active)  (Create_activity=stop)  (Edit_activity=stop)  ( View_activity=stop).  (main_activity=killed) (Create_activity= killed)  (Edit_activity= killed)  ( View_activity= killed).  (Create_activity=active)  (main_activity=stop)  (Edit_activity=stop)  ( View_activity=stop).  (Edit_activity=active)  (main_activity=stop)  (Create_activity=stop)  ( View_activity=stop).  (View_activity=active)  (main_activity=stop)  (Create_activity=stop)  ( Edit_activity=stop).  49 Hình 4.11. Một phần của machine Note_M 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 50  EVENT, ACTION  Event thoát ứng dụng thể hiện trong Hình 4.12. Hình 4.12 Event thoát ứng dụng  Event chọn chức năng gọi cửa sổ Create thể hiện trong Hình 4.13. Hình 4.13 Event chọn chức năng Create  Event chọn chức năng gọi cửa sổ Edit thể hiện trong Hình 4.14. Hình 4.14 Event chọn chức năng Edit BtnExit_Click ≙ STATUS ordinary WHEN grd1 : (BtnExit=TRUE)∧(Main_activity=active) THEN act1 : Main_activity≔killed act2 : Operator≔Exit act3 : Edit_activity≔killed act4 : Create_activity≔killed act5 : View_activity≔killed END Select_Create ≙ STATUS ordinary WHEN grd1 : (Main_activity=active) THEN act1 : Create_activity≔active act2 : Main_activity≔stop act3 : Select≔Create END Select_Edit ≙ STATUS ordinary WHEN grd1 : Main_activity=active THEN act1 : Edit_activity≔active act2 : Main_activity≔stop act3 : Select≔Edit END 51  Event chọn chức năng gọi cửa sổ View thể hiện trong Hình 4.15. Hình 4.15 Event chọn chức năng View  Event chọn chức năng xóa và chuyển về cửa sổ Main thể hiện trong Hình 4.16. Hình 4.16 Event chọn chức năng Delete  Các sự kiện trên trên các đối tượng của các cửa sổ thể hiện trong Hình 4.17 Select_View ≙ STATUS ordinary WHEN grd1 : Main_activity=active THEN act1 : View_activity≔active act2 : Main_activity≔stop act3 : Select≔View END Select_Delete ≙ STATUS ordinary WHEN grd1 : Main_activity=active THEN act1 : Operator≔Del act2 : Main_activity≔active END Edit_Saveclick ≙ STATUS ordinary WHEN grd1 : Edit_activity=active ∧ Select=Edit ∧ BtnSave=TRUE THEN act1 : Operator≔Save act2 : Main_activity≔active act3 : Select≔Null act4 : Edit_activity≔stop act5 : BtnSave≔FALSE END 52 Hình 4.17. Các Event trên các đối tượng của các cửa sổ Edit_Canelclick ≙ STATUS ordinary WHEN grd1 : Edit_activity=active ∧ Select=Edit∧BtnCancel=TRUE THEN act1 : Operator≔Cancel act2 : Main_activity≔active act3 : Select≔Null act4 : Edit_activity≔stop act5 : BtnCancel≔FALSE END Create_Saveclick ≙ STATUS ordinary WHEN grd1 : Create_activity=active ∧ Select=Create ∧BtnSave=TRUE THEN act1 : Operator≔Save act2 : Main_activity≔active act3 : Select≔Null act4 : Create_activity≔stop act5 : BtnSave≔FALSE END Create_Cancelclick ≙ STATUS ordinary WHEN grd1 : Create_activity=active ∧ Select=Create∧BtnCancel=TRUE THEN act1 : Operator≔Save act2 : Main_activity≔active act3 : Create_activity≔stop act4 : Select≔Null act5 : BtnCancel≔FALSE END View_backclick ≙ STATUS ordinary WHEN grd1 : View_activity=active ∧ Select=View∧BtnBack=TRUE THEN act1 : Main_activity≔active act2 : View_activity≔stop act3 : Select≔Null act4 : BtnBack≔FALSE END 53 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 4.18 minh họa việc sinh tự động. Toàn bộ mã lệnh sẽ được trình bày chi tiết trong phần Phụ lục của luận văn. Hình 4.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 4.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 4.19. Bảng kết quả Statistics 54  Không phải lúc nào các đặc tả khi thiết kế cũng điều đúng đắn và không lỗi, giả sử trong trường hợp của ứng dụng Note trên trong đặc tả thiết kế chức năng chọn lệnh chỉnh sửa trong thực đơn nhưng sự kiện được đặc tả tương ứng lại chuyển tới cửa sổ khác View mà lại không phải Edit như mong muốn trong thiết kế như trong Hình 4.20. Trong trường hợp này công cụ Rodin lập tức xuất hiện biểu tượng dấu “?” trước vị trí không được chứng minh thể hiện trong Hình 4.21 và Hình 4.22, điều đó tương đương với tại vị trí đặc tả đó chưa thỏa đáng hoặc có lỗi nào đó và dựa vào đây để người phát triển tìm và xem xét để có những cập nhật phù hợp. Hình 4.20 Sự kiện chọn chức năng chỉnh sửa Hình 4.21 Thông báo mệnh đề chưa chứng minh được tự động Select_Edit ≙ STATUS ordinary WHEN grd1 : Main_activity=active THEN act1 : View_activity≔active act2 : Main_activity≔stop act3 : Select≔Edit END 55 Hình 4.22 Cửa sổ Goal Hình 4.23 Cửa sổ Statistics trong trường hợp lỗi 56 KẾT LUẬN VÀ HƢỚNG PHÁT TRIỂN 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 đề kiểm chứng và xây dựng phần mềm nói chung và giao diện người dùng của phần mềm nói riêng có thể đảm bảo các yếu tố chất lượng ngày 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. Giao diện đồ họa người dùng GUI là giao diện phổ biến mà từ đó người dùng có thể tương tác với hệ thống phần mềm. Kiểm chứng giao diện người dùng thường là một công việc phức tạp và không hề dễ dàng do bản chất của giao diện đồ họa không chỉ chứa các đối tượng đồ họa mà còn có rất nhiều các sự kiện điều khiển có thể có những sự kiện không mong muốn mà người kiểm chứng không thể lường trước được. Thông qua việc kiểm chứng người phát triển có thể phát hiện ra những sai sót để có những khắc phục kịp thời đảm bảo có được phần mềm chất lượng và có một giao diện dễ dùng. Hiện nay nhiều phương pháp kiểm chứng giao diện đã và đang được người phát triển, mỗi một phương pháp đều có những ưu nhược điểm riêng. Với khả năng mô hình hóa mạnh mẽ của phương pháp mô hình hóa Event-B dựa trên các ký pháp toán học kết hợp với bộ công cụ mã nguồn mở Rodin hỗ trợ cho việc biên tập, tự động sinh và kiểm chứng một cách chính xác thì việc nghiên cứu, xây dựng phương pháp kiểm chứng và mô hình hóa giao diện ứng dụng phần mềm với Event-B là một hướng đi thiết thực. Luận văn đã tập trung vào tìm hiểu về các đặc điểm của giao diện phần mềm, các cơ chế, đặc trưng, các phương pháp kiểm chứng hiện có. Tập trung 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, từ đó xây dựng quy trình tổng quát, xây dựng quy trình chi tiết, đưa ra mô hình giao diện người dùng trừu tượng, xây dựng tập luật chuyển đổi từ mô hình GUI trừu tượng sang 57 mô hình Event-B tổng quát, thực hiện 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. Áp dụng vào kiểm chứng thứ tự xuất hiện của các cửa sổ giao diện của ứng dụng trên thiết bị di động. Nghiên cứu bước đầu đã đưa ra được phương pháp, mô hình tổng quát chung cho việc kiểm chứng giao diện phần mềm và dừng lại ở việc kiểm chứng, phát hiện các lỗi về thứ tự xuất hiện của các cửa sổ giao diện giúp người phát triển có những điều chỉnh phù hợp, nhưng chưa thể kiểm chứng các ràng buộc trên các thành phần khác của giao diện, công việc chuyển đổi từ đặc tả vào mô hình và từ mô hình vào công cụ rodin vẫn còn thủ công chưa được thực hiện một cách tự động. 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 và phát triển để xây dựng thêm, bổ sung thêm vào các mô hình quy trình để áp dụng và kiểm chứng không chỉ là thứ tự xuất hiện của các cửa sổ giao diện mà còn trên nhiều tiêu chí khác của nhiều thành phần khác nhau trên giao diện ứng dụng, hoặc hơn thế nữa là áp dụng với nhiều loại giao diện ứng dụng hơn không chỉ là các ứng dụng trên thiết bị di động mà có thể là trên giao diện Window Form hoặc là giao diện Web. 58 CONTEXT Note_C SETS S Menu P CONSTANTS active stop pause killed Null start Create Edit View Delete None Exit Save Cancel Del AXIOMS axm1 : partition(S, {active}, {stop}, {pause}, {killed}, {start}) axm2 : partition(Menu,{Null},{Create}, {Edit}, {View}, {Delete}) axm3 : partition(P, {None}, {Exit}, {Save}, {Cancel}, {Del}) END PHỤ LỤC A. Đặc tả context Note_C của ứng dụng Note B. Đặc tả machine Note_M của ứng dụng Note MACHINE Note_M SEES Note_C VARIABLES Main_activity Edit_activity View_activity Create_activity Select BtnExit BtnSave 59 BtnCancel Operator BtnBack 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 : Create_activity=active⇒ Main_activity=stop ∧ Edit_activity=stop ∧ View_activity=stop inv7 : Edit_activity=active⇒ Main_activity=stop ∧ Create_activity=stop ∧ View_activity=stop inv8 : View_activity=active ⇒ Main_activity=stop ∧ Edit_activity=stop ∧ Create_activity=stop 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 inv12 : BtnExit ∈ BOOL inv13 : BtnSave ∈ BOOL inv14 : BtnCancel ∈ BOOL inv15 : Main_activity=killed ⇒ (Create_activity=killed) ∧ (Edit_activity=killed) ∧ (View_activity=killed) inv16 : Operator ∈ P inv17 : BtnBack ∈ BOOL inv18 : Select=Edit⇒Edit_activity=active inv19 : Select=View⇒View_activity=active inv20 : Select=Create⇒Create_activity=active EVENTS INITIALISATION ≙ STATUS ordinary BEGIN act1 : Main_activity ≔ start act2 : Edit_activity ≔ start act3 : View_activity ≔ start act4 : Create_activity ≔ start act5 : Select ≔ Null act6 : BtnExit ≔ FALSE act7 : BtnSave ≔ FALSE act8 : BtnCancel ≔ FALSE act9 : Operator ≔ None act10 : BtnBack ≔ FALSE END BtnExit_Click ≙ STATUS ordinary WHEN grd1 : (BtnExit=TRUE)∧(Main_activity=active) THEN act1 : Main_activity≔killed act2 : Operator≔Exit act3 : Edit_activity≔killed act4 : Create_activity≔killed act5 : View_activity≔killed END 60 Select_Create ≙ STATUS ordinary WHEN grd1 : (Main_activity=active) THEN act1 : Create_activity≔active act2 : Main_activity≔stop act3 : Select≔Create END Select_Edit ≙ STATUS ordinary WHEN grd1 : Main_activity=active THEN act1 : Edit_activity≔active act2 : Main_activity≔stop act3 : Select≔Edit END Select_View ≙ STATUS ordinary WHEN grd1 : Main_activity=active THEN act1 : View_activity≔active act2 : Main_activity≔stop act3 : Select≔View END Select_Delete ≙ STATUS ordinary WHEN grd1 : Main_activity=active THEN act1 : Operator≔Del act2 : Main_activity≔active END Edit_Saveclick ≙ STATUS ordinary WHEN grd1 : Edit_activity=active ∧ Select=Edit ∧ BtnSave=TRUE THEN act1 : Operator≔Save act2 : Main_activity≔active act3 : Select≔Null act4 : Edit_activity≔stop act5 : BtnSave≔FALSE END 61 Edit_Canelclick ≙ STATUS ordinary WHEN grd1 : Edit_activity=active ∧ Select=Edit∧BtnCancel=TRUE THEN act1 : Operator≔Cancel act2 : Main_activity≔active act3 : Select≔Null act4 : Edit_activity≔stop act5 : BtnCancel≔FALSE END Create_Cancelclick ≙ STATUS ordinary WHEN grd1 : Create_activity=active ∧ Select=Create∧BtnCancel=TRUE THEN act1 : Operator≔Save act2 : Main_activity≔active act3 : Create_activity≔stop act4 : Select≔Null act5 : BtnCancel≔FALSE END View_backclick ≙ STATUS ordinary WHEN grd1 : View_activity=active ∧ Select=View∧BtnBack=TRUE THEN act1 : Main_activity≔active act2 : View_activity≔stop act3 : Select≔Null act4 : BtnBack≔FALSE END END 62 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]