ÑI H≈C QU»C GIA HÀ NÀI
Tr˜Ìng §i hÂc Công nghª
Lê HÁng Anh
Ph˜Ïng pháp mô hình hóa và ki∫m ch˘ng các hª
thËng h˜Óng s¸ kiªn
Tóm t≠t lu™n án ti∏n sˇ ngành công nghª thông tin
Chuyên ngành: Công nghª ph¶n m∑m
Mã sË: 62.48.10.01
Hà NÎi, 2014
Công trình ˜Òc hoàn thành t§i Khoa Công nghª thông tin, Tr˜Ìng
QuËc Gia Hà NÎi.
Ng˜Ìi h˜Óng d®n khoa hÂc:
PGS. TS Tr˜Ïng Ninh Thu™n
PGS. TS Ph§m B£o SÏn
Ph£n biªn 1: ........................
Ph£n biªn 2: ........................
Ph£n biªn 3: ........................
Có th∫ tìm hi∫u lu™n án t§i
- Th˜ viªn QuËc gia Viªt Nam
- Trung tâm thông tin th˜ viên ,
§i hÂc QuËc gia Hà NÎi
§i hÂc Công nghª,
§i hÂc
Ch˜Ïng 1. TÍng quan v∑ lu™n án
1.1 L˛ do l¸a chÂn ∑ tài
Mô hình hóa là mÎt trong các cách th˘c hiªu qu£ ∫ qu£n l˛ Î ph˘c t§p trong
phát tri∫n ph¶n m∑m, nó cho phép thi∏t k∏ và ánh giá các yêu c¶u cıa hª thËng.
Mô hình hóa không chø cung cßp các nÎi dˆng mÎt cách tr¸c quan mà còn c£ các
nÎi dung k˛ t¸. Các kˇ thu™t ki∫m th˚ có th∫ ˜Òc s˚ dˆng trong phát tri∫n ph¶n
m∑m thông th˜Ìng ∫ ki∫m tra liªu mÎt ph¶n m∑m th¸c thi có th‰a mãn yêu c¶u
cıa ng˜Ìi dùng. Tuy nhiên, ki∫m th˚ là cách xác th¸c không ¶y ı vì nó chø có
th∫ phát hiªn ˜Òc lÈi trong mÎt vài tr˜Ìng hÒp nh˙ng không £m b£o ˜Òc hª
thËng ch§y úng trong mÂi tr˜Ìng hÒp. Ki∫m ch˘ng ph¶n m∑m là mÎt trong nh˙ng
ph˜Ïng pháp m§nh hiªu qu£ ∫ tìm ra lÈi ho∞c ch˘ng minh không có lÈi mÎt cách
toán hÂc. MÎt vài kˇ thu™t ã ˜Òc ∑ xußt cho ki∫m ch˘ng ph¶n m∑m nh˜ ki∫m
ch˘ng mô hình, ch˘ng minh ‡nh l˛, và phân tích ch˜Ïng trình. Trong các kˇ thu™t
này, ch˘ng minh ‡nh l˛ có ˜u i∫m vì có kh£ n´ng ki∫m ch˘ng các ch˜Ïng trình
có kích cÔ lÓn và suy diπn qui n§p. Tuy nhiên, ch˘ng minh ‡nh l˛ th˜Ìng sinh ra
nhi∑u các ch˘ng minh ph˘c t§p và khó hi∫u. Trên khía c§nh khác, ki∏n trúc ph¶n
m∑m là mÎt khái niªm ˜Òc ∑ xußt ∫ xây d¸ng các hª thËng ph¶n m∑m mÎt cách
hiªu qu£. MÎt d§ng ki∏n trúc ho∞c ki∫u thi∏t k∏ th˜Ìng có các ph˜Ïng pháp mô
hình hóa và ki∫m ch˘ng phù hÒp khác nhau. Ki∏n trúc h˜Óng s¸ kiªn là mÎt trong
nh˙ng ki∏n trúc phÍ bi∏n trong phát tri∫n ph¶n m∑m cung cßp cÏ ch∏ gÂi d‡ch vˆ
không tr¸c ti∏p. MÈi thành ph¶n cıa ki∏n trúc này có th∫ sinh ra các s¸ kiªn, sau
ó hª thËng s≥ gÂi các thı tˆc ã ´ng k˛ vÓi các s¸ kiªn này. ây là mÎt ki∏n
trúc ¶y h˘a hµn vì nó cho phép phát tri∫n và mô hình các hª thËng ít ràng buÎc
nhau và lÒi ích cıa nó ã ˜Òc công nh™n rÎng rãi trong khoa hÂc và ˘ng dˆng. Có
nhi∑u lo§i hª thËng h˜Óng s¸ kiªn bao gÁm các hª thËng giao ªndiªn ng˜Ìi dùng
cho phép s˚ dˆng các s¸ kiªn ∫ th¸c thi lªnh cıa ng˜Ìi dùng, các hª thËng sinh
ra lu™t s˚ dˆng trong trí tuª nhân t§o khi x£y ra mÎt i∑u kiªn nào ó, hay các
Ëi t˜Òng ho§t Îng khi thay Íi giá tr‡ cıa các thuÎc tính thì kích ho§t mÎt sË
hành Îng [11]. Trong ki∏n trúc h˜Óng s¸ kiªn, các lu™n d§ng ECA ˜Òc ∑ xußt
nh˜ mÎt các ti∏p c™p ∫ ∞c t£ các quan hª khi các s¸ kiªn x£y ra mÎt i∑u kiªn
‡nh tr˜Óc. Lu™t ECA có d§ng: On Event IF conditions DO actions có nghæa là
khi s¸ kiªn Event x£y ra trong mÎt i∑u kiªn conditions thì th¸c thi actions. Ta
cÙng có th∫ bi∫u diπn các lu™t này mÎt cách không hình th˘c b¨ng các lu™t if-then,
nghæa là if Events x£y ra trong i∑u kiªn condition, then th¸c thi action. Các ˜u
i∫m cıa ph˜Ïng pháp này ã ˜Òc ˘ng dˆng và tích hÒp trong nhi∑u lænh v¸c
khác nhau nh˜ hª thËng CSDL, các ˘ng dˆng c£m ng˙ c£nh. ã có nhi∑u nghiên
c˘u v∑ phân tích các hª thËng h˜Óng s¸ kiªn cÙng nh˜ là hình th˘c hóa các lu™t
ECA. Tuy nhiên, các ph˜Ïng pháp mô hình hóa và ki∫m ch˘ng các hª thËng h˜Óng
s¸ kiªn tÍng quát là ch˜a ı vì trên th¸c t∏ ta th˜Ìng phát tri∫n mÎt d§ng ∞c
tr˜ng cıa hª thËng h˜Óng s¸ kiªn có s˚ dˆng các lu™t ECA. HÏn n˙a các nghiên
c˘u hiªn t§i cıa ki∫m ch˘ng ph¶n m∑m chı y∏u tâp trung vào phân tích các mô
1
2
TÍng quan v∑ lu™n án
t£ chính xác v∑ ch˘c n´ng và hành vi cıa hª thËng. Chính vì nh˙ng l˛ do trên,
các ph˜Ïng pháp mô hình hóa và ki∫m ch˘ng phù hÒp cho các hª thËng này là c¶n
thi∏t. N∏u ta có th∫ ki∫m ch˘ng các tính chßt quan trÂng cıa hª thËng sÓm thì s≥
ti∏t kiªm ˜Òc chi phí phát tri∫n. Các ph˜Ïng pháp này vì th∏ n∏u gi£m ˜Òc Î
ph˘c t§p trong ch˘ng minh thì s≥ có kh£ n´ng áp dˆng vào th¸c t∏ cao. Lu™n án
∑ xußt các ph˜Ïng pháp mÓi ∫ §t ˜Òc các yêu c¶u trên b¨ng s˚ dˆng ph˜Ïng
pháp hình Event-B. Event-B ˜Òc d¸a trên l˛ thuy∏t t™p hÒp và phù hÒp cho mô
hình hóa các hª thËng lÓn và ph£n ˘ng. Tính nhßt quán cıa mô hình Event-B ˜Òc
b£o £m bi các ch˘ng minh hình th˘c. Các công cˆ hÈ trÒ ˜Òc chung cßp cho
∞c t£ và ch˘ng minh Event-B trên n∑n t£ng Rodin. Vì vây, s˚ dˆng Event-B làm
ph˜Ïng pháp hình th˘c ∫ mô hình hóa và ki∫m ch˘ng các hª thËng h˜Óng s¸ kiªn
có rßt nhi∑u ˜u i∫m.
1.2 Mˆc tiêu
Lu™n án ˜a ra mÎt cách ti∏p c™n khác so vÓi các nghiên c˘u hiªn t§i. Thay vì
phân tích mÎt hª thËng h˜Óng s¸ kiªn tÍng quát, chúng tôi t™p trung vào s˚ dˆng
Event-B ∫ mô hình hóa các hª thËng h˜Óng s¸ kiªn ∞c tr˜ng nh˜ các hª thËng
CSDL, các hª thËng c£m ng˙ c£nh. Lu™n án ∑ xußt các ph˜Ïng pháp hiªu không
chø mô hình hóa các hành vi ˜Òc bi∫u diπn b¨ng các lu™t If-Then mà còn hình
th˘c hóa các tính chßt quan trÂng b¨ng các thành ph¶n Event-B. Tính úng ≠n
cıa các tính chßt này ˜Òc ch˘ng minh mÎt cách toán hÂc b¨ng viªc ch˘ng minh
các mªnh ∑ c¶n ch˘ng minh ˜Òc sinh ra bi Event-B. Công cˆ Rodin ˜Òc s˚
dˆng trong hÈ trÒ quá trình mô hình hóa và ch˘ng minh t¸ Îng. Lu™n án có mˆc
tiêu phân tích các hª thËng h˜Óng s¸ kiªn ˜Òc mô t£ b¨ng các yêu c¶u không
chính xác. Lu™n án giÓi thiªu ph˜Ïng pháp mÓi d¸a trên làm m‡n ∫ mô hình hóa
và ki∫m ch˘ng tính chßt an toàn và tính ho§t Îng cıa hª thËng.
1.3
óng góp mÓi cıa lu™n án
Các nghiên c˘u óng góp cıa lu™n án bao gÁm
1. Lu™n án ∑ xußt mÎt ph˜Ïng pháp ∫ mô hình hóa và ki∫m ch˘ng các hª thËng
CSDL có thành ph¶n trigger s˚ dˆng Event-B. Ph˜Ïng pháp này giÓi thiªu các
b˜Óc chi ti∏t ∫ chuy∫n Íi các khái niªm trong CSDL sang các k˛ hiªu Event-B.
Quá trình chuy∫n Íi d¸a trên s¸ t˜Ïng t¸ gi˙a cßu trúc cıa triggers và Event-B
event. VÓi ph˜Ïng pháp ∑ xußt, tính chßt b£o toàn các ràng buÎc ˜Òc ki∫m
ch˘ng và các vòng l∞p vô h§n sinh ra bi các trigger có th∫ ˜Òc phát hiªn b¨ng
các ch˘ng minh hình th˘c. Các phát hiªn này s≥ óng góp làm gi£m chi phí phát
tri∫n. MÎt công cˆ hÈ trÒ chuy∫n Ëi bán t¸ Îng cÙng ˜Òc phát tri∫n.
2. Lu™n án ti∏p tˆc nghiên c˘u ˜u i∫m cıa cÏ ch∏ ho§t Îng t˜Ïng t¸ gi˙a các
lu™t ECA và Event-B event ∫ ∑ xußt ph˜Ïng pháp mô hình hóa và ki∫m ch˘ng
các hª thËng c£m ng˙ c£nh. Lu™n án phát hiªn ra ˜u i∫m cıa cÏ ch∏ làm m‡n
trong Event-B ∑ làm cho ph˜Ïng pháp ∑ xußt phù hÒp vÓi mô hình hóa t¯ng
b˜Óc. Các tính chßt quan trÂng nh˜ là b£o toàn ràng buÎc ng˙ c£nh có th∫ ˜Òc
ki∫m ch˘ng t¸ Îng b¨ng s˚ dˆng công cˆ Rodin.
Hình 1.1: Cßu trúc lu™n án
3. Lu™n án x˚ l˛ tr˜Ìng hÒp mÎt hª thËng ˜Òc mô t£ b¨ng các yêu c¶u không
chính xác. Các hành vi cıa hª thËng này ˜Òc bi∫u diπn d˜Ói d§ng lu™t If-Then
mÌ. Lu™n án giÓi thiªu mÎt bi∫u diπn mÓi cıa các thu™t ng˙ mÌ b¨ng các t™p
hÒp và ˜a ra mÎt t™p lu™t ∫ chuy∫n Íi các lu™t If-Then mÌ thành các ph¶n
t˚ Event-B. Chúng tôi cÙng ˜a ra mÎt khái niªm m rÎng lu™t If-Then mÌ thÌi
gian ∫ mô hình hóa các hª thËng ˜Òc ‡nh thÌi.
4. Lu™n án k∏ th¯a tính làm m‡n cıa Event-B, d¸a trên ph˜Ïng pháp mô hình hóa
các lu™t If-Then mÌ và mÎt sË ph˜Ïng pháp suy diπn ∫ phân tích mÎt sË tính
chßt quan trÂng cıa các yêu c¶u không chính xác nh˜ tính an toàn và tính ho§t
Îng.
1.4 Cßu trúc lu™n án
Lu™n án ˜Òc tÍ ch˘c nh˜ Hình 1.1. Ch˜Ïng 2 cung cßp các ki∏n th˘c n∑n t£ng
cho lu™n án. Ch˜Ïng 3 giÓi thiªu ph˜Ïng pháp mô hình hóa và ki∫m ch˘ng các hª
thËng CSDL. Ch˜Ïng 4 t™p trung vào vßn ∑ mô hình hóa và ki∫m ch˘ng các hª
thËng c£m ng˙ c£nh. Trong Ch˜Ïng 5, lu™n án ∑ xußt mÎt ph˜Ïng pháp mô hình
hóa cho các hª thËng h˜Óng s¸ kiªn ˜Òc mô t£ bØng các lu™t If-Then mÌ. Ch˜Ïng
6 giÓi thiªu ph˜Ïng pháp ki∫m ch˘ng tính chßt an toàn và ho§t Îng cıa các yêu
c¶u không chính xác. Ch˜Ïng 7 tÍng k∏t lu™n án và ˜a ra h˜Óng phát tri∫n.
Ch˜Ïng 2. Ki∏n th˘c cÏ s
2.1 Temporal logic
Propositional temporal logic (PTL) là s¸ m rÎng cıa logic mªnh ∑ trong ó mô
t£ mÎt chuÈi các tr§ng thái nh˙ng kho£ng thÌi gian khác nhau gÂi là thÌi i∫m
t˘c thÌi. MÎt thành ph¶n cÏ b£n PTL là mÎt công th˘c logic b™c 1 ˜Òc xây
d¸ng t¯ các nguyên tË v‡ t¯,các phép l˜Òng hóa 9, 8; các toán t˚ ^, _ ,¬; và các
3
4
toán t˚ thÌi gian ⇤ (“always”),⌃ (“eventually”), và (“next”), U (“until"). Cú pháp
cıa mÎt công th˘c PTL ˜Òc mô t£ nh˜ trong B£ng 2.1
B£ng 2.1: Cú pháp cıa công th˘c PTL
hformulai
htermi >
hfactor i >
hprimaryi >
::= htermi {_ htermi}
::= hfactor i {^ hfactor i}
::= hprimaryi {U hprimaryi}
::= hatomc propositioni >
| ¬ hprimaryi >
| hprimaryi >
| ⌃ hprimaryi >
| ⇤ hprimaryi >
2.2 L˛ thuy∏t t™p hÒp
T™p hÒp là các Ëi t˜Òng cÏ b£n ˜Òc s˚ dˆng ∫ ‡nh nghæa các khái niªm khác
trong toán hÂc. Ngôn ng˙ cıa l˛ thuy∏t t™p hÒp d¸a trên các quan hª cÏ b£n gÂi
là thành viên. A là mÎt thành viên cıa B (A 2 B ), có nghæa là B ch˘a A nh˜ mÎt
ph¶n t˚ cıa nó [14]. Có nhi∑u ‡nh nghæa cÏ b£n khác cıa l˛ thuy∏t t™p hÒp nh˜
là t™p mÙ, quan hª, hàm, bi∫u diπn lamda, vv..
2.3 T™p mÌ và lu™t If-Then mÌ
Trong phát tri∫n ˘ng dˆng trên th¸c t∏, các hª thËng th˜Ìng không ˜Òc mô t£
mÎt cách chính xác. Các stakeholders th˜Ìng s˚ dˆng các thu™t ng˙ mÌ nh˜ “rßt
tËt", “nóng",.. ∫ x˚ l˛ các hª thôgns ˜Òc khó ˜Òc bi∫u diπn b¨ng các mô t£
chính xác Zadeh [16] ã giÓi thiªu mÎt khung làm viªc logic không ph£i là logic hai
giá tr‡ truy∑n thËng mà là a giá tr‡ hay ˜Òc biên d‡ch bi các t™p mÌ. MÎt t™p
mÌ F ˜Òc ‡nh nghæa trên mÎt t™p X là mÎt t™p, mà mÈi ph¶n t˚ là mÎt c∞p:
A = {(x , ) µA (x )}, x 2 X
(2.1)
trong ó µA (x ) : X ! [0, 1] ˜Òc ‡nh nghæa nh˜ mÎt hàm thuÎc cıa mÎt ph¶n t˚
x trong A.
MÎt fuzzy hedge là mÎt toán t˚ bi∏n Íi t™p mÌ F (x ) sang t™p mÌ F (hx ). Các
hedges là các hàm sinh ra mÎt t™p lÓn hÏn các giá tr‡ cho các bi∏n. Ví dˆ, s˚ dˆng
hedge very vÓi not trên t¯ tall có th∫ sinh ra very tall or not very tall. Các lu™t
If-Then mÌ ˜Òc vi∏t d˜Ói d§ng Ïn gi£n: “If a is A then b is B ", óng mÎt vai trò
quan trÂng trong l˛ thuy∏t t™p mÌ. Nó là cách ti∏p c™n ∫ phân tích các yêu c¶u
không chính xác cıa hª thËng. Ta th˜Ìng s˚ dˆng các lu™t này ∫ mô t£ hành vi
cıa các hª thËng vÓi yêu c¶u không chính xác.
2.4 Các ph˜Ïng pháp hình th˘c
Các ph˜Ïng phác hình th˘c ˜Òc s˚ dˆng ∫ ∞c t£ và ki∫m ch˘ng các hª thËng
mÎt cách toán hÂc. MÎt ph˜Ïng pháp là hình th˘c n∏u nó ˜Òc có inh nghæa cÏ
s d˜Ói d§ng toán hÂc th˜Ìng ˜Òc ˜a ra bi mÎt ngôn ng˙ hình th˘c [13]. Các
ph˜Ïng pháp ki∫m ch˘ng hình th˘c tr nên phÍ bi∏n trong công nghiªp và ngày
càng có các yêu c¶u ˘ng dˆng chúng. Có hai cách ti∏p c™n phÍ bi∏n trong ki∫m
Ch˜Ïng 2 Ki∏n th˘c cÏ s
ch˘ng là ki∫m ch˘ng mô hình và ch˘ng minh ‡nh l˛. Lu™n án này s˚ dˆng ph˜Ïng
pháp Event-B ∫ mô hình hóa và ki∫m ch˘ng các s¸ kiªn, vì v™y trong ph¶n này
tr˜Óc khi trình bày v∑ Event-B chúng tôi s≥ giÓi thiªu mÎt sË ph˜Ïng pháp liên
quan nh˜ VDM [8], Z [12], B [2].
2.4.1
VDM
VDM là vi∏t t≠t cıa “The Vienna Development Method" bao gÁm mÎt nhóm các
kˇ thu™t cho ∞c t£ hình th˘c và phát tri∫n cıa các hª tính toán. VDM là mÎt
ph˜Ïng pháp d¸a trên mô hình mô t£ các hª thËng ph¶n m∑m thành các mô hình
[8]. Các mô hình này ˜Òc ∞c t£ nh˜ các Ëi t˜Òng và các hành Îng trên các Ëi
t˜Òng trong ó các Ëi t˜Òng bi∫u diπn các tr§ng thái input, output và bên trong
cıa hª thËng. VDM có ngôn ng˙ ∞c t£ VDM-SL bao gÁm mô hình toán hÂc ˜Òc
xây d¸ng t¯ các d˙ liªu cÏ b£n nh˜ t™p hÒp, danh sách và ánh x§ cùng vÓi các
hành Îng thay Íi tr§ng thái cıa mô hình. VDM-SL có ‡nh nghæa hình th˘c d¸a
trên Logic of Partial Functions (LPF).
2.4.2
Ph˜Ïng pháp Z
∞c t£ Z d¸a trên l˛ thuy∏t t™p hÒp và tính toán v‡ t¯ b™c 1. MÈi Ëi t˜Òng có
mÎt ki∫u riêng, ˜Òc bi∫u diπn bi mÎt t™p c¸c §i trong ∞c t£ hiªn t§i. MÎt khía
c§nh cıa Z là s˚ dˆng ngôn ng˙ t¸ nhiên. Z s˚ dˆng toán hÂc ∫ ˜a ra vßn ∑,
tìm ra các gi£i pháp và ch˘ng minh thi∏t k∏ l¸a chÂn phù hÒp vÓi ∞c t£. Z cung
cßp cÏ ch∏ làm m‡n ∫ xây d¸ng hª thËng d¶n d¶n. MÎt tài liªu ∞c t£ Z bao gÁm
các o§n hình th˘c và phi hình th˘c [12].
2.4.3
Ph˜Ïng pháp B
B là mÎt ph˜Ïng pháp ∞c t£, thi∏t k∏ và vi∏t mã cho các hª thËng ph¶n m∑m. fi
t˜ng chính cıa B là b≠t ¶u b¨ng mÎt mô hình rßt tr¯u t˜Òng, sau ó thêm d¶n
các chi ti∏t vào các mô hình cˆ th∫ ti∏p theo [2]. B ˜a ra các khái niªm v∑ máy
tr¯u t˜Òng óng gói các thành ph¶n toán hÂc, h¨ng, t™p hÒp, bi∏n và mÎt t™p hÒp
các hành Îng trên các bi∏n này. Các thành ph¶n này ˜Òc ch˘a trong các môdun
có tên ∫ có th∫ ˜Òc s˚ dˆng các môdun khác.
2.5 Event-B
Event-B [3] là mÎt ph˜Ïng pháp hình th˘c mô hình hóa và phân tích m˘c mô hình.
∞c tính chı chËt cıa Event-B là s˚ dˆng l˛ thuy∏t tâp hÒp làm k˛ hiªu mô t£, s˚
dˆng cÏ ch∏ làm m‡n ∫ bi∫u diπn các hª thËng các m˘c tr¯u t˜Òng khác nhau và
s˚ dˆng các ch˘ng minh toán hÂc ∫ ki∫m ch˘ng s¸ Áng nhßt gi˙a các m˘c làm
m‡n. MÎt cßu trúc mô hình Event-B cÏ b£n bao gÁm mÎt máy và ng˙ c£nh.
Ng˙ c£nh Event-B mô t£ ph¶n tænh trong ó các tính chßt liên quan và các gi£
thuy∏t. MÎt ng˙ c£nh có th∫ bao gÁm các t™p hÒp, h¨ng và các gi£ thi∏t. T™p mang
s ˜Òc bi∫u diπn bi tên và khác rÈng. Các t™p mang có tên khác thì hoàn toàn Îc
l™p nhau. H¨ng c ˜Òc xác ‡nh bi các gi£ thi∏t P (s , c ), các gi£ thi∏t này cÙng
phˆ thuÎc vào t™p mang s.
Máy Event-B ˜Òc xác ‡nh b¨ng mÎt t™p các mªnh ∑ bao gÁm các bi∏n, bßt bi∏n,
‡nh l˛ và s¸ kiªn. Bi∏n v biπu diπn tr§ng thái cıa mô hình. Bßt bi∏n I (v ) sinh ra
6
các lu™t ∑ £m b£o các bi∏n v luôn th‰a mãn. Các lu™t này ˜Òc hình th˘c hóa
b¨ng các v‡ t¯ bi∫u diπn bi tính toán v‡ t¯ b™c mÎt ˜Òc m rÎng bi Equality bi
l˛ thuy∏t t™p hÒp. MÈi s¸ kiªn có dang evt = any x where G (x , v ) then A(x , v , v 0 )
end trong ó x là các bi∏n cˆc bÎ cıa s¸ kiªn, G (x , v ) là i∑u kiªn x£y ra s¸ kiµn
và A(x , v , v 0 ) là hành Îng cıa s¸ kiªn. MÎt s¸ kiªn ˜Òc kích ho§t n∏u i∑u kiªn
cıa nó tho£ mãn. MÎt hành Îng cıa s¸ kiªn có th∫ có nhi∑u phép gán. MÈi phép
gán có th∫ là (1) phép gán Ïn ‡nh (x := E (t , v )), (2) phép gán rÈng (skip), ho∞c
(3) phép gán không Ïn ‡nh (x :| P (t , v , x 0 )). ∫ gi£i quy∏t s¸ ph˘c t§p khi mô
hình hóa hª thËng, Event-B cung cßp cÏ ch∏ làm m‡n cho phép xây d¸ng hª thËng
t¯ng b˜Óc b¨ng viªc thêm vào các chi ti∏t ∫ §t ˜Òc mô hình chính xác hÏn. MÎt
máy làm m‡n th˜Ìng có nhi∑u bi∏n hÏn máy tr¯u t˜Òng vì ta có nhi∑u bi∏n biπu
diπn mô hình chi ti∏t hÏn. Trong làm m‡n chÁng, các bi∏n tr¯u t˜Òng v®n tÁn t§i
trong máy làm m‡n, trong làm m‡n theo chi∑u dÂc các bi∏n tr¯u t˜Òng ˜Òc thay
th∏ bi các bi∏n cˆ th∫. K∏t nËi gi˙a bi∏n tr¯u t˜Òng v và bi∏n cˆ th∫ w ˜Òc bi∫u
diπn b¨ng các bßt bi∏n J (v , w ). ∫ ki∫m tra xem mÎt máy Event-B có th‰a mãn
mÎt t™p các tính chßt không, Event-B ‡nh nghæa ra các mªnh ∑ c¶n ch˘ng minh.
MÎt vài mªnh ∑ c¶n ch˘ng minh liên quan ∏n lu™n án là invariant preservation
(INV), convergence (VAR), deadlock-freeness (DLF).
2.6 Rodin tool
Lu™n án s˚ dˆng công cˆ Rodin phiên b£n 2.8 [1] là môi tr˜Ìng Eclipse ∫ mô hình
hóa và ch˘ng minh trong Event-B. Nó ˜Òc xây d¸ng trên n∑n t£ng cıa Eclipse
bao gÁm các công cˆ hÈ trÒ mô hình hóa plug-ins. Rodin có giao diªn phong phú
bao gÁm các c˚a sÍ nh˜ proving, Event-B editor..
• C˚a sÍ Proving: Cung cßp tßt c£ các mªnh ∑ ˜Òc sinh ra mÎt cách t¸ Îng cho
các máy Event-B. Các mênh ∑ này ˜Òc ch˘ng minh t¸ Îng ho∞c t˜Ïng tác
thông qua các c˚a sÍ mªnh ∑ và mˆc tiêu.
• C˚a sÍ Event-B: Bao gÁm các giao diªn cho phép chønh s˚a các máy và ng˙ c£nh.
N∏u ng˜Ìi s˚ dˆng mã hóa không chính xác, c˚a sÍ problem s≥ hiªn th‡ thông
báo lÈi.
2.7 Các hª thËng h˜Óng s¸ kiªn
Có nhi∑u lo§i hª thËng h˜Óng s¸ kiªn nh˜ giao diªn cıa ph¶n m∑m, các hª thËng
sinh lu™t ˜Òc s˚ dˆng trong trí tuª nhân t§o khi i∑u kiªn úng thì th¸c thi mÎt
hành Îng, hay trong các Ëi t˜Òng ho§t ông khi thay Íi giá tr‡ hay thuÎc tính
cıa Ëi t˜Òng [11]. Trong lu™n án này, chúng tôi xét ∏n hai ˘ng dˆng ó là các
hª thËng CSDL và c£m ng˙ c£nh. C£ hai hª thËng này ∑u s˚ dˆng các lu™t d§ng
ECA ∫ bi∫u diπn các hành vi.
2.7.1
Hª thËng CSDL và triggers
MÎt hª thËng CSDL quan hª d¸a trên mô hình quan hª gi˙a các Ëi t˜Òng và các
quan hª, hành Îng cho thao tác d˙ liªu và toàntoàn vµn d˙ liªu. Các hª thËng
CSDL quan hª hiªn §i s˚ dˆng các lu™t ho§t Îng nh˜ trigger CSDL áp ˘ng
l§i các s¸ kiªn x£y ra bên trong và bên ngoài cıa CSDL. Trigger là mÎt o§n mã
t¸ Îng th¸c thi khi có mÎt s¸ kiªn xác ‡nh x£y ra trong CSDL. S¸ kiªn th˜Ìng
liên quan ∏n viªc thao tác d˙ trong CSDL. Trigger th˜Ìng ˜Òc s˚ dˆng trong
các tr˜Ìng hÒp: ki∫m soát ti∏n trình, t¸ Îng th¸c thi các hành Îng ho∞c các
lu™t nghiªp vˆ ph˘c t§p. Cßu trúc cıa mÎt trigger có d§ng ECA : rule name::
Event(e) IF condition DO action. Trigger CSDL ph¶n lÓn có th∫ chia thành hai
lo§i: Data Manipulation Language(DML) vàvà Data Definition Language (DDL)
triggers. Lo§i ¶u tiên ˜Òc th¸ thi khi thao tác vÓi d˙ liêu, lo§i th˘ hai ˜Òc kích
ho§t khi có các s¸ kiªn DDL x£y ra nh˜ t§o b£ng ho∞c login, commit, roll-back..
2.7.2
Các hª thËng c£m ng˙ c£nh
Thu™t ng˙ “c£m ng˙ c£nh" ˜Òc ˜a ra l¶n ¶u tiên bi Bill Schilit [10], tác gi£ ã
‡nh nghæa ng˙ c£nh là v‡ trí, là ‡nh danh cıa các Ëi t˜Òng và s¸ thay Íi cıa
các Ëi t˜Òng này sau ó làm cho ch˜Ïng trình thích nghi vÓi ng˙ c£nh. Có nhi∑u
nghiên c˘u ã t™p trung vào ‡nh nghæa các thu™t ng˙ c£m ngh˙ c£nh. Lu™n án
t™p trung vào các hª thËng c£m ng˙ c£nh s˚ dˆng d˙ liªu ng˙ c£nh mÎt cách tr¸c
ti∏p t¯ các c£m bi∏n v™t l˛. Hª thËng có th∫ c£m nh™n ˜Òc nhi∑u lo§i ng˙ c£nh
trong môi tr˜Ìng nó ho§t Îng nh˜ v‡ trí, Î t´ng tËc, nhiªt Î, Î £m, thÌi thi∏t..
Và viªc x˚ l˛ cıa hª thËng này là phˆ thuÎc vào ng˙ng˙ c£nh t˘c là ph£n ˘ng vÓi
các thay Íi cıa ng˙ c£nh.
Ch˜Ïng 3. Mô hình hóa và ki∫m ch˘ng các hª thËng CSDL
3.1 GiÓi thiªu
MÎt trigger là mÎt o§n mã có cu pháp, không mã hóa nh˜ng không có ng˙ nghæa.
Chính vì v™y, ta chø có th∫ ki∫m tra liªu mÎt trigger ho§t Îng có d®n ∏n xung
Ît ràng buÎc d˙ liªu hay các triggers có th∫ d®n ∏n các vòng l∞p vô h§n không
b¨ng cách th¸c thi chúng ho∞c i∑u tra t¯ng b˜Óc mÎt. Vì nh˙ng l˛ do này, các
nghiên c˘u v∑ mÎt khung làm viªc hình th˘c cho mô hình hóa và ki∫m ch˘ng các
triggers CSDL là c¶n thi∏t. Thêm vào ó, n∏u ta có th∫ chø ra r¨ng th¸c thi cıa
các trigger là úng thÌi i∫m thi∏t k∏ thì nó có th∫ làm gi£m chi phí phát tri∫n
các ˘ng dˆng CSDL. Trong ch˜Ïng này, chúng tôi ∑ xußt mÎt ph˜Ïng pháp mÓi
∫ mô hình hóa và ki∫m ch˘ng hª thËng CSDL có trigger s˚ dˆng Event-B giai
o§n thi∏t k∏. fi t˜ng chính cıa ph˜Ïng pháp xußt phát t¯ s¸ t˜Ïng Áng vè cÏ
ch∏ ho§t Îng cıa trigger và s¸ kiªn Event-B. ¶u tiên, chúng tôi ∑ xußt mÎt t™p
lu™t ∫ chuy∫n Íi mÎt hª thËng CSDL có trigger sang mô hình Event-B, sau ó
ki∫m tra mÎt cách hình th˘c liªu hª thËng có th‰a mãn ràng buÎc d˙ liªu và phát
hiªn các vòng l∞p vô h§n b¨ng viªc ch˘ng minh các mênh ∑ c¶n ch˘ng minh cıa
máy Event-B. ◊u i∫m cıa ph˜Ïng pháp là hª thËng CSDL có th∫ chuy∫n Ëi sang
mô hình Event-B mÎt cách tr¸c ti∏p. Các tính chßt quan trÂng ˜Òc ch˘ng minh
mÎt cách toán hÂc thông qua ch˘ng minh mªnh ∑ c¶n ch˘ng minh vì v™y tính
úng ≠n cıa các tính chßt này ˜Òc £m b£o. Ph˜Ïng pháp này có giá tr‡ vì nó
£m b£o ˜Òc hª thËng tránh ˜Òc mÎt sË lÈi nghiêm trÂng thÌi i∫m thi∏t k∏.
Ngoài ra, vÓi công cˆ hÈ trÒ Rodin thì các vßn ∑ s≥ ˜Òc ch˘ng minh t¸ Îng, nó
s≥ làm gi£m bÓt Î ph˘c t§p so vÓi ch˘ng minh thı công. Ph˜Ïng pháp này cÙng
có th∫ dπ dàng áp dˆng ∫ th¸c thi mÎt công cˆ hÈ trÒ mô hình hóa bán t¸ Îng
7
8
mÎt CSDL sang Event-B. i∑u này cÙng kh≠c phˆc nh˜Òc i∫m v∑ Î ph˘c t§p
khi mô hình hóa cıa các ph˜Ïng pháp hình th˘c khi∏n chúng tr nên khó áp dˆng
trong phát tri∫n ph¶n m∑m.
3.2 Mô hình hóa và ki∫m ch˘ng hª thËng triggers
3.2.1
Mô hình hóa hª thËng CSDL
MÎt hª thËng CSDL th˜Ìng ˜Òc thi∏t k∏ bi các ph¶n t˚ nh˜ b£ng, khung nhìn vÓi
các ràng buÎc và các triggers. Khi ng˜Ìi dùng th¸c thi các câu lªnh Insert, Delete
và Update, nh˙ng s¸ thay Íi này có th∫ làm kích ho§t triggers Áng thÌi cÙng
ph£i tuân theo các ràng buÎc ‡nh tr˜Óc. Các qui t≠c chuy∫n Íi mÎt hª CSDL
sang Event-B ˜Òc tÍng k∏t B£ng 3.1.
B£ng 3.1: Qui t≠c chuy∫n Íi gi˙a CSDL và Event-B
Rule 1.
Rule 2
Rule 3
Rule 4
Rule 5
Rule 6
3.2.2
Database definitions
db = hT , C , Gi
t = hr1 , .., rm i
ri = hfi1 , .., fin i
Primary key constraint
Constraint C
Trigger E
Event-B concepts
DB M , DB C
T = TYPE1 ⇥ TYPE2 ⇥ TYPEn
t 2T
f : TYPE1 !
77 T
Invariant I
Event Evt
Hình th˘c hóa triggers
B£ng 3.2 mô t£ cách chuy∫n mÎt trigger sang mÎt s¸ kiªn Event-B trong ó i∑u
kiªn cıa s¸ kiªn là hÒp cıa lo§i trigger và i∑u kiªn trigger x£y ra. Ph¶n th¸c thi
cıa trigger ˜Òc chuy∫n Íi thành ph¶n thân cıa s¸ kiªn Event-B. Ta xét tr˜Ìng
hÒp Ïn gi£n là thân chø ch˜a các câu lªnh DML Ïn. Mã hóa nÎi dung cıa trigger
˜Òc mô t£ trong B£ng 3.3
B£ng 3.2: Hình th˘c hóa mÎt trigger
IF (e)
ON (c)
ACTION (a)
3.2.3
WHEN (e ^ condition)
THEN (a) END
Ki∫m ch˘ng các tính chßt cıa hª thËng
Sau khi chuy∫n Íi, vÓi các ∞c i∫m cıa Event-B và công cˆ hÈ trÒ, ta có th∫ ki∫m
ch˘ng ˜Òc các tính chßt sau:
B£ng 3.3: Mã hóa hành Îng cıa trigger
ANY r
INSERT INTO T
VALUES (value1,..,valuen)
WHEN (r 2 T ^ e ^ c)
THEN T := T [ r
END
ANY v
DELETE FROM T
WHERE hcolumn1 = some valuei
WHEN (v 2 TYPE1 ^ e ^ c)
THEN t := t
f (v )
END
ANY v 1, v 2
UPDATE T
SET column1=value, column2=value2
WHERE hcolumn1 = some valuei
WHEN v 1 2 TYPE1 ^ v 2 2 TYPE2 ^ e ^ c
THEN t := {1 7! value1, 2 7! value2}
END
t
Ch˜Ïng 3 Mô hình hóa và ki∫m ch˘ng các hª thËng CSDL
• Vòng l∞p vô h§n: Vì mÎt trigger có th∫ kích ho§t trigger khác, nên nó có th∫
d®n ∏n vòng l∞p vô h§n. Tình tr§ng này có th∫ x£y ra khi sau mÎt chuÈi các s¸
kiªn thì tr§ng thái cıa hª thËng không thay Íi. Có hai cách ∫ phát hiªn tính
chßt này sau khi mô hình hóa b¨ng ph˜Ïng pháp ã ∑ xußt. Các th˘ nhßt, ta
ch˘ng minh mªnh ∑ c¶n ch˘ng minh deadlock-freeness (DLKF), mênh ∑ này
là hÒp cıa các i∑u kiªn cıa các s¸ kiªn Event-B, bi∫u diπn mÎt cách hình th˘c:
I (v ), P (c ) ` G1 (v ) _ ... _ Gn (v ), trongtrong ó v là bi∏n, I (v ) là bßt bi∏n, Gi (v )
làlà i∑u kiªn cıa s¸ kiªn. Trong mÎt sËt r˜Ìng hÒp, mªnh ∑ DLKF không suy
diπn ˜Òc t¯ t™p các bßt bi∏n I (v ) và h¨ng ràng buÎc, ta s≥ ch˘ng minh t§i mÎt
thÌi i∫m luôn có 1 s¸ kiªn ˜Òc kích ho§t b¨ng ch˘ng minh hÎi cıa các i∑u
kiªn luôn úng tr˜Óc và sau khi th¸c thi event, t˘c là ch˜ngs minh mªnh ∑ c¶n
ch˘ng minh INV (bao gÁm c£ s¸ kiên INITIALISATION ).
• B£o toàn ràng buÎc: VÓi ph˜Ïng pháp chuy∫n Íi ∑ xußt, mÎt trigger không vi
ph§m các luât này n∏u I (v ), G (w , v ), S (w , v , v 0 ) ` I (v 0 ). ây cÙng chính là mªnh
∑ c¶n ch˘ng minh INV cıa máy Event-B.
3.3 Case study: Hª thËng qu£n l˛ nhân s¸
3.3.1
Mô t£
Trong mÎt hª thËng CSDL cho ˘ng dˆng qu£n l˛ nhân s¸ có hai b£ng EMPLOYEES
(gÁm hai tr˜Ìng id và level) vàvà b£ng BONUS (gÁm hai tr˜Ìng id và amount).
Ÿng dˆng có yêu c¶u ràng buÎc v∑ d˙ liªu nh˜ sau.: Tr˜Ìng amount cıa BONUS
>=10 n∏u level cıa nhân viên >5. . Hª CSDL này ˜Òc thi∏t k∏t hai triggers th¸c
hiªn nhiªm vˆ sau:
Trigger 1. N∏u b£ng nhân viên employee ˜Òc c™p nhât thì bonus t´ng lên 10 .
Trigger 2. N∏u tr˜Ìng amount cıa nhân viên BONUS ˜Òc t´ng >=10 thì level
cıa nhân viên t´ng lên 1.
3.3.2
Mô hình hóa
MÎt ph¶n ∞c t£ Event-B cıa ví dˆ ˜Òc th∫ hiªn Hình 3.1, Hình 3.2 và Hình 3.3.
CONTEXT TRIGGER C
SETS
TYPES
TABLE NAMES
CONSTANTS
TBL EMPL
TBL BONUS
AXIOMS
axm1 : partition(TYPES, {insert}, {update}, {delete})
axm2 : TBL EMPL ✓ {1 7! N, 2 7! N}
axm3 : TBL BONUS ✓ {1 7! N, 2 7! N}
axm4 : partition(TABLE NAMES, {employees}, {bonus})
END
Hình 3.1: Ng˙ c£nh Event-B
10
MACHINE TRIGGER M
SEES TRIGGER C
VARIABLES
bonus
empl
f bonus
f empl
type
INVARIANTS
inv1 : bonus 2 P (TBL BONUS)
inv2 : empl 2 P (TBL EMPL)
inv3 : type 2 TYPES
inv4 : f bonus 2 N !
77 N
inv5 : f empl 2 N !
77 N
SYS CTR : 8 eid.eid 2 dom(empl) ^ pk empl(eid) > 5 ) pk bonus(eid) > 10
INF LOOP : (type = update ^ table = BONUS) _ (type = update ^ table = EMPL)
END
Hình 3.2: Máy Event-B
Event trigger1 =
b
any
eid
when
grd1 : type = update
grd2 : table = EMPL
grd3 : eid 2 dom(empl)
then
act1 : type := update
act3 : table := BONUS
act5 : bonus := {eid 7! (pk bonus(eid) + 10)} bonus
act5 : pk bonus(eid) := pk bonus(eid) + 10
end
Event trigger2 =
b
any
eid
when
grd1 : type = update
grd2 : table = BONUS
grd3 : pk bonus(eid) 10
then
act1 : type := update
act2 : table := EMPL
act3 : empl := {eid 7! (pk empl(eid) + 1)} empl
end
Hình 3.3: Mã hóa trigger
3.3.3
Ki∫m ch˘ng các thuÎc tính
• B£o toàn ràng buÎc: Tính chßt này ˜Òc hình th˘c hóa bi bßt bi∏n SYS CTR :
8 eid .eid 2 dom (empl ) ^ pk empl (eid ) > 5 ) pk bonus (eid ) > 10.
Ta c¶n ch˘ng minh bßt bi∏n này b£o toàn tr˜Óc và sau khi các s¸ kiªn th¸c thi,
mªnh ∑ c¶n ch˘ng minh t˜Ïng ˘ng cıa trigger 1 ˜Òc mô t£ nh˜ B£ng 3.4. Hai
s¸ kiªn Trigger 1 và Trigger 2 cıa máy DB M sinh ra các mªnh ∑ c¶n ch˘ng
minh t˜Ïng ˘ng là trigger1/SYS CTR/INV, trigger2/SYS CTR/INV.
B£ng 3.4: INV PO of event trigger 1.
8 nid .nid 2 dom(empl rec) ^ pk empl (nid ) > 5 ) pk bonus(nid ) > 10
emplid 2 dom(empl rec)
type = update
table = EMPL
`
8 nid .nid 2 dom(empl rec) ^ pk empl (nid ) > 5
) (pk bonus {emplid 7! pk bonus(emplid ) + 10})(nid ) > 10
trigger1/
SYS CTR/
INV
• Vòng l∞p vô h§n: – mˆc 3.2.3, bßt bi∏n INF LOOP là mªnh ∑ tuy∫n cıa các
i∑u kiªn cıa s¸ kiªn ˜Òc s˚ dˆng ∫ phát hiªn vòng l∞p vô h§n. N∏u bßt bi∏n
này b£o toàn vÓi hai s¸ kiªn thì th¸c thi cıa hai triggers s≥ d®n ∏n vòng l∞p vô
h§n. Mªnh ∑ c¶n ch˘ng minh cıa tính chßt này ˜Òc th∫ hiªn B£ng 3.5.
B£ng 3.5: Mªnh ∑ c¶n ch˘ng minh INV cıa trigger 1
8 nid .(nid 2 dom(empl rec) ^
type = update ^ table = BONUS ^
pk bonus(nid ) > 10) _ (type = update ^ table = EMPL)) ^
emplid 2 dom(bonus rec)
table = BONUS ^ pk bonus(emplid ) > 10
`
8 nid .(nid 2 dom({emplid 7! pk empl (emplid ) + 1} empl rec) ^
update = update ^ EMPL = BONUS ^
pk bonus(nid ) > 10) _
(update = update ^ EMPL = EMPL)
trigger 1
/INF LOOP
/INV
3.4 Cài ∞t
T¯ ph˜Ïng pháp ∑ xußt Mˆc 3.2, chúng tôi ã cài ∞c mÎt công cˆ Trigger2B
∫ hÈ trÒ mô hình hóa và ki∫m ch˘ng mÎt hª thËng CSDL có trigger. Công cˆ này
có th∫ sinh ra các file d˜Ói ‡nh d§ng XML ∫ có th∫ s˚ dˆng làm ¶u vào cho các
công cˆ hÈ trÒ khác cıa Event-B nh˜ Rodin. Ki∏n trúc cıa công cˆ ˜Òc mô t£
nh˜ Hình 3.4.
Hình 3.4: Architecture of Trigger2B tool
Ch˜Ïng 4. Mô hình hóa và ki∫m ch˘ng các hª thËng c£m ng˙
c£nh
4.1 GiÓi thiªu
C£m ng˙ canh cıa mÎt ˘ng dˆng liên quan tÓi kh£ n´ng áp ˘ng, ph£n hÁi và
Î nh§y c£m cıa ˘ng dˆng vÓi các thay Íi cıa ng˙ c£nh [5]. Theo nghæa hµp thì
mÎt hª thËng c£m ng˙ c£nh có th∫ xem nh˜ mÎt hª thËng h˜Óng s¸ kiªn nghæa
là nó nh™n các s¸ kiªn g˚i khi có s¸ thay Íi v∑ ng˙ c£nh và ph£n hÁi l§i các s¸
11
12
kiªn này vÓi các tri th˘c v∑ ng˙ c£nh ang có. Hành vi cıa các hª thËng c£m ng˙
c£nh th˜Ìng là ph˘c t§p và không ch≠c ch≠n. ã có nhi∑u k∏t qu£ nghiên c˘u vÓi
nhi∑u cách tiªp c™n khác nhau nh˜ mô hình hóa vai trò Ëi t˜Òng, mô hình hóa d¸a
trên ontology, mô hình hóa d¸a trên logic [5]. MÎt sË nghiên c˘u cÙng ˜Òc ra các
khung làm viªc cho mô hình hóa ng˙ c£nh. Tuy nhiên, theo quan i∫m cıa chúng
tôi, ch˜a có mÎt cách ti∏p c™n nào mô hình hóa c£m ng˙ c£nh trên mÎt vài khía
c§nh nh˜ s¸ kiªn cıa môi tr˜Ìng, các lu™t ng˙ c£nh và tính không ch≠c ch≠n. HÏn
th∏ n˙a, mô hình §t ˜Òc có th∫ ˜Òc ki∫m ch˘ng ∫ £m b£o tính úng ≠n cıa
hª thËng. Trong ch˜Ïng này, chúng tôi ∑ xußt s˚ dˆng Event-B ∫ mô hình hóa và
ki∫m ch˘ng các hª thËng c£m ng˙ c£nh. Các óng góp cıa ∑ xußt này là (1) Bi∫u
diπn t¸ nhiên các hª thËng c£m ng˙ c£nh b¨ng các thành ph¶n Event-B. ∑ xußt
mÎt t™p lu™t ‡nh nghæa các thành ph¶n c£m ng˙ c£nh mÎt cách hình th˘c. ây là
ph˜Ïng pháp d¸a trên làm m‡n cho phép xây d¸ng hª thËng theo t¯ng b˜Óc. (2)
Sau khi hình th˘c hóa, các tính chßt quan trÂng cıa hª thËng ˜Òc ki∫m ch˘ng
qua các mªnh ∑ c¶n ch˘ng minh cıa cÏ ch∏ làm m‡n mà không qua b˜Óc chuy∫n
Íi trung gian nào.
4.2 Hình th˘c hóa tính chßt c£m ng˙ c£nh
4.2.1
Mô hình hóa hª thËng c£m ng˙ c£nh
Các lu™t chuy∫n Íi gi˙a mÎt hª thËng c£m ng˙ c£nh và mô mÎt mô hình Event-B
˜Òc trình bày B£ng 4.1
B£ng 4.1: Chuy∫n Íi gi˙a các mô hình c£m ng˙ c£nh và thành ph¶n Event-B
Rule
Rule
Rule
Rule
4.2.2
1
2
3
4
Context-aware concepts
Context data CD
Context rules r = he, c, ai
Environments triggers E
Context constraints CC
Event-B notations
Sets, Constants
Events
Events
Invariants
Mô hình hóa t´ng d¶n s˚ dˆng làm m‡n
Trên th¸c t∏, phát tri∫n các hª thËng c£m ˘ng th˜Ìng ˜Òc xây d¸ng t¯ các yêu
c¶u cÏ b£n, sau ó ˜Òc xây d¸ng d¶n khi có thêm các yêu c¶u v∑ các th¸c th∫ ng˙
c£nh và tri th˘c suy diπn. Ví dˆ, hª thËng bÍ sung thêm các bÎ c£m bi∏n ∫ lßy
thêm nhi∑u lo§i d˙ liªu ng˙ c£nh. Hª thËng cÙng có thêm các lu™t ng˙ c£nh ∫ x˚
l˛ các d˙ liªu này. Lúc này, hª thËng mÓi v®n ph£i th‰a mãn nh˙ng ràng buÎc ã
˜Òc thi∏t l™p. Vì v™y, ta c¶n có mÎt ph˜Ïng pháp mô hình hóa phù hÒp cho qui
trình phát tri∫n ti∏n hóa này. Hình 4.1 mô t£ mÎt ph˜Ïng pháp mô hình hóa ti∏n
hóa d¸a trên ph˜Ïng pháp ã ∑ xußt Mˆc 4.2.1.
CÏ ch∏ làm m‡n cho phép mô hình hóa các hª thËng c£m ng˙ c£nh theo t¯ng b˜Óc.
Event-B có hai cÏ ch∏ làm m‡n chÁng và làm m‡n theo chi∑u dÂc. Trong ó cÏ ch∏
th˘ hai, các bi∏n tr¯u t˜Òng v®n tÁn t§i trong các máy cˆ th∫ cùng vÓi các bi∏n
bÍ sung. Chính vì v™y ph˜Ïng pháp d¸a trên cÏ ch∏ này phù hÒp vÓi mÎt hª thËng
c£m ng˙ c£nh ˜Òc m rÎng b¨ng viªc bÍ sung các c£m bi∏n.
Ch˜Ïng 4 Mô hình hóa và ki∫m ch˘ng các hª thËng c£m ng˙ c£nh
Hình 4.1: Mô hình hóa ti∏n hóa s˚ dˆng làm m‡n
• Ph¶n d˙ liªu tænh: khi mÎt c£m bi∏n ˜Òc thêm vào hª thËng, ta có th∫ s≥ ph£i
gi£i quy∏t vÓi các ki∫u d˙ liªu khác. Ph˜Ïng pháp ∑ xußt mô hình hóa nó nh˜
mÎt ng˙ c£nh mÓi m rÎng t¯ các ng˙ c£nh mô hình tr¯u t˜Òng.
• Ph¶n Îng: Ta b≠t ¶u b¨ng mô hình hóa các hành vi chung cıa hª thËng khi
mÓi b≠t ¶u, sau ó làm m‡n các máy này b¨ng các máy cˆ th∫. Trong các máy
ã làm m‡n các bi∏n mÓi ˜Òc thêm có th∫ tham chi∏u ∏n các thành ph¶n d˙
liªu ng˙ c£nh. Các s¸ kiªn cıa mÎt máy làm m‡n có th∫ k∏ th¯a các s¸ kiªn cıa
máy tr¯u t˜Òng.
4.3 Case study: Hª thËng Adaptive Cruise Control
4.3.1
Mô t£ ban ¶u
Hª thËng ACC i∑u khi∫n tËc Î cıa ôtô d¸a trên i∑u kiªn l§i xe Áng thÌi ˜Òc
có ch˘c n´ng c£m ng˙ c£nh nh˜ nh™n bi∏t v™t c£n phía tr˜Óc nhÌ s˚ dˆng c£m
bi∏n tr˜Óc xe. Ô tô có tËc Î Ëi a và ˜Òc thi∏t l™p khi b≠t ¶u khi Îng xe.
N∏u không phát hiªn v™t c£n phía tr˜Óc thì s≥ t´ng và gi£m tËc Î. N∏u xe d¯ng
và không có v™t c£n thì tËc Î xe l§i ˜Òc thi∏t l™p là tËi a.
Hª thËng ACC luôn th‰a mãn ràng buÎc ng˙ c£nh là tËc Î luôn trong kho£ng an
toàn t˘c là không v˜Òt quá tËc Î cho phép.
4.3.2
Mô hình hóa hª thËng ACC
Trong k‡ch b£n này, hª thËng có ba c£m bi∏n, theo ph˜Ïng pháp ˜Òc ∑ xußt
Mˆc4.2, chúng ta ∞c t£ hª thËng ban ¶u vÓi mÎt máy và ng˙ c£nh là ACC M 0
và Target (Hình 4.2).
4.3.3
Làm m‡n: BÍ sung c£m bi∏n thÌi ti∏t và Î nhÆn m∞t ˜Ìng
Hai c£m bi∏n này ˜Òc g≠ng vÓi hª thËng t˜Ïng t¸ nh˜ c£m bi∏n phát hiªn ch˜Óng
ng§i v™t,g˚i d˙ liªu v∑ hª thËng. Các lu™t ng˙ c£nh ˜Òc m rÎng ∫ x˚ l˛ các s¸
kiªn g˚i d˙ liªu v∑ hai c£m bi∏n này nh˜ sau: “Khi mÎt ôtô di chuy∫n trong i∑u
kiªn trÌi m˜a ho∞c m∞t ˜Ìng không tËt thì ACC gi£m tËc Îc ôtô". VÓi hª thËng
mÓi này, hª thËng c¶n £m b£o trong i∑u kiªn thÌi ti∏t ho∞c ˜Ìng xßu thì tËc Î
nh‰ hÏn tËc Î tËi a.
CONTEXT Target
CONSTANTS
TARGET DETECTION
MAX SPEED
INC
AXIOMS
axm1 : TARGET DETECTION = BOOL
axm2 : MAX SPEED 2 N
axm3 : INC < MAX SPEED
axm4 : INC 2 N
END
Hình 4.2:
EVENTS
Event TargetDetected =
b
when
grd1 : target det = TRUE
grd2 : speed > INC
then
act1 : speed := speed INC
end
Event TargetUndetected =
b
when
grd1 : target det = FALSE
grd2 : speed < MAX SPEED INC
then
act1 : speed := speed + INC
end
END
∞c t£ Event-B cho hª thËng ban ¶u
Mô hình làm m‡n: D¸a trên ph˜Ïng th˘c ã giÓi thiªu 4.2.2, ng˙ c£nh Weather Road
m rÎng ng˙ c£nh Target bi∫u diπn d˙ liªu ng˙ c£nh cıa các c£m bi∏n mÓi. Ta
thêm hai s¸ kiªn cho máy làm m‡n. S¸ kiªn th˘ nhßt bi∫u diπn lu™t mÓi và không
làm m‡ s¸ kiªn nào máy tr¯u t˜Òng. Nó bi∫u diπn hành vi cıa hª thËng khi các
c£m bi∏n g˚i d˙ liªu bi∫u diπn tr§ng thái thÌi ti∏t có m˜a hay ˜Ìng xßu. Trong
khi s¸ kiªn TargetUndetected làm m‡n s¸ kiªn cıa máy tr¯u t˜Òng. Ràng buÎc ng˙
c£nh ˜Òc hình th˘c hóa thành bßt bi∏n cxt ct (Hình 4.3).
4.3.4
Ki∫m ch˘ng các tính chßt cıa hª thËng
Các ràng buÎc ng˙ c£nh ˜Òc chuy∫n Íi thành các mªnh ∑ bßt bi∏n. Vì v™y, ta
có th∫ ch˘ng minh tính úng ≠n cıa hª thËng b¨ng ch˘ng minh các mªnh ∑ c¶n
ch˘ng minh INV.
B£ng 4.2: Ch˘ng minh tính b£o toàn ng˙ c£nh
target det = TRUE ) speed < MAX SPEED
target det = TRUE
speed > INC
`
target det = TRUE ) speed INC < MAX SPEED
TargetDetected/ctx ct1/INV
Các mªnh ∑ c¶n ch˘ng minh cho các bßt bi∏n cıa c£ máy tr¯u t˜Òng là làm m‡n
nh˜ sau:
• Machine ACC M 0: “TargetDetected/ctx ct1/INV " (Hình 4.2) and “TargetUndetected/ctx ct1/INV "
• Machine ACC M 1: “TargetUndetected/ctx ct/INV " and “RainSharp/ctx ct/INV "
Ch˜Ïng 5. Mô hình hóa các yêu c¶u không chính xác
5.1 GiÓi thiªu
Các ph˜Ïng pháp hình th˘c là các kˇ thu™t toán hÂc s˚ dˆng ∫ mô t£ các tính
chßt mô hình hª thËng. Nh˙ng ph˜Ïng pháp này ˜a ra các khung làm viªc ∫ ∞c
14
Ch˜Ïng 5 Mô hình hóa các yêu c¶u không chính xác
CONTEXT Weather Road
EXTENDS Target
CONSTANTS
RAINING
SHARP
AXIOMS
axm1 : RAINING = BOOL
axm2 : SHARP = BOOL
END
MACHINE ACC M1
REFINES ACC M0
SEES Weather Road
VARIABLES
isRain
speed
target det
isSharp
INVARIANTS
inv1 : isRain 2 RAINING
cxt ct : isRain = TRUE _ isSharp = TRUE ) speed <
MAX SPEED
inv3 : isSharp 2 SHARP
EVENTS
Event TargetUndetected =
b
extends TargetUndetected
when
grd1 : target det = F ALSE
grd2 : speed < M AX SP EED IN C
grd3 : isRain = FALSE
grd4 : isSharp = FALSE
then
act1 : speed := speed + IN C
end
Event RainSharp =
b
when
grd1 : isRain = TRUE _ isSharp = TRUE
then
act1 : speed := speed INC
end
END
Hình 4.3: Mô hình làm m‡n cıa hª thËng ACC
t£ và ki∫m ch˘ng tính úng ≠n cıa các hª thËng nói chung và các hª thËng h˜Óng
s¸ kiªn nói riêng th˜Ìng òi h‰i các yêu c¶u mô t£ chính xác. Tuy nhiên, chúng
ta th˜Ìng ph£i Ëi m∞t vÓi nh˙ng mô t£ không chính xác có các thu™t ng˙ không
rõ ràng, nh™p nh¨ng hay không ch≠c ch≠n nh˜ “rßt l§nh", “xa", ho∞c “kém quan
trÂng", bi vì nh˙ng ng˜Ìi tham gia phát tri∫n ph¶n m∑m th˜Ìng không quan tâm
nhi∑u ∏n mô t£ các hª thËng mÎt cách chính xác. Chính vì v™y, nh˙ng khung làm
viªc hình th˘c có th∫ s˚ dˆng ∫ phân tích và bi∫u diπn các yêu c¶u không chính
xác là c¶n thi∏t. Ph˜Ïng pháp vÓi t™p mÌ ˜Òc ∑ xußt bi Zadeh [16] là mÎt trong
nh˙ng khung làm viªc nh˜ v™y, trong ó các lu™t Fuzz If-Then ˜Òc s˚ dˆng ∫
bi∫u diπn các yêu c¶u không chính xác. MÎt cách tÍng quát, các yêu c¶u hª thËng
bao gÁm các ∞c t£ ch˘c n´ng có th∫ ˜Òc ki∫m tra cùng m˘c tr¯u t˜Òng tr˜Óc
khi b≠t ¶u các b˜Óc phát tri∫n ti∏p theo. Các yêu c¶u này ˜Òc bi∫u diπn d˜Ói
d§ng các lu™t If-Then mÌ có th∫ là ı bi∫u diπn nh˜ng v®n có yêu c¶u các kˇ thu™t
ti∏p theo ∫ ki∫m ch˘ng các tính chßt mÎt cách hình th˘c trên nhi∑u khía c§nh ∫
16
phát hiªn và gi£i quy∏t các xung Ît. Các lu™t If-Then mÌ ˜Òc chuy∫n sang các
khung làm viªc hình th˘c khác nh˜ PetriNet [7, 15] ho∞c k˛ hiªu Z [9].
Ch˜Ïng này s˚ dˆng lÒi th∏ cıa cÏ ch∏ làm m‡n Event-B ∫ mô hình hóa các hª
thËng h˜Óng s¸ kiªn ˜Òc mô t£ bi các t™p lu™t If-Then mÌ. óng góp cıa ch˜Ïng
là (1) ˜a ra mÎt t™p lu™t chuy∫n Íi t¯ các lu™t If-Then mÌ sang mô t£ Event-B
(2) s˚ dˆng cÏ ch∏ làm m‡n cıa Event-B ∫ hình th˘c hóa các lu™t If-Then mÌ.
5.2 Mô hình hóa và ki∫m ch˘ng các yêu c¶u m s˚ dˆng Event-B
Trong ph¶n này, lu™n án giÓi thiªu mÎt cách ti∏p c™n ∫ bi∫u diπn các thu™t ng˙
mÌ b¨ng l˛ thuy∏t t™p hÒp cÍ i∫n. D¸a trên các bi∫u diπn này, chúng tôi ∑ xuát
mÎt t™p lu™t ∫ chuy∫n Íi các lu™t If-Then mÌ sang Event-B. Sau ó s˚ dˆng cÏ
ch∏ làm m‡ ∫ mô hình hóa các hª ‡nh thÌi.
5.2.1
Bi∫u diπn các thu™t ng˙ mÌ b¨ng t™p hÒp cÍ i∫n
Corollary 5.1. MÎt t™p các yêu c¶u mÌ ˜Òc ‡nh nghæa rõ ràng có th∫ ˜Òc ∞c
t£ b¨ng các t™p hÒp cÍ i∫n.
Ch˘ng minh. Gi£ s˚ các yêu c¶u mÌ cıa mÎt hª thËng ˜Òc ∞c t£ bi FR =
{FRi }, FRi = {xi , mi , i , µs , Yi , Pi }, i = 1, n. Ta thßy xi , mi ˜Òc xem nh˜ các
bi∏n trong ∞c t£, Pi ˜Òc mô t£ b¨ng các t™p giá tr‡. Ta xét n∏u i Yi có th∫
˜Òc ∞c t£ b¨ng mÎt t™p cÍ i∫n trong ó i là mÎt hedge, Yi là mÎt bÎ sinh cıa
mÎt generator cıa mªnh ∑ mÌ. Vì FR là mÎt t™p h˙u h§n các lu™t nên hedges và
generators trong hª thËng ˜Òc thi∏t l™p bi các t™p khác nhau vàvà Y , t˜Ïng
˘ng. Theo ‡nh nghæa 4 và 5 i Yi là ⇥ Y , trong ó µs là mÎt hàm t¯ t™p N tÓi .
Vì v™y, mÈi ph¶n t˚ cıa FR có th∫ ˜Òc ∞c t£ bi các t™p hÒp cÍ i∫n.
⌅
5.2.2
Mô hình hoá các tr§ng thái rÌi r§c cıa các yêu c¶u không chính xác
vnMÎt hª thËng bao gÁm mÎt t™p các yêu c¶u FRi , i = 1, n ˜Òc mô hình hóa bi
mÎt mô hình Event-B FRB = hFR C , FR M i, trong ó FR C vàvà FR M là ng˙
c£nh và máy Event-B t˜Ïng ˘ng. Chúng tôi ∑ xußt mÎt ph¶n các lu™t ˜Òc s˚
dˆng ∫ ánh x§ các yêu c¶u không chính xác vào các ph¶n t¯ Evemt-B. Nguyên
t≠c quan trÂng là vÓi ph˜Ïng pháp này ta có th∫ b£o toàn cßu trúc và bi∫u diπn
toàn bÎ các yêu c¶u mÌ s˚ dˆng k˛ hiªu Event-B. Các lu™t chuy∫n Íi:
• Lu™t 1. hedges i , generators Yi và giá tr‡ Pi trong mÎt t™p các yêu c¶u có th∫
˜Òc chuy∫n Íi thành ba t™p hÒp t˜Ïng ˘ng , Y , and P . Các t™p này ˜Òc ˜a
ra trong ng˙ c£nh FR C .
• Lu™t 2. Các bi∏n xi , mi trong mÈi FRi ˜Òc ánh x§ ∏n các bi∏n xi , mi cıa máy
Event-B FR M .
• Lu™t 3. MÈi bi∏n xi ˜Òc bi∫u diπn thành ⇥ Y , trong ó mi 2 ⇥ P (Corollary
5.1).
• Lu™t 4. MÈi yêu c¶u FRi ˜Òc mô hình hóa bi mÎt s¸ kiên evi trong máy Event-B
FR M
L˜u ˛ là ßy chø là các qui t≠c bi∏n Íi mÎt ph¶n, ta c¶n thêm vào nhi∑u thành
ph¶n khác ∫ §t ˜Òc ∞c t£ Event-B hoàn chønh(Hình 5.1).
Ch˜Ïng 5 Mô hình hóa các yêu c¶u không chính xác
CONTEXT FR C
SETS
P
Y
END
MACHINE FR M
SEES FR C
VARIABLES
x i
m i
INVARIANTS
inv1 : xi 2 P ( ⇥ Y)
inv2 : mi 2 P ( ⇥ P)
inv3 : I
EVENTS
Event FRi =
b
when
grd1 : xi = { i 7! Yi }
then
act1 : mi := { i 7! Pi }
act2 : xi := { j 7! Yj }
end
END
Hình 5.1: A part of Event-B specification for discrete transitions modeling
5.2.3
Mô hình hóa các hª mÌ
Tr˜Óc tiên ta ‡nh nghæa các lu™t If-Then mÌ ‡nh thÌi có d§ng nh˜ sau: IF x(t)
is A THEN y(t) is B. Ti∏p tˆc ph˜Ïng pháp ˜Òc giÓi thiêu trong [4], n∏u mÎt
yêu c¶u mÌ FR i ch˘a mÎt bi∏n phˆ thuÎc thÌi gian nào ó, thì ta s≥ làm m‡n s¸
kiªn t˜Ïng ˘ng cıa máy tr¯u t˜Òng (Mˆc 5.2.2, Lu™t 5). Áng thÌi, ta cÙng ã giÓi
thiªu trong Lu™t 4 là n∏u mÎt bi∏n x ˜Òc ∞c t£ nh˜ mÎt thành viên cıa ⇥ Y ,
trong ó là mÎt t™p hÒp cıa các fuzzy hedges, Y là mÎt t™p mÌ. T˜Ïng t¸, ta
7
⇥ P.
thêm các bi∏n liên tˆc xc cıa máy làm m‡n ˜Òc khai báo nh˜ sau xc 2 R !
Lu™t án giÓi thiªu hai lu™t cho mô hình hóa các tr§ng thái liêu tˆc phˆ thuÎc thÌi
gian cıa yêu c¶u nh˜ sau:
• Lu™t 6: N∏u mÎt bi∏n x i or m i (trong mÎt yêu c¶u mÌi FR i) g≠n vÓi trˆc
thÌi gian, thì s¸ kiªn t˜Ïng ˘ng s≥ ˜Òc làm m‡n. MÎt bi∏n t .t 2 R ∫ bi∫u diπn
thÌi gian s≥ ˜Òc thêm vào máy làm m‡n.
• Rule 7: Các bi∏n phˆ thuÎc thÌi gian (trong Rule 1) ˜Òc thay th∏ bi các hàm
thÌi gian và bßt bi∏n ràng buÎc trong máy làm m‡n.
5.3 Case study: Container Crane Control
5.3.1
Mô t£
C¶n c©u container ˜Òc s˚ dˆng ∫ nhßc và th£ hàng ˜Òc s˚ dˆng trong các c£ng.
MÎt t™p hÒp các yêu c¶u mÌ mô t£ hª thËng nh˜ sau:
• FR1 N∏u c¶n c©u ang v‡ tr‡ ban ¶u, thì tËc Î m˘c nhanh.
• FR2 . N∏u kho£ng cách t¯ c¶n c©u ∏n container xa, thì tËc Î m˘c trung bình.
• FR3 . N∏u kho£ng cách ∏n container là trung bình thì tËc Î ˜Òc i∑u chønh
m˘c thßp.
• FR4 . N∏u kho£ng cách là g¶n thì tËc Î là rßt ch™m.
• FR5 . N∏u c¶n c©u trên container thì tËc Î b¨ng 0.
5.3.2
Mô hình hóa hª thËng Container Crane Control
Mô hình hóa các hành vi rÌi r§c:
Áp dˆng các lu™t chuy∫n Íi ã trình bày trong Mˆc 5.2.2, t™p các yêu c¶u cıa hª
thËng ˜Òc chuy∫n Íi sang mô hình Event-B nh˜ sau:
• Áp dˆng Lu™t 1 : Fuzzy hedges, generators và các giá tr‡ trong t™p các yêu c¶u
˜Òc chuy∫n thành các t™p HEDGES, DISTANCE và POWER trong ng˙ c£nh
Event-B Crane C 0.
• Áp dˆng Lu™t 2 : Các hàm thuÎc cıa hedges vàvà giá tr‡ mÌ ˜Òc bi∫u diπn nh˜
các hàm sË nguyên. Ví dˆ: h deg : HEDGES ! N. Ta có axiom cho giá tr‡ này
nh˜ sau h deg (very ) = 3 ^ h deg (quite ) = 2 ^ h deg (precise ) = 1.
Ta ti∏p tˆc hình th˘c hóa ph¶n Îng cıa mô hình vÓi các chuy∫n Íi.
• Áp dˆng Lu™t 3 : Các bi∏n trong yêu c¶u ˜Òc chuy∫n thành các thành ph¶n
Event-B nh˜ distance and power. Ki∫u cıa hai bi∏n này ˜Òc bi∫u diπn nh˜ các
bßt bi∏n inv 1 and inv 2.
• Áp dˆng Lu™t 5 : MÈi yêu c¶u không chính xác FRi cıa hª thËng ˜Òc chuy∫n
thành mÎt s¸ kiên evti , i = 1, 5.
Mô hình hóa các hành vi liên tˆc:
Ta làm m‡n mô hình chuy∫n Íi mˆc tr˜Óc b¨ng viªc xem xét hª thËng mÎt cách
chi ti∏t và cˆ th∫ hÏn. Trên th¸c t∏, mÈi di chuy∫n cıa c¶n c©u g≠n vÓi trˆc thÌi
gian vì nó di chuy∫n mÎt cách liên lˆc trong khi tËc Î thì ˜Òc i∑u chønh rÌi r§c.
Ta áp dung các lu™t ˜Òc ˜a ra trong mˆc 5.2.3 nh˜ sau:
• Áp dˆng Lu™t 6 : N´m s¸ kiªn ˜Òc làm m‡n trong máy làm m‡ Crane M 1, bi∏n
∏m thÌi gian t cÙng ˜Òc bÍ sung.
• Apply Rule 7 : Replace dis by disc (the distance which is time-dependent). The
new variable of refined machine disc and one of abstract machine dis have a gluing
variant (inv 3).
Ch˜Ïng 6. Ki∫m ch˘ng các yêu c¶u hª thËng không chính xác
6.1 GiÓi thiªu
Các ph˜Ïng pháp hình th˘c ˜Òc s˚ dˆng không chø ∞c t£ mà còn phát hiªn và
gi£i quy∏t các xung Ît cıa yêu c¶u hª thËng. Trong Ch˜Ïng 5, lu™n án ∑ xußt
mÎt ph˜Ïng pháp mÓi ∫ mô hình hóa các yêu c¶u hª thËng không chính xác ˜Òc
mô t£ b¨ng các ph¶n t˚ Event-B. Tuy nhiên, ki∫m ch˘ng các thuÎc tính quan trÂng
cıa các hª thËng này ch˜a ˜Òc ∑ c™p ∏n. Các tính chßt phÍ bi∏n cıa các hª
thËng là tính an toàn và tính ho§t Îng. Tính an toàn b£o £m ∫ hª thËng không
rÏi vào tr§ng thái xßu trong khi các tính chßt ho§t Îng £m b£o mÎt tr§ng thái
tËt cıa hª thËng (tính d¯ng, ho§t Îng, ti∏n trình). Ch˜Ïng 6 cıa lu™n án s≥ giÓi
thiªu mÎt ph˜Ïng pháp d¸a trên làm m‡n mÓi ∫ mô hình hóa và ki∫m ch˘ng c£
18
- Xem thêm -