Tóm tắt Luận văn Thạc sĩ Công nghệ thông tin: 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

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ẽ

3

đư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

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

4

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].

Sees

CONTEXT ….. EXTENDS ….. SETS ….. CONSTANTS …. AXIOMS ….. THEOREMS ….. END

MACHINE ….. REFINES ….. SEES …. VARIABLES ….. INVARIANTS ….. VARIANT …. EVENTS ….. END

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]:

CONTEXT ….. EXTENDS ….. SETS ….. CONSTANTS …. AXIOMS ….. THEOREMS ….. END

Hình 3.2. Cấu trúc của một context.

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].

MACHINE ….. REFINES ….. SEES …. VARIABLES ….. INVARIANTS ….. VARIANT …. EVENTS ….. END

Hình 3.4. Cấu trúc của machine trong Event-B.

EVENT REFINES ANY WHERE WITH THEN END

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 

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.

see s

refines

see s

M

refines

see s

C0 1 M C0 1 extend

C

see s Hình 3.8 Ví dụ về mối quan hệ Refinement trong Event-B

M

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=

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=

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 =

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:

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 = < G, A, S, E, C, M > 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 = < G, A, S, E, C, M > 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.

Chuyển đổi

Sự kiện & Hành động Đặc tả, bản thiết kế GUI của ứng dụng Android

Activity & Thành phần Sơ đồ hoạt động của GUI

Mô hình back stack Vòng đời Activity

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

[Exit Application]

18

MainActivity Start

[Select MenuContext]

[Delete true]

[Create false]

[Edit false]

[Edit true]

[View true]

MainActivity Pause

[Create true]

MainActivity Stop

MainActivity Stop

MainActivity Stop

[

l

ViewActivity Start

CreateActivity Start

EditActivity Start

D e e t e N o t e ]

Cancel

Cancel

ViewActivity Stop

Save

Save

CreateActivity Stop

EditActivity Stop

Hình 5.8. Sơ đồ Activity Diagram

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.

Machine  Variables

 Invariants

 Events

Object  Window  Controller stop  Properties:  Security  Constraints

Action:

EVENT-B Event-B

Đặc tả, bản thiết kế của GUI

 Click  Chagne

Context

 SET

 CONSTANT

 AXIOMS

 Constant  Statuts  Properties

Tinh chỉnh

Luật chuyển đổi

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

Mô hình Event-B trừu tượng

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.

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



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 :

inv10 :

Main_activity=start ⇒ (Create_activity=start) ∧ (Edit_activity=start) ∧ (View_activity=start) ¬(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

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ổ.

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] http://code.google.com/events/io/.

[9] http://www.Event-B.org/.

[10] http://www.android.com/.

[11] http://o7planning.org/web/fe/default/vi/document/1283892/huong-dan-

lap-trinh-android-voi-database-sqlite.

[12] http://android.vn/forums/.