3
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
PHẠM NHƯ UYỂN
MÔ HÌNH HÓA VÀ KIỂM CHỨNG
CÁC CHƯƠNG TRÌNH PHẦN MỀM HƯỚNG KHÍA CẠNH
Ngành: Công nghệ Thông tin
Chuyên ngành: Kỹ thuật Phần mềm
Mã số: 60480103
NGƯỜI HƯỚNG DẪN KHOA HỌC: PGS.TS Trương Ninh Thuận
HÀ NỘI - 2016
4
CHƯƠNG 1: ĐT VN ĐỀ
1.1 Sự cần thiết của đề tài
C rt nhiều công trnh nghiên cu tập trung vo kim chng mô hnh hưng kha
cnh s dng cc kỹ thuật khc nhau như UML [10], kim chng mô hnh (model
checking) [9], Petri-net [4], v B [7] nhưng không ph hp vi mt hệ thống da trên
cc s kiện.
Mt số công trnh nghiên cu đ khai thc nhng k hiệu ca UML hoc m
rng nhng k hiệu UML đ c th ha nhng vn đề crosscutting. Tuy nhiên, nhng
nghiên cu ny đ không gii quyt nhng kha cnh kim chng do bn cht không
chnh thc hoc bn chnh thc ca UML. Ubayashi v Tamain [8] đđề xut mt
phương php đ kim chng chương trnh AOP s dng mô hnh kim tra. Phương
php nhm vo cc giai đon lập trnh v ng dng cc mô hnh kim tra đ c kt
qu đan code ca lp v aspect. Phương php ny đm bo s chnh xc trong kim
chng, tuy nhiên li b qua cc vn đề kim chng mô đun. Điều ny c ngha l rt
kh c th s dng phương php ny đ xc minh phần mềm ln.
Dianxiang Xu [9] đ đề xut s dng my trng thi v kim chng nhng
chương trnh s dng aspect. Chng đ chuyn ha cc mô hnh đan v cc lp mô
hnh không b nh hưng bi aspect thnh cc chương trnh FSP, m s đưc kim
chng bi mô hnh LTSA chống li cc thuc tnh hệ thống mong muốn. Tuy nhiên,
phương php ny cần phi chuyn ha chương trnh cơ bn v aspect sang mô hnh
trng thi trưc khi khi đng mô hnh FSP [7] S dng B đ kim chng đan aspect.
Tc gi ny trnh by lp cơ bn v mt số aspect liên quan ca AspectJ trong ngôn
ng B. N nhm mc đch đt đưc li ch t cc minh chng to ra bi công c B
đ đm bo chnh xc ca aspectJ thnh phần.
Đ gii quyt vn đề ny, EAOP [3] cho phép xem xét hệ thống mối quan hệ gia
point-cut v đ thc hiện các aspect khi nhận đưc s kiện đưc pht sinh bi chương
trnh cơ bn. Tuy nhiên, mô hnh ny không đi kèm vi phương php đc t c th
chnh thc cũng như không cung cp bt kỳ cơ ch đxc minh tnh cht ca n
chnh thc. Trong bi ny, chng tôi đề xut mt phương php da trên mô hnh hóa
phương thc trên Event-B [2] đ phân tch mt ng dng EAOP. Đầu tiên, chng ta
xc đnh cc thnh phần ca n trong Event-B nơi s dng cc Event- B cơ ch làm
5
mn đ mô hnh cơ bn v chương trnh gim st. Sau đ, khai thc Event – B đ
chng minh đưc to ra đ kim tra xem cc hn ch p dng bi aspect cross-cuts.
1.2. Nội dung đề tài
Lập trnh hưng kha cnh da trên s kiện (EAOP) mô hnh cho phép xem
xét hệ thống mối quan hệ gia point-cut v đ thc hiện các aspect khi nhận đưc s
kiện đưc pht sinh bi chương trnh cơ bn. Tuy nhiên, mô hnh ny không đi kèm
vi phương php đc t cth chnh thc cũng như không cung cp bt kỳ cơ ch đ
xc minh tnh cht ca n chnh thc. Trong bi ny, chng tôi đề xut mt phương
php da trên mô hnh hóa phương thc trên Event-B đ phân tch mt ng dng
EAOP. Đầu tiên, chng ta xc đnh cc thnh phần ca n trong Event-B nơi s dng
các Event- B cơ ch lm mn đ mô hnh cơ bn v chương trnh gim st. Sau đ,
chúng ta khai thác Event – B đ chng minh đưc to ra đ kim tra xem cc hn
ch p dng bi aspect cross-cuts. Cuối cng, phương php đề xut đưc minh họa
chi tit vi mt chương trnh ATM.
1.3. Đóng góp của luận văn
Đng gp ca luận văn liên quan việc mô hình hóa và kim chng EAOP s dng
phương php hnh thc Event-B. Phương php m chng tôi đề xut da trên việc
dch mt chương trnh EAOP thnh cc my ca Event-B, tận dng cc cơ ch lm
mn đ kim chng nhng rng buc trong chương trnh trong mi aspect. Vi mong
muốn kim tra chương trnh c cn lưu gi mt số đnh ngha thuc tnh sau khi đan
chương trnh. Luận văn cũng minh họa phương php mô hnh ha v kim chng
trong mt chương trnh ATM.
1.4. Cu trc luận văn
Cc phần cn li ca luận văn s đưc trnh by bao gm cc phần sau:
CHƯƠNG 2: EAOP VÀ EVENT-B
Gii thiệu khái quát nhng kin thc cơ bn v EAOP. Mô hình kin trúc
EAOP. Trình bày nhng kin thc tổng quan về phương php mô hnh ha Event-B,
6
mô t cu trúc ca mô hình, các thành phần. Trình bày công c kim chng t đng
Rodin.
CHƯƠNG 3: MÔ HÌNH HÓA VÀ KIỂM CHỨNG CÁC PHẦN MỀM
HƯỚNG KHÍA CẠNH.
Tập trung vào việc mô hình hóa và kim chng chương trnh phần mềm hưng
khía cnh đưa ra cch đnh ngha hưng kha cnh hệ thống hưng s kiện trong
Event-B. Mô hnh ha hệ thống lập trnh hưng kha cnh sdng Event-B. Kim
chng hệ thống.
CHƯƠNG 4: ÁP DỤNG BÀI TOÁN.
Áp dng phương php đ trnh by trên đ mô hình hóa và kim chng bài
toán máy ATM.
CHƯƠNG 5: KẾT LUẬN.
Kt luận tổng th các kt qu đt đưc trong luận văn v hưng phát trin ca
luận văn.
7
CHƯƠNG 2. EAOP VÀ EVENT-B
2.1. Event-based Aspect Oriented Programming
Nền tng chung ca EAOP đưc trnh by trong [3]. EAOP ch  đn cc s kiện
pht sinh ra trong qu trnh thc hiện chương trnh đc lập vi bt kỳ ngôn ng lập
trnh c th. Tnh năng chnh ca mô hnh l aspect c th đnh ngha mt hnh đng
cho mt chui cc s kiện thay v c nhân ch như mô t trong mô hnh AOP. N c
nhng đc đim chnh sau:
Aspect: đưc đnh ngha về cc s kiện sinh ra trong qu trnh thc hiện
chương trnh.
Cross-cuts: gim chui s kiện, c th bao gm cc trng thi thay đổi, đưc
xc đnh bi mô hnh s kiện đ đưc kt hp trong qu trnh thc hiện chương
trnh.
Mt cross-cuts đưc chọn, mt hnh đng liên quan đưc thc hiện.
2.2. Cc đăc đim của AOP
a. Đim nối (join point)
Join point [13]: có th là bt kỳ đim nào có th xc đnh đưc khi thc hiện chương
trình. C th l li gọi hm đn mt phương thc hoc mt lệnh gn cho mt bin
ca đối tưng. Trong Aspect mọi th đều xoay quanh join point.
b. Hướng cắt (pointcut)
Pointcut [13]: l cu trc chương trnh m n chọn cc join point v ng cnh ti cc
join point đ. V d mt pointcut c th chọn mt join point l mt li gọi đn mọt
phương thc v ly thông tin ng cnh ca phương thc đ như đối tưng cha
phương thc, cc đối số ca phương thc đ.
c. Mã hành vi (advice)
Advice [13]: l m đưc thc hiện ti mt join point mà đưc chọn bi poincut.
Advice tương t cu trc ca hm cung cp cc thc, cc hnh đng đan xen ti cc
join point mn đưc chọn bi pointcut. Poincut v advice s hnh thnh nên cc
luật đan kt cc quan hệ đan xen.