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

ĐẠ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

ĐẠ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

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

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

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

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Ẽ ............................................................................. 5

Chƣơng 1. GIỚI THIỆU ..................................................................................... 7

1.1. Sự cần thiết của đề tài ............................................................................... 7

1.2. Nội dung nghiên cứu ................................................................................ 9

1.3. Đóng góp của đề tài .................................................................................. 9

1.4. Cấu trúc của luận văn ............................................................................... 9

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

2.1. Giao diện người dùng ............................................................................. 11

2.2. Các phương pháp kiểm chứng giao diện ................................................ 12

2.2.1. Phương pháp tĩnh ............................................................................. 14

2.2.2. Phương pháp động ............................................................................ 14

2.3. Tổng quan về Event-B ............................................................................ 16

2.3.1 Context .................................................................................................... 17

2.3.2 Machine .................................................................................................. 18

2.3.3 Ký hiệu toán học trong Event-B ............................................................. 21

2.3.4 Tinh chỉnh ............................................................................................... 22

2.3.5 Mệnh đề chứng minh .............................................................................. 23

2.3.6 Công cụ Rodin ........................................................................................ 24

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

3.1. Phương pháp chung ................................................................................ 27

3.2. Phương pháp chi tiết ............................................................................... 28

3.3. Mô hình hóa giao diện phần mềm .......................................................... 31

3.4. Mệnh đề chứng minh .............................................................................. 32

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

4.1. Tổng quan về các ứng dụng trên điện thoại di động .............................. 34

4.1.1. Các thành phần cơ bản của một ứng dụng Android ........................ 35

4.1.2. Cơ chế quản lý các Activity ............................................................ 35

4.2. Ứng dụng Note ....................................................................................... 38

4.2.1. Giới thiệu chung ............................................................................... 38

4.2.2 Ứng dụng Note ................................................................................. 38

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

Kết luận ............................................................................................................ 56

Hướng phát triển .............................................................................................. 57

PHỤ LỤC ........................................................................................................... 58

A. Đặc tả context Note_C của ứng dụng Note ............................................ 58

B. Đặc tả machine Note_M của ứng dụng Note ......................................... 58

TÀI LIỆU THAM KHẢO ................................................................................ 62

DANH MỤC KÝ HIỆU VÀ CHỮ VIẾT TẮT

IDE Integrated Development Environment

GUI Graphical User Interface

POS Proof Obligations

INV Invariant

DLF Deadlock Freeness

VAR Variant

WD well-definedness

DANH MỤC CÁC BẢNG

Bảng 2.1 Các phép toán logic ......................................................................... 21

Bảng 2.2 Luật chứng minh INV với sự kiện evt ............................................. 24

Bảng 3.1 Chuyển đổi từ GUI tới Event-B ....................................................... 32

Bảng 4.1 Bảng CSDL ghi chú Note ................................................................ 38

Bảng 4.2 Mô tả cửa sổ giao diện MainActivity .............................................. 39

Bảng 4.3 Mô tả sơ bộ các đối tượng của cửa sổ giao diện CreateActivity ..... 40

Bảng 4.4 Mô tả sơ bộ các đối tượng của cửa sổ giao diện EditActivity ......... 41

Bảng 4.5 Mô tả sơ bộ các đối tượng của cửa sổ giao diện ViewActivity ....... 43

DANH MỤC CÁC HÌNH VẼ

Hình 2.1 Giao diện đồ họa người dùng ................................................ 11

Hình 2.2 Giao diện dòng lệnh .............................................................. 12

Hình 2.3 Cấu trúc và mối quan hệ của các thành phần mô hình trong Event-

B ................................................................................................................. 17

Hình 2.4 Cấu trúc context..................................................................... 18

Hình 2.5 Ví dụ về context trong Event-B ............................................ 18

Hình 2.6 Cấu trúc machine trong Event-B ........................................... 20

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

Hình 2.8 Ví dụ machine trong Event-B ............................................... 20

Hình 2.9 Ví dụ Event trong Event-B .................................................... 21

Hình 2.10 Ví dụ về mối quan hệ Refinement trong Event-B ................. 22

Hình 2.11 Sơ đồ định nghĩa sự kiện ....................................................... 23

Hình 2.12 Định nghĩa sự kiện evt .......................................................... 24

Hình 2.13 Giao diện đồ họa của công cụ Rodin .................................... 25

Hình 2.14 Symbols View ....................................................................... 36

Hình 2.15 Event-B Explorer ................................................................... 36

Hình 2.16 Menu bar ................................................................................ 36

Hình 3.1 Quy trình kiểm chứng tổng quát ........................................... 27

Hình 3.2 Quy trình kiểm chứng chi tiết ............................................... 30

Hình 4.1 Cơ chế Back Stack ................................................................ 36

Hình 4.2 Activity State ......................................................................... 37

Hình 4.3 MainActivity.XML ............................................................... 40

Hình 4.4 CreateActivit.XML ............................................................... 41

Hình 4.5 EditActivit.XML ................................................................... 42

Hình 4.6 ViewActivity.XML ............................................................... 43

Hình 4.7 Quy trình xây dựng Activity Diagram .................................. 44

Hình 4.8 Sơ đồ Activity Diagram ........................................................ 45

Hình 4.9 Quá trình mô hình hóa từ đặc tả vào trong Event-B ............. 46

Hình 4.10 Context Note_C ..................................................................... 47

Hình 4.11 Một phần của machine Note_M ............................................ 49

Hình 4.12 Event thoát ứng dụng ............................................................ 50

Hình 4.13 Event chọn chức năng Create ................................................ 50

Hình 4.14 Event chọn chức năng Edit .................................................... 50

Hình 4.15 Event chọn chức năng View .................................................. 51

Hình 4.16 Event chọn chức năng Delete ................................................ 51

Hình 4.17 Các Event trên các đối tượng của các cửa sổ ........................ 51

Hình 4.18 Cửa sổ sinh kiểm chứng tự động ........................................... 53

Hình 4.19 Bảng kết quả Statistics .......................................................... 53

Hình 4.20 Thông báo mệnh đề chưa chứng minh được tự động............ 54

Hình 4.21 Cửa sổ Goal ........................................................................... 54

Hình 4.22 Cửa sổ Statistics trong trường hợp lỗi ................................... 55

Hình 4.23 Cửa sổ Statistics trong trường hợp lỗi ................................... 55

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) thân thiện và người sử dụng

chỉ việc tương tác với giao diện của phần mềm.

Việc phát triển phần mềm dần hướng tới đưa ra sản phẩm có giao diện dễ

sử dụng, có tính thẩm mỹ cao và đảm bảo được các chức năng cần thiết. 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ư mong muốn. Lỗi phần mềm chủ yếu xuất hiện 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 thiệt hại về kinh tế và có thể nguy hại tới tính mạng của

người sử dụng,... 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 lỗi và sửa

chữa kịp thời hoặc bất cứ vấn đề bất thường nào có thể có của giao diện là vô

cùng quan trọng và là một thách thức lớn trong quá trình xây dựng phần mềm.

Kiểm chứng giao diện phần mềm là một quy trình gồm nhiều công việc

khác nhau trên nhiều đối tượng của giao diện. Trong đó 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 và cần thiết, có thể

thấy người sử dụng làm việc với phần mềm chủ yếu thông qua các cửa sổ giao

diện qua đó người dùng có thể giao tiếp, tương tác, trao đổi nhập xuất thông tin

với phần mềm. 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ẽ đư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.

Từ trước tới nay có nhiều phương pháp kiểm chứng, kiểm thử được áp

dụng để kiểm chứng, kiểm thử các bản đặc tả thiết kế giao diện phần mềm như

kiểm chứng tĩnh, kiểm chứng động, kiểm thử hộp đen,.... Tuy nhiên mỗi phương

pháp lại bộc lộ những ưu và nhược điểm riêng. Với kiểm chứng tĩnh lại phụ

thuộc chủ yếu vào kiến thức với kinh nghiệm khả năng phân tích của người

kiểm thử và thường tốn nhiều thời gian. Trong khi đó kiểm chứng động thì lại

được áp dụng trong quá trình thực hiện của phần mềm và sử dụng các kỹ thuật

kiểm thử tùy theo cấp độ như kiểm thử modul hay kiểm thử đơn vị, phương

pháp này tốt cho việc tìm lỗi nhưng lại đòi hỏi thực hiện chương trình tức là việc

kiểm chứng chỉ thực hiện sau khi đã có mã nguồn. 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.

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 cùng với ưu điểm của phương pháp Event-B và công cụ Rodin, 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 giao diện chung và tập trung vào 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 phần mềm cho các ứ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 đặ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.

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

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 4 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 và Phƣơng pháp

mô hình hóa Event-B

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.

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 3: 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 quy trình kiểm chứng tổng quát và chi tiết

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, xây dựng quy trình chi tiết, đư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 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

Trình bày tổng quan về ứng dụng trên thiết bị di động 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, biên tập mô hình thu

được và kiểm chứng tự động với công cụ Rodin.

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.

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

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

Giao diện người dùng Graphical user interfaces (GUI) là giao diện đồ họa

của chương trình cho phép người sử dụng giao tiếp với máy tính và các thiết bị

điện tử thông qua tương tác với các đối tượng đồ họa như: nút ấn, menu, hộp

nhập,…, thay vì chỉ là các dòng lệnh đơn thuần như trong Hình 2.2. GUI được

sử dụng phổ biến trong máy tính, các thiết bị cầm tay, các thiết bị đa phương

tiện trong văn phòng hoặc nhà ở.

Con người tương tác với phần mềm thông qua các đối tượng đồ họa: cửa

sổ, biểu tượng và các menu. Có nhiều phương pháp để tương tác, điều khiển như

thông qua việc sử dụng một con chuột, bàn phím hoặc cũng có thể sử dụng

bằng cách sử dụng các phím tắt bàn phím, phím mũi tên, hoặc thông qua giao

diện cảm ứng.

GUI cung cấp cho người dùng một cách 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 bắt mắt và dễ dùng hơn. Một

ví dụ minh họa về GUI thể hiện trong Hình 2.1.

Hình 2.1 Giao diện đồ họa người dùng

Hình 2.2 Giao diện dòng lệnh

2.2. Các phƣơng pháp kiểm chứng giao diện

Kiểm chứng giao diện là quá trình gồm nhiều kỹ thuật kiểm tra, kiểm thử

giao diện phần mềm để đảm bảo các chức năng tương ứng của giao diện đồ họa

người dùng của phần mềm phải phù hợp với thông số kỹ thuật bằng văn bản tức

là các bản đặc tả, thiết kế của nó [1].

Kiểm chứng những khiếm khuyết trong giao diện rất khó khăn bởi vì một

số lỗi giao diện chỉ biểu lộ trong những điều kiện đặc biệt. Các lỗi thường xảy ra

trên giao diện khi: một thành phần gọi tới các thành phần khác và gây ra lỗi

trong khi sử dụng giao diện của nó, 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, .v.v.

Ngoài chức năng phát hiện lỗi, kiểm chứng giao diện còn đánh giá các

yếu tố thiết kế như bố cục, màu sắc, phông chữ, cỡ 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.

Kiểm chứng giao diện có thể phân chia vào việc xem xét hai khía cạnh

chính [5]:

 Khả năng sử dụng của giao diện

 Tính thẩm mỹ, bắt mắt

 Màu sắc.

 Hình khối và biểu tượng (Icon).

 Vị trí, kích thước của các đối tượng nút ấn, hộp nhập, …

 Ngôn ngữ, các ký hiệu, từ viết tắt, chính tả.

 …

 Sự điều hướng

 Thông qua thao tác để truy cập qua cô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

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

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.

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

refines

Machine

sees

Sees

extends

Context

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

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

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.

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

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.

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

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

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.

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

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

EVENT REFINES ANY WHERE WITH THEN END

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

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 

 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

sees

tượng và các tinh chỉnh của chúng.

sees

refines

C01 C01

extends

sees

refines

sees

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

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

evt

any x where

G(s, c, v, x)

then

v:| BA(s, c, v, x, v’)

end

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

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 A(s, c)

Invariants và theorems I (s, c, v)

Guards của event G(s, c, v, x) evt/inv/INV

Vị từ trước và sau khi sự kiện BA(s, c, v, x, v’)

Thay đổi của các bất biến inv(s, c, v’)

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.

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.

 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

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

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ử

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.

Hình 3.2 Quy trình kiểm chứng chi tiết

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=

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.

 Đị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 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:

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

Luật 2 O, Properties Variables

Luật 3 Thành phần thuộc tính, Constants, Set, Axiom

trạng thái

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

được ký hiệu là Grd(g). Ta có thể định nghĩa nhiệm vụ chứng minh POs như

Grd(g)  E(g, g’)  I(g)  I(g’)

Hay có thể viết

Grd(x), E(g, g’), I(g) I(g’)

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.

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

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

Hình 4.2 Activity State [10].

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

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

 Name: MainActivity

Attribute  Type: Activity

 Layout: RelativeLayout

 Active (Running)

 Paused Status

 Stop

 Killed

ListView Control

ListView (hiển thị danh sách

các note)

BtnCreate Button Control

Object Control BtnExit Button Control

ContextMenu Menu Control

BtnexitClicked Button_Click

BtncreateClicked Button_Click

FocusListview Event

ClickContext Menu

RefreshListview

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

 Name: CreateActivity

Attribute  Type: Activity

 Layout: RelativeLayout

 Active (Running) Status  Paused

 Stop

 Killed

Texttitle Edittext Control

Textcontent Edittext Control

Object Control Btncancel Button Control

Btnsave Button Control

buttonSaveClicked Button_Click Event 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.

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

 Name: EditActivity

Attribute  Type: Activity

 Layout: RelativeLayout

Status

 Active (Running)  Paused  Stop  Killed Texttitle Edittext Control

Textcontent Edittext Control Object Control Btncancel Button Control

Btnsave Button Control

buttonSaveClicked Button_Click Event buttonCancelClicked Button_Click

Hình 4.5 EditActivit.XML

 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

 Name: ViewActivity

Attribute  Type: Activity

 Layout: RelativeLayout

Status

 Active (Running)  Paused  Stop  Killed Texttitle Edittext Control

Textcontent Edittext Control Object Control BtnBack Button Control

buttonCancelClicked Button_Click Event

Hình 4.6 ViewActivity.XML

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.

Chuyển đổi

Sự kiện & Hành động Đặc tả, yêu cầu thiết kế GUI

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

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

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.

[Exit Application]

MainActivity Start

[Select MenuContext]

[Delete true]

[Create false]

[Edit false]

[Edit true]

[View true]

[Create true]

MainActivity Pause

MainActivity Stop

[

ViewActivity Start

CreateActivity Start

EditActivity Start

D e l e t e N o t e ]

Cancel

ViewActivity Stop

Save

CreateActivity Stop

EditActivity Stop

Hình 4.8. Sơ đồ hoạt động

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.

Machine  Variables

 Invariants

 Events

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

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

Action:

EVENT-B Event-B

 Click

Sơ đồ hoạt động của GUI

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 4.9 Quá trình mô hình hóa từ đặc tả vào trong 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 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).

 (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).

 …

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 4.11. Một phần của machine Note_M

 EVENT, ACTION

 Event thoát ứng dụng thể hiện trong Hình 4.12.

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

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.

Select_Create ≙ STATUS

ordinary

WHEN

grd1 : (Main_activity=active)

act1 : Create_activity≔active act2 : Main_activity≔stop act3 : Select≔Create

THEN

END

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.

Select_Edit ≙

STATUS

ordinary

grd1 : Main_activity=active

WHEN

THEN

act1 : Edit_activity≔active act2 : Main_activity≔stop act3 : Select≔Edit

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

Hình 4.17. Các Event trên các đối tượng của các cửa sổ

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

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

Select_Edit ≙

STATUS

ordinary

WHEN

grd1 : Main_activity=active

THEN

act1 : View_activity≔active act2 : Main_activity≔stop act3 : Select≔Edit

END

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

Hình 4.22 Cửa sổ Goal

Hình 4.23 Cửa sổ Statistics trong trường hợp lỗi

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

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.

PHỤ LỤC

A. Đặc tả context Note_C của ứng dụng Note

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

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

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