Tóm tắt Luận án Tiến sỹ ngành Công nghệ thông tin: Phương pháp mô hình hóa và kiểm chứng các hệ thống hướng sự kiện

ÑI H≈C QU»C GIA HÀ NÀI<br /> Tr˜Ìng §i hÂc Công nghª<br /> <br /> Lê HÁng Anh<br /> <br /> Ph˜Ïng pháp mô hình hóa và ki∫m ch˘ng các hª<br /> thËng h˜Óng s¸ kiªn<br /> <br /> Tóm t≠t lu™n án ti∏n sˇ ngành công nghª thông tin<br /> Chuyên ngành: Công nghª ph¶n m∑m<br /> Mã sË: 62.48.10.01<br /> <br /> Hà NÎi, 2014<br /> <br /> Công trình ˜Òc hoàn thành t§i Khoa Công nghª thông tin, Tr˜Ìng<br /> QuËc Gia Hà NÎi.<br /> Ng˜Ìi h˜Óng d®n khoa hÂc:<br /> PGS. TS Tr˜Ïng Ninh Thu™n<br /> PGS. TS Ph§m B£o SÏn<br /> <br /> Ph£n biªn 1: ........................<br /> Ph£n biªn 2: ........................<br /> Ph£n biªn 3: ........................<br /> <br /> Có th∫ tìm hi∫u lu™n án t§i<br /> - Th˜ viªn QuËc gia Viªt Nam<br /> - Trung tâm thông tin th˜ viên ,<br /> <br /> §i hÂc QuËc gia Hà NÎi<br /> <br /> §i hÂc Công nghª,<br /> <br /> §i hÂc<br /> <br /> Ch˜Ïng 1. TÍng quan v∑ lu™n án<br /> 1.1 L˛ do l¸a chÂn ∑ tài<br /> 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<br /> 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.<br /> 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<br /> 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<br /> 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<br /> 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ó<br /> 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ª<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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ô<br /> 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<br /> 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ˆ<br /> 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<br /> ó 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<br /> 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<br /> 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ó<br /> 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<br /> 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<br /> 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<br /> Ë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Ë<br /> hành Îng [11]. Trong ki∏n trúc h˜Óng s¸ kiªn, các lu™n d§ng ECA ˜Òc ∑ xußt<br /> 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<br /> ‡nh tr˜Óc. Lu™t ECA có d§ng: On Event IF conditions DO actions có nghæa là<br /> khi s¸ kiªn Event x£y ra trong mÎt i∑u kiªn conditions thì th¸c thi actions. Ta<br /> 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,<br /> nghæa là if Events x£y ra trong i∑u kiªn condition, then th¸c thi action. Các ˜u<br /> 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<br /> khác nhau nh˜ hª thËng CSDL, các ˘ng dˆng c£m ng˙ c£nh. ã có nhi∑u nghiên<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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ô<br /> 1<br /> <br /> 2<br /> <br /> TÍng quan v∑ lu™n án<br /> <br /> 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,<br /> 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<br /> 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≥<br /> 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 Î<br /> 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<br /> ∑ 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<br /> 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ô<br /> 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<br /> 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<br /> ∞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<br /> 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<br /> có rßt nhi∑u ˜u i∫m.<br /> 1.2 Mˆc tiêu<br /> 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ì<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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<br /> các mªnh ∑ c¶n ch˘ng minh ˜Òc sinh ra bi Event-B. Công cˆ Rodin ˜Òc s˚<br /> 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<br /> 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<br /> 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<br /> và ki∫m ch˘ng tính chßt an toàn và tính ho§t Îng cıa hª thËng.<br /> 1.3<br /> óng góp mÓi cıa lu™n án<br /> Các nghiên c˘u óng góp cıa lu™n án bao gÁm<br /> 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<br /> CSDL có thành ph¶n trigger s˚ dˆng Event-B. Ph˜Ïng pháp này giÓi thiªu các<br /> b˜Óc chi ti∏t ∫ chuy∫n Íi các khái niªm trong CSDL sang các k˛ hiªu Event-B.<br /> 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<br /> 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<br /> 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<br /> 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<br /> tri∫n. MÎt công cˆ hÈ trÒ chuy∫n Ëi bán t¸ Îng cÙng ˜Òc phát tri∫n.<br /> 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<br /> lu™t ECA và Event-B event ∫ ∑ xußt ph˜Ïng pháp mô hình hóa và ki∫m ch˘ng<br /> 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<br /> trong Event-B ∑ làm cho ph˜Ïng pháp ∑ xußt phù hÒp vÓi mô hình hóa t¯ng<br /> 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<br /> ki∫m ch˘ng t¸ Îng b¨ng s˚ dˆng công cˆ Rodin.<br /> <br /> Hình 1.1: Cßu trúc lu™n án<br /> <br /> 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<br /> 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<br /> 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<br /> 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<br /> 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<br /> gian ∫ mô hình hóa các hª thËng ˜Òc ‡nh thÌi.<br /> 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<br /> 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<br /> 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<br /> Îng.<br /> 1.4 Cßu trúc lu™n án<br /> 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<br /> 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ª<br /> 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ª<br /> 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<br /> 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<br /> 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<br /> 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.<br /> <br /> Ch˜Ïng 2. Ki∏n th˘c cÏ s<br /> 2.1 Temporal logic<br /> Propositional temporal logic (PTL) là s¸ m rÎng cıa logic mªnh ∑ trong ó mô<br /> 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<br /> 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<br /> 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<br /> 3<br /> <br />