Ñ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 §i hÂc Công nghª, §i hÂc
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
-Trungtâmthôngtinth˜viên,§ihÂcQuËcgiaHàNÎi
Chẽng 1. Tng quan v lun ỏn
1.1 L do láa chn ti
Mụ hỡnh húa l mẻt trong cỏc cỏch thc hiêu quÊ quÊn l ẻ phc tĐp trong
phỏt trin phản mm, nú cho phộp thit k v ỏnh giỏ cỏc yờu cảu ca hê thậng.
Mụ hỡnh húa khụng chứ cung còp cỏc nẻi dng mẻt cỏch trác quan m cũn cÊ cỏc
nẻi dung k tá. Cỏc k thut kim th cú th ềc s dng trong phỏt trin phản
mm thụng thèng kim tra liêu mẻt phản mm thác thi cú tha món yờu cảu
ca ngèi dựng. Tuy nhiờn, kim 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 vi trèng hềp nhng khụng Êm bÊo ềc hê
thậng chĐy ỳng trong mi trèng hềp. Kim chng phản mm l mẻt trong nhng
phẽng phỏp mĐnh hiêu quÊ tỡm ra lẩi hoc chng minh khụng cú lẩi mẻt cỏch

1
2 Tng quan v lun ỏn
tÊ chớnh xỏc v chc nng v hnh vi ca hê thậng. Chớnh vỡ nhng l do trờn,
cỏc phẽng phỏp mụ hỡnh húa v kim chng phự hềp cho cỏc hê thậng ny l cản
thit. Nu ta cú th kim chng cỏc tớnh chòt quan trng ca hê thậng sểm thỡ s
tit kiêm ềc chi phớ phỏt trin. Cỏc phẽng phỏp ny vỡ th nu giÊm ềc ẻ
phc tĐp trong chng minh thỡ s cú khÊ nng ỏp dng vo thác t cao. Lun ỏn
xuòt cỏc phẽng phỏp mểi Đt ềc cỏc yờu cảu trờn băng s dng phẽng
phỏp hỡnh Event-B. Event-B ềc dáa trờn l thuyt tp 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 ca mụ hỡnh Event-B ềc
bÊo Êm bi cỏc chng minh hỡnh thc. Cỏc cụng c hẩ trề ềc chung còp cho
c tÊ v chng minh Event-B trờn nn tÊng Rodin. Vỡ võy, s dng Event-B lm
phẽng phỏp hỡnh thc mụ hỡnh húa v kim chng cỏc hê thậng hểng sá kiên
cú ròt nhiu u im.
1.2 Mc tiờu
Lun ỏn a ra mẻt cỏch tip cn khỏc so vểi cỏc nghiờn cu hiên tĐi. Thay vỡ
phõn tớch mẻt hê thậng hểng sá kiên tng quỏt, chỳng tụi tp trung vo s dng
Event-B mụ hỡnh húa cỏc hê thậng hểng sá kiên c trng nh cỏc hê thậng
CSDL, cỏc hê thậng cÊm ng cÊnh. Lun ỏn xuòt cỏc phẽng phỏp hiêu khụng
chứ mụ hỡnh húa cỏc hnh vi ềc biu din băng cỏc lut If-Then m cũn hỡnh
thc húa cỏc tớnh chòt quan trng băng cỏc thnh phản Event-B. Tớnh ỳng n
ca cỏc tớnh chòt ny ềc chng minh mẻt cỏch toỏn hc băng viêc chng minh
cỏc mênh cản chng minh ềc sinh ra bi Event-B. Cụng c Rodin ềc s
dng trong hẩ trề quỏ trỡnh mụ hỡnh húa v chng minh tá ẻng. Lun ỏn cú mc
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. Lun ỏn giểi thiêu phẽng phỏp mểi dáa trờn lm mn mụ hỡnh húa
v kim chng tớnh chòt an ton v tớnh hoĐt ẻng ca hê thậng.
1.3 úng gúp mểi ca lun ỏn
Cỏc nghiờn cu úng gúp ca lun ỏn bao gm
1. Lun ỏn xuòt mẻt phẽng phỏp mụ hỡnh húa v kim chng cỏc hê thậng

6 giểi thiê u phẽng phỏp kim chng tớnh chòt an ton v hoĐt ẻng ca cỏc yờu
cảu khụng chớnh xỏc. Chẽng 7 tng kt lun ỏn v a ra hểng phỏt trin.
Chẽng 2. Kin th c cẽ s
2.1 Temporal logic
Propositional temporal logic (PTL) l sá m rẻng ca logic mênh trong ú mụ
tÊ mẻt chuẩi cỏc trĐng thỏi nhng khoÊng thèi gian khỏc nhau gi l thèi im
tc thèi. Mẻt thnh phản cẽ bÊn PTL l mẻt cụng thc logic bc 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ỏctoỏnt^, _ ,ơ;vcỏc
3
4
toỏn t thèi gian (always), (eventually), v (next), U (until"). Cỳ phỏp
ca mẻt cụng thc PTL ềc mụ tÊ nh trong BÊng 2.1
BÊng 2.1: Cỳ phỏp ca cụng thc PTL
hformulai ::= htermi {_ htermi}
htermi > ::= hfactori {^ hfactori}
hfactori > ::= hprimaryi {U hprimaryi}
hprimaryi > ::= hatomc propositioni >
|ơhprimaryi >
|hprimaryi >
| hprimaryi >
| hprimaryi >
2.2 L thuyt tp hềp
Tp hềp l cỏc ậi tềng cẽ bÊn ềc s dng nh nghổa cỏc khỏi niêm khỏc
trong toỏn hc. Ngụn ng ca l thuyt tp hềp dáa trờn cỏc quan hê cẽ bÊn gi
l thnh viờn. A l mẻt thnh viờn ca B (A 2 B), cú nghổa l B cha A nh mẻt
phản t ca nú [14]. Cú nhiu nh nghổa cẽ bÊn khỏc ca l thuyt tp hềp nh
l tp m, quan hê, hm, biu din lamda, vv
2.3 Tp mè v lut If-Then mè
Trong phỏt trin ng dng 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 dng cỏc thut ng mè nh ròt

VDM l vit tt ca The Vienna Development Method" bao gm mẻt nhúm cỏc
k thut cho c tÊ hỡnh thc v phỏt trin ca 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 mm thnh cỏc mụ hỡnh
[8]. Cỏc mụ hỡnh ny ềc c tÊ nh cỏc ậi tềng v cỏc hnh ẻng trờn cỏc ậi
tềng trong ú cỏc ậi tềng biu din cỏc trĐng thỏi input, output v bờn trong
ca hê thậng. VDM cú ngụn ng c tÊ VDM-SL bao gm mụ hỡnh toỏn hc ềc
xõy dáng t cỏc d liêu cẽ bÊn nh tp hềp, danh sỏch v ỏnh xĐ cựng vểi cỏc
hnh ẻng thay i trĐng thỏi ca mụ hỡnh. VDM-SL cú nh nghổa hỡnh thc 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 thuyt tp hềp v tớnh toỏn v t bc 1. Mẩi ậi tềng cú
mẻt kiu riờng, ềc biu din bi mẻt tp các Đi trong c tÊ hiên tĐi. Mẻt khớa
cĐnh ca Z l s dng ngụn ng tá nhiờn. Z s dng toỏn hc a ra vòn ,
tỡm ra cỏc giÊi phỏp v chng minh thit k láa chn phự hềp vểi c tÊ. Z cung
còp cẽ ch lm mn xõy dáng hê thậng dản dản. Mẻt ti liêu c tÊ Z bao gm
cỏc oĐn hỡnh thc v phi hỡnh thc [12].
2.4.3 Phẽng phỏp B
BlmẻtphẽngphỏpctÊ,thitkvvitmóchocỏchêthậngphảnmm.
tng chớnh ca B l bt ảu băng mẻt mụ hỡnh ròt tru tềng, sau ú thờm dản
cỏc chi tit vo cỏc mụ hỡnh c th tip theo [2]. B a ra cỏc khỏi niêm v mỏy
tru tềng úng gúi cỏc thnh phản toỏn hc, hăng, tp hềp, bin v mẻt tp hềp
cỏc hnh ẻng trờn cỏc bin ny. Cỏc thnh phản ny ềc cha trong cỏc mụdun
cú tờn cú th ềc s dng cỏc mụdun khỏc.
2.5 Event-B
Event-B [3]lmẻtphẽngphỏphỡnhthcmụhỡnhhúavphõntớchmcmụhỡnh.
c tớnh ch chật ca Event-B l s dng l thuyt tõp hềp lm k hiêu mụ tÊ, s
dng cẽ ch lm mn biu din cỏc hê thậng cỏc mc tru tềng khỏc nhau v
s dng cỏc chng minh toỏn hc kim chng sá ng nhòt gia cỏc mc lm
mn. Mẻt còu trỳc mụ hỡnh Event-B cẽ bÊn bao gm 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Ê

(INV), convergence (VAR), deadlock-freeness (DLF).
2.6 Rodin tool
Lun ỏn s dng cụng c Rodin phiờn bÊn 2.8 [1] l mụi trèng Eclipse mụ hỡnh
húa v chng minh trong Event-B. Nú ềc xõy dáng trờn nn tÊng ca Eclipse
bao gm cỏc cụng c hẩ trề mụ hỡnh húa plug-ins. Rodin cú giao diên phong phỳ
bao gm cỏc ca s nh proving, Event-B editor
Ca 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 ny ềc chng minh tá ẻng hoc tẽng tỏc
thụng qua cỏc ca s mênh v mc tiờu.
Ca s Event-B: Bao gm cỏc giao diên cho phộp chứnh sa cỏc mỏy v ng cÊnh.
Nu ngèi s dng mó húa khụng chớnh xỏc, ca 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ú nhiu loĐi hê thậng hểng sá kiên nh giao diên ca phản mm, cỏc hê thậng
sinh lut ềc s dng trong trớ tuê nhõn tĐo khi iu kiên ỳng thỡ thác thi mẻt
hnh ẻng, hay trong cỏc ậi tềng hoĐt ụng khi thay i giỏ tr hay thuẻc tớnh
ca ậi tềng [11]. Trong lun ỏn ny, chỳng tụi xột n hai ng dng ú l cỏc
hê thậng CSDL v cÊm ng cÊnh. CÊ hai hê thậng ny u s dng cỏc lut dĐng
ECA biu din cỏc hnh 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ê gia cỏc ậi tềng v cỏc
quan hê, hnh ẻng cho thao tỏc d liêu v tonton vàn d liêu. Cỏc hê thậng
CSDL quan hê hiên Đi s dng cỏc lut hoĐt ẻng nh trigger CSDL ỏp ng
lĐi cỏc sá kiên xÊy ra bờn trong v b ờn ngoi ca 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 dng trong
cỏc trèng hềp: kim soỏt tin trỡnh, tá ẻng thác thi cỏc hnh ẻng hoc cỏc
lut nghiêp v phc tĐp. Còu trỳc ca mẻt trigger cú dĐng ECA : rule name::
Event(e) IF condition DO action. Trigger CSDL phản lển cú th chia thnh hai
loĐi: Data Manipulation Language(DML) vv Data Definition Language (DDL)

mẻt cỏch toỏn hc thụng qua chng minh mênh cản chng minh vỡ vy tớnh
ỳng n ca cỏc tớnh chòt ny ềc Êm bÊo. Phẽng phỏp ny cú giỏ tr vỡ nú
Êm bÊo ềc hê thậng trỏnh ềc mẻt sậ lẩi nghiờm trng thèi im thit k.
Ngoi ra, vểi cụng c hẩ trề Rodin thỡ cỏc vòn s ềc chng minh tá ẻng, nú
s lm giÊm bểt ẻ phc tĐp so vểi chng minh th cụng. Phẽng phỏp ny cng
cú th d dng ỏp dng 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∏ bi 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
Database definitions Event-B concepts
Rule 1. db = hT , C , Gi DB M , DB C
Rule 2 t = hr
1
, ,r
m
i T = TYPE
1
⇥ TYPE
2
⇥ TYPE

END
ANY v
DELETE FROM T WHEN (v 2 TYPE
1
^ e ^ c)
WHERE hcolumn 1=some valuei THEN t := t  f (v)
END
ANY v 1, v2
UPDATE T WHEN v 1 2 TYPE
1
^ v2 2 TYPE
2
^ e ^ c
SET column1=value, column2=value2 THEN t := {1 7! value1, 2 7! value2}t
WHERE hcolumn 1=some valuei END
Chẽng 3 Mụ hỡnh húa v kim chng cỏc hê thậng CSDL
Vũng lp 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 lp vụ hĐn. Tỡnh trĐng ny cú th xÊy ra khi sau mẻt chuẩi cỏc sá
kiên thỡ trĐng thỏi ca hê thậng khụng thay i. Cú hai cỏch phỏt hiên tớnh
chòt ny sau khi mụ hỡnh húa băng phẽng phỏp ó xuòt. Cỏc th nhòt, ta
chng minh mênh cản chng minh deadlock-freeness (DLKF), mờnh ny
l hềp ca cỏc iu kiên ca cỏc sá kiên Event-B, biu din mẻt cỏch hỡnh thc:
I (v), P(c) ` G
1
(v) _ _ G
n
(v),trongtrongúv l bin, I (v) l bòt bin, G
i
(v)
ll iu kiên ca sá kiên. Trong mẻt sật rèng hềp, mênh DLKF khụng suy

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 2P(TBL BONUS)
inv2 : empl 2P(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

8 nid.nid 2 dom(empl rec) ^ pk empl(nid) > 5 ) pk bonus(nid) > 10
emplid 2 dom(empl rec)
type = update trigger1/
table = EMPL SYS CTR/
` INV
8 nid.nid 2 dom(empl rec) ^ pk empl(nid) > 5
) (pk bonus {emplid 7! pk bonus(emplid) + 10})(nid) > 10
Vũng lp vụ hĐn: mc 3.2.3,bòtbinINF LOOP l mênh tuyn ca cỏc
iu kiên ca sá kiên ềc s dng phỏt hiên vũng lp vụ hĐn. Nu bòt bin
ny bÊo ton vểi hai sá kiên thỡ thác thi ca hai triggers s dđn n vũng lp vụ
hĐn. Mênh cản chng minh ca tớnh chòt ny ềc th hiên BÊng 3.5.
BÊng 3.5: Mênh cản chng minh INV ca 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 trigger1
` /INF LOOP
8 nid.(nid 2 dom( {emplid 7! pk empl(emplid)+1}empl rec ) ^ /INV
update = update ^ EMPL = BONUS ^
pk bonus(nid) > 10) _
(update = update ^ EMPL = EMPL)
3.4 Ci t
T phẽng phỏp xuòt Mc 3.2,chỳngtụiócicmẻtcụngcTrigger2B
hẩ trề mụ hỡnh húa v kim chng mẻt hê thậng CSDL cú trigger. Cụng c ny
cú th sinh ra cỏc file dểi nh dĐng XML cú th s dng lm ảu vo cho cỏc
cụng c hẩ trề khỏc ca Event-B nh Rodin. Kin trỳc ca cụng c ềc mụ tÊ
nh Hỡnh 3.4.
Hỡnh 3.4: Architecture of Trigge r2B tool
Chẽng 4. Mụ hỡnh húa v kim chng cỏc hê thậng cÊm ng

Rule 1 Context data CD Sets, Constants
Rule 2 Context rules r = he, c, ai Events
Rule 3 Environments triggers E Events
Rule 4 Context constraints CC Invariants
4.2.2 Mụ hỡnh húa tng dản s dng lm mn
Trờn thác t, phỏt trin 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 thc suy din. Vớ d, hê thậng b sung thờm cỏc bẻ cÊm bin lòy
thờm nhiu loĐi d liêu ng cÊnh . Hê thậng cng cú thờm cỏc lut ng cÊnh x
l cỏc d liêu ny. Lỳc ny, hê thậng mểi vđn phÊi tha món nhng rng buẻc ó
ềc thit lp. Vỡ vy, ta cản cú mẻt phẽng phỏp mụ hỡnh húa phự hềp cho qui
trỡnh phỏt trin tin húa ny. Hỡnh 4.1 mụ tÊ mẻt phẽng phỏp mụ hỡnh húa tin
húa dáa trờn phẽng phỏp ó xuòt Mc 4.2.1.
Cẽ ch lm mn cho phộp mụ hỡnh húa cỏc hê thậng cÊm ng cÊnh theo tng bểc.
Event-B cú hai cẽ ch lm mn chng v lm mn theo chiu dc. Trong ú cẽ ch
th hai, cỏc bin tru tềng vđn tn tĐi trong cỏc mỏy c th cựng vểi cỏc bin
b sung. Chớnh vỡ vy phẽng phỏp dáa trờn cẽ ch ny 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 bin.
Chẽng 4 Mụ hỡnh húa v kim chng cỏc hê thậng cÊm ng cÊnh
Hỡnh 4.1: Mụ hỡnh húa tin húa s dng lm mn
Phản d liêu tổnh: khi mẻt cÊm bin ềc thờm vo hê thậng, ta cú th s phÊi
giÊi quyt vểi cỏc kiu 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 tru tềng.
Phản ẻng: Ta bt ảu băng mụ hỡnh húa cỏc hnh vi chung ca hê thậng khi
mểi bt ảu, sau ú lm mn cỏc mỏy ny băng cỏc mỏy c th. Trong cỏc mỏy
ó lm mn cỏc bin mểi ềc thờm cú th tham chiu n cỏc thnh phản d
liêu ng cÊnh. Cỏc sá kiên ca mẻt mỏy lm mn cú th k tha cỏc sá kiên ca
mỏy tru tềng.
4.3 Case study: Hê thậng Adaptive Cruise Control
4.3.1 Mụ tÊ ban ảu

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
Hỡnh 4.2: c tÊ Event-B cho hê thậng ban ảu
Mụ hỡnh lm mn: Dáa trờn phẽng thc ó giểi thiêu 4.2.2,ngcÊnhWeather Road
m rẻng ng cÊnh Target biu din d liêu ng cÊnh ca cỏc cÊm bin mểi. Ta
thờm hai sá kiên cho mỏy lm mn. Sá kiên th nhòt biu din lut mểi v khụng
lm m sá kiên no mỏy tru tềng. Nú biu din hnh vi ca hê thậng khi cỏc
cÊm bin gi d liêu biu din trĐng thỏi thèi tit cú ma hay èng xòu. Trong
khi sá kiên TargetUndetected lm mn sá kiên ca mỏy tru tềng. Rng buẻc ng
cÊnh ề c hỡnh thc húa thnh bòt bin cxt ct (Hỡnh 4.3).
4.3.4 Kim chng cỏc tớnh chòt ca hê thậng
Cỏc rng buẻc ng cÊnh ềc chuyn i thnh cỏc mênh bòt bin. Vỡ vy, ta
cú th chng minh tớnh ỳng n ca hê thậng băng chng minh cỏc mênh cản
chng minh INV.
BÊng 4.2: Chng minh tớnh bÊo ton ng cÊnh
target det = TRUE ) speed < MAX SPEED
target det = TRUE

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 < MAX SPEED INC
grd3 : isRain = FALSE
grd4 : isSharp = FALSE
then
act1 : speed := speed + INC
end
Event RainSharp b=
when
grd1 : isRain = TRUE _ isSharp = TRUE
then
act1 : speed := speed INC
end
END
Hỡnh 4.3: Mụ hỡnh lm mn ca hê thậng ACC
tÊ v kim chng tớnh ỳng n ca 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 hi cỏc yờu cảu mụ tÊ chớnh xỏc. Tuy nhiờn, chỳng
ta thèng phÊi ậi mt vểi nhng mụ tÊ khụng chớnh xỏc cú cỏc thut ng khụng
rừ rng, nhp nhăng hay khụng chc chn nh ròt lĐnh" , xa", hoc kộm quan
trng", bi vỡ nhng ngèi tham gia phỏt trin phản mm thèn g khụng quan tõm

i
, m
i
,
i
,à
s
, Y
i
, P
i
}, i = 1, n.Tathòyx
i
, m
i
ềc xem nh cỏc
bin trong c tÊ, P
i
ềc mụ tÊ băng cỏc tp giỏ tr. Ta xột nu
i
Y
i
cú th
ềc c tÊ băng mẻt tp c in trong ú
i
l mẻt hedge, Y
i
l mẻt bẻ sinh ca
mẻt generator ca mênh mè. Vỡ FR l mẻt tp hu hĐn cỏc lut nờn hedges v
generators trong hê thậng ềc thit lp bi cỏc tp khỏc nhau vv Y ,tẽng

, m
i
trong mẩi FR
i
ềc ỏnh xĐ n cỏc bin x
i
, m
i
ca mỏy
Event-B FR M .
Lut 3. Mẩi bin x
i
ềc biu din thnh Y ,trongúm
i
2 P (Corollary
5.1).
Lut 4. Mẩi yờu cảu FR
i
ềc mụ hỡnh húa bi mẻt sá kiờn ev
i
trong mỏy Event-B
FR M
Lu l òy chứ l cỏc qui tc bin i mẻt phản, ta cản thờm vo nhiu thnh
phản khỏc Đt ềc c tÊ Event-B hon 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

i
7! P
i
}
act2 : x
i
:= {
j
7! Y
j
}
end
END
Hình 5.1: ApartofEvent-Bspecificationfordiscretetransitionsmodeling
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™t5).ÁngthÌi,tacÙ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
thêm các bi∏n liên tˆc x
c
cıa máy làm m‡n ˜Òc khai báo nh˜ sau x
c
2 R 7!  ⇥ P.
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≠nvÓitrˆ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

p dng Lut 2: Cỏc hm thuẻc ca hedges vv giỏ tr mè ềc biu din nh
cỏc hm sậ nguyờn. Vớ d: h deg : HEDGES ! N.Tacúaxiomchogiỏtrny
nh sau h deg(very)=3^ h deg(quite)=2^ h deg(precise)=1.
Ta tip tc hỡnh thc húa phản ẻng ca mụ hỡnh vểi cỏc chuyn i.
p dng Lut 3 : Cỏc bin trong yờu cảu ềc chuyn thnh cỏc thnh phản
Event-B nh distance and power. Kiu ca hai bin ny ềc biu din nh cỏc
bòt bin inv1 and inv2.
p dng Lut 5 : Mẩi yờu cảu khụng chớnh xỏc FR
i
ca hê thậng ềc chuyn
thnh mẻt sá kiờn evt
i
, i = 1, 5.
Mụ hỡnh húa cỏc hnh vi liờn tc:
Ta lm mn mụ hỡnh chuyn i mc trểc băng viêc xem xột hê thậng mẻt cỏch
chi tit v c th hẽn. Trờn thác t, mẩi di chuyn ca cản câu gn vểi trc thèi
gian vỡ nú di chuyn mẻt c ỏch liờn lc trong khi tậc ẻ thỡ ềc iu chứnh rèi rĐc.
Ta ỏp dung cỏc lut ềc a ra trong mc 5.2.3 nh sau:
p dng Lut 6:NmsákiênềclmmntrongmỏylmmCrane M 1,bin
m thèi gian t cng ềc b sung.
Apply Rule 7 :Replacedis by dis
c
(the distance which is time-dependent). The
new variable of refined machine dis
c
and one of abstract machine dis have a gluing
variant (inv3).
Chẽng 6. Kim chng 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 thc ềc s dng khụng chứ c tÊ m cũn phỏt hiên v

6.3 Phõn tớch tớnh an ton v hoĐt ẻng trong Event-B
Event-B cung còp mẻt cỏch biu din cỏc thuẻc tớnh an ton mẻt cỏch trác tip
băng cỏc bòt bin. Vỡ vy, ta cú th chng minh tớnh ỳng n ca cỏc tớnh chòt
ny băng chng minh mênh INV . Event-B khụng hẩ trề c tÊ cỏc tớnh chòt
hoĐt ẻng mẻt cỏch trác tip nhng ta cú th thác thi theo phẽng phỏp suy
din trong bi bỏo [6]kimchngcỏctớnhchòtnhexistence (P), progress
((P
1
) P
2
)), persistence (P), trong ú P l mẻt cụng thc logic bc mẻt,
v l cỏc toỏn t chuân ca Linear Temporal Logic (LTL).
6.4 Mụ hỡnh húa cỏc tớnh chòt ca yờu cảu khụng chớnh xỏc
6.4.1 Mụ hỡnh húa tớnh an ton
Corollary 6.1. Vểi cỏc lut chuyn i ó xuòt, cỏc tớnh chòt an ton ềc bÊo
ton bi cỏc hnh ẻng trong yờu cảu hê thậng khụng chớnh xỏc.
6.4.2 Mụ hỡnh húa tớnh hoĐt ẻng
Lun ỏn xuòt mẻt phẽng phỏp dáa trờn lm mn vểi viêc b sung thờm cỏc
lut m rẻng ng cÊnh v lm mn mỏy Event-B nh sau:
Lut 6. Giỏ tr mè P, Y vv hedges ềc chuyn thnh cỏc hm tẽng ng
deg
P
! N, deg
y
Y : Y ! N, deg
H
: ! N.
Lut 7: Thờm mẻt a variant ỏnh xĐ tểi bin cú xuòt hiên trong biu thc thuẻc
tớnh hoĐt ụng Q.
Lut 8. Lm mn cỏc sá kiên biu din cho cỏc yờu cảu If-Then băng hai sá kiên:

i
.x
i
= Y
i
)
Corollary 6.4. Vểi cỏc lut chuyn i ó xuòt, nu mẻt tp lut If-Then mè
l hẻi t v deadlock-free t mẻt biu thc logic trĐng thỏi Q(x) trong ú x l mẻt
bin thỡ thuẻc tớnh trĐng thỏi ơQ(x) s luụn xÊy ra. Mẻt cỏch hỡnh thc, ta cú
{FR}`ơQ(x).
6.5 Kim chng hê thậng Container Crane Control
Hê thậng cú mẻt thuẻc tớnh an ton Êm bÊo tậc ẻ ca motor khụng tậc ẻ
cao khi khoÊng cỏch khụng (I). ng thèi hê thậng cng cản tha món tớnh chòt
t v trớ ban ảu, mẻt lỳc no ú cản câu s trờn container(Q). Biu din mẻt
cỏch hỡnh thc, ta cản kim chng {FR}`I v {FR}`Q.
6.5.1 Lm mn: Mụ hỡnh húa tớnh chòt hoĐt ẻng
Ta thác hiên chin lềc lm mn nh ó trỡnh by Mc 6.4.2 mụ hỡnh húa
tớnh chòt hoĐt ẻng mong muận. ảu tiờn, ta ỏp dng Rule 6 m rụng ng cÊnh
CraneCtrl C 0 thnh CraneCtrl C1 băng viêc a thờm ba hm ỏnh xĐ cỏc tp
mè sang cỏc giỏ tr sậ. c tÊ ca ng cÊnh ềc mụ tÊ mẻt phản nh sau:
CONTEXT CraneCtrl C1
EXTENDS CraneCtrl C0
CONSTANTS
deg HED, deg POWER, d DIS
AXIOMS
axm4 : deg HED : HEDGES ! N
axm5 : deg HED(very)=3 ^ deg HED(quite)=2
^ deg HED(precise)=1
END
Tip theo, ta lm min mỏy Crane M0 cú Crane M1 vểi 05 sá kiên hẻi t v 05

{precise 7! above}
act2 : d :=
deg DIS(above)
end
Event evt4 OE b=
Status ordinary
extends evt
4
when
grd1 : distance =
{precise 7! close}
grd2 : d =
deg
DIS(close)
grd3 : d =
deg DIS(above)
then
act1 : power :=
{very 7! slow}
act2 : distance :=
{precise 7! above}
act2 : d :=
deg DIS(above)
end
6.5.2 Ki∫m ch˘ng thuÎc tính
Hª thËng có mÎt tính chßt ã ˜Òc hình th˘c hóa thành mÎt bßt bi∏n
inv4:ran(dist)={close})¬ran(power )={fast}. MÈi mªnh ∑ c¶n ch˘ng minh
này ˜Òc sinh ra cho mÈi s¸ kiªn cıa máy Crane M 0.B£ng6.1 th∫ hiªn mªnh ∑
c¶n ch˘ng minh inv4 cıa s¸ kiªn evt4
B£ng 6.1: INV PO of event evt4

thậng, lun ỏn tp trung vo cỏc ng dng c trng l hê thậng cẽ s d liêu bao
gm cỏc triggers v cÊm ng cÊnh. Hai ng dng ny cú tớnh chòt v chc nng
cung còp riờng. Tuy nhiờn trong hai hê thậng, trigger nờn v cỏc quy tc ng cÊnh
cú còu trỳc tẽng tá hỡnh thc nh dĐng ECA. Phẽng phỏp xuòt ca chỳng
tụi ềc dáa trờn cẽ ch lm viêc tẽng tá gia lut ECA v mẻt sá kiên Event-B.
Vỡ l do ny, quỏ trỡnh xõy dáng mụ hỡnh l tá nhiờn v d dng. Hẽn na, lun
ỏn s dng Event-B hỡnh thc húa hê thậng, chỳng ta khụng cản bòt k bểc
trung gian no kim th tớnh ỳng n ca hê thậng.
Trong phản th hai, lun ỏn cng úng gúp lển vo viêc phõn tớch hê thậng hểng
sá kiên theo quy nh ca yờu cảu khụng chớnh xỏc. Mc dự yờu cảu khụng chớnh
xỏc thèng ềc tỡm thòy trong quỏ trỡnh phỏt trin phản mm, nhng nhng
nghiờn cu ch yu giÊi quyt vòn mụ hỡnh v kim chng cỏc yờu cảu chớnh
xỏc. Phản ny trỡnh by phẽng phỏp mểi dáa trờn qui tc lm mn, trong ú cỏc
yờu cảu ềc mụ phng bi If-Then mè. Cỏc quy tc ó ềc chuyn i sang mẻt
tp hềp cỏc sá kiên Event-B. Lun ỏn cng xuòt phẽng phỏp d áa trờn lm mn
cú th kim chng tớnh chòt an ton v hoĐt ẻng ca hê thậng.
7.2 HĐn ch
Bờn cĐch cỏc kt quÊ ó Đt ềc, lun ỏn vđn cũn mẻt sậ hĐn ch
Phẽng phỏp xuòt cho mụ hỡnh v kim chng cỏc hê thậng cẽ s d liêu
khụng hẩ trề cho suy din trác tip v thuẻc tớnh kt thỳc, trong khi nú l mẻt
trong nhng c tớnh mong muận m ngèi phỏt trin phản mm muận kim tra.
22
Chẽng 7 Kt lun
Phẽng phỏp x l cỏc trèng hềp ẽn giÊn ca mẻt chuẩi cỏc cõu lênh DML
khụng cha lng nhau v cỳ phỏp trigger ảy .
Do thiu sá hẩ trề kiu d liêu nguyờn thy trong Event-B, lun ỏn chứ cú th
lm phong phỳ thờm mụ hỡnh d liêu ng cÊnh băng cỏch kt hềp vểi cỏc Plug-in
mểi. Bậi cÊnh l d liêu thè ng ròt phc tĐp v cú nhiu loĐi d liêu. Hẽn na,
mẻt ng dng cÊm ng cÊnh thác thèng cha d liêu thèi gian cú liờn quan.
Tuy nhiờn, Event-B khụng hẩ trề logic thèi gian, do ú mụ hỡnh v kim chng

minh tớnh liveness mi giai oĐn lm mn cng l mẻt mc tiờu. Hẽn na, nn
tÊng l thuyt suy din v liveness trong Event-B cng cản phÊi ềc m rẻng cho
trèng hềp tng quỏt bao gm sá cụng băng giÊ nh. iu ú cng lm cho nú cú
th xỏc minh cỏc thuẻc tớnh liveness quan trng khỏc nh persistence, progress.