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, luận án tập trung vào sử dụng Event-B để mô hình hóa các hệ thống hướng sự hiện đặc trưng như các hệ thống cơ sở dữ liệu, các hệ thống cảm ngữ cảnh; đồng thời, đề 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. . | Ñ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Ë: 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 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 .
