Đăng ký Đăng nhập
Trang chủ Phương pháp mô hình hóa và kiểm chứng các hệ thống hướng sự kiện [tt]...

Tài liệu Phương pháp mô hình hóa và kiểm chứng các hệ thống hướng sự kiện [tt]

.PDF
27
721
62

Mô tả:

Ñ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 bi 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 bi 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 bi 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 bi 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 bi 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 bi 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 bi 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 bi 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 bi tính toán v‡ t¯ b™c mÎt ˜Òc m rÎng bi Equality bi 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∏ bi 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 bi 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∏ 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 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 bi 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 khi Î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", bi 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 bi 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£ bi 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£ bi 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 bi 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£ bi 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 bi 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 bi 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∏ bi 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 -

Tài liệu liên quan