Luận án Mô hình hóa và đặc tả hình thức giao diện thành phần chứa chất lượng dịch vụ và tính tương tranh

Nội dung tài liệu: Luận án Mô hình hóa và đặc tả hình thức giao diện thành phần chứa chất lượng dịch vụ và tính tương tranh

1. Mục lục 1 Giới thi»u 1 1.1 Đặt v§n đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 1.2 C¡c k¸t qu£ ch½nh cõa luªn ¡n . . . . . . . . . . . . . . . . . . . . .5 1.3 Bè cục cõa luªn ¡n . . . . . . . . . . . . . . . . . . . . . . . . . . .8 2 Ki¸n thùc n·n t£ng 10 2.1 Công ngh» ph¦n m·m dựa tr¶n thành ph¦n . . . . . . . . . . . . . 11 2.1.1 Giới thi»u . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.1.2 C¡c công ngh» x¥y dựng h» thèng ph¦n m·m dựa tr¶n thành ph¦n hi»n nay . . . . . . . . . . . . . . . . . . . . . . 13 2.1.3 Đảm b£o ch§t lượng cho c¡c h» thèng ph¦n m·m dựa tr¶n thành ph¦n . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.2 Ô-tô-mát thời gian . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.2.1 Giới thi»u . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.2.2 Ô-tô-mát thời gian . . . . . . . . . . . . . . . . . . . . . . . 21 2.2.3 Công cụ UPPAAL . . . . . . . . . . . . . . . . . . . . . . . 29 2.3 Lý thuy¸t V¸t và ùng dụng trong đặc t£ h» thèng tương tranh . . 36 2.3.1 Giới thi»u . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2.3.2 V¸t Mazurkiewicz . . . . . . . . . . . . . . . . . . . . . . . . 37 2.3.3 Ô-tô-mát đo¡n nhªn ngôn ngú V¸t . . . . . . . . . . . . . . 43 2.3.4 Logic tr¶n V¸t . . . . . . . . . . . . . . . . . . . . . . . . . . 46 2.4 K¸t luªn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 3 Lý thuy¸t V¸t thời gian 51 3.1 Giới thi»u . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 3.2 V¸t thời gian và ô-tô-mát kho£ng b§t đồng bë . . . . . . . . . . . 53 3.2.1 V¸t thời gian . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 3.2.2 Ô-tô-mát kho£ng b§t đồng bë . . . . . . . . . . . . . . . . . 57 3.3 Lôgic tr¶n V¸t thời gian . . . . . . . . . . . . . . . . . . . . . . . . 61 3.4 C¡c nghi¶n cùu li¶n quan . . . . . . . . . . . . . . . . . . . . . . . . 65 3.5 K¸t luªn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 i
2. 4 Mët mô h¼nh cho h» thèng tương tranh có ràng buëc thời gian dựa tr¶n c¡c kh¡i ni»m và kỹ thuªt rCOS 67 4.1 Giới thi»u . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.2 Ki¸n trúc thành ph¦n và c¡c giao thùc tương t¡c . . . . . . . . . . 69 4.3 V¸t thời gian và biºu di¹n cõa nó . . . . . . . . . . . . . . . . . . . 70 4.4 Mô h¼nh thành ph¦n . . . . . . . . . . . . . . . . . . . . . . . . . . 71 4.4.1 Thi¸t k¸ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 4.4.2 Giao di»n và hñp đồng . . . . . . . . . . . . . . . . . . . . . 73 4.4.3 Gh²p nèi c¡c hñp đồng . . . . . . . . . . . . . . . . . . . . . 75 4.4.4 Thành ph¦n . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.5 K¸t luªn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 5 Phương ph¡p đặc t£ c¡c thành ph¦n trong h» tương tranh có ràng buëc thời gian theo nguy¶n lý thi¸t k¸ dựa tr¶n giao di»n 83 5.1 Giới thi»u . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 5.2 Ô-tô-mát giao di»n tương tranh có ràng buëc thời gian . . . . . . 85 5.2.1 Định nghĩa . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 5.2.2 Kh£ n«ng gh²p nèi và T½ch song song c¡c TCIA . . . . . . 88 5.2.3 Làm mịn c¡c thành ph¦n . . . . . . . . . . . . . . . . . . . 92 5.3 C¡c nghi¶n cùu li¶n quan . . . . . . . . . . . . . . . . . . . . . . . . 94 5.4 K¸t luªn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 6 Mô h¼nh đặc t£ và kiºm chùng c¡c h» ph¥n t¡n có ràng buëc thời gian dựa tr¶n h» dịch chuyºn ph¥n t¡n 98 6.1 H» ph¥n t¡n có ràng buëc thời gian . . . . . . . . . . . . . . . . . . 99 6.2 Lôgic thời gian tr¶n c§u h¼nh Foata . . . . . . . . . . . . . . . . . . 103 6.3 Bài to¡n kiºm chùng . . . . . . . . . . . . . . . . . . . . . . . . . . 108 6.4 C¡c nghi¶n cùu li¶n quan . . . . . . . . . . . . . . . . . . . . . . . . 109 6.5 K¸t luªn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 7 K¸t luªn 112 7.1 C¡c k¸t qu£ đạt được . . . . . . . . . . . . . . . . . . . . . . . . . . 112 7.2 Hướng ph¡t triºn ti¸p theo . . . . . . . . . . . . . . . . . . . . . . . 114 ii
3. Danh s¡ch h¼nh v³ 1.1 C§u trúc luªn ¡n . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 2.1 Mô h¼nh ph¡t triºn CBSE . . . . . . . . . . . . . . . . . . . . . . . 12 2.2 Ki¸n trúc CBSE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3 Đồng hồ là mët hàm thời gian . . . . . . . . . . . . . . . . . . . . . 21 2.4 Mô h¼nh đi·u khiºn đèn không có thời gian . . . . . . . . . . . . . 22 2.5 Mô h¼nh đi·u khiºn đèn có thời gian . . . . . . . . . . . . . . . . . 22 2.6 Mô h¼nh h» thèng điều khiºn thanh ch­n tàu . . . . . . . . . . . . 29 2.7 Thuëc t½nh Safety và Real-time Liveness cõa bài to¡n mô h¼nh h» điều khiºn đóng mở thanh ch­n tàu . . . . . . . . . . . . . . . . . 30 2.8 M¤ng c¡c ô-tô-mát thời gian . . . . . . . . . . . . . . . . . . . . . . 31 2.9 Ô-tô-mát t½ch cõa hai ô-tô-mát trong H¼nh 2.8 . . . . . . . . . . . 32 2.10 V½ dụ mët m¤ng với c¡c vùng thời gian không lồi . . . . . . . . . . 33 2.11 Ki¸n trúc h» thèng cõa UPPAAL . . . . . . . . . . . . . . . . . . . 35 2.12 Đồ thị phụ thuëc cõa b£ng chú c¡i phụ thuëc . . . . . . . . . . . . 38 2.13 Mët đồ thị biºu di¹n cõa V¸t Mazurkiewicz . . . . . . . . . . . . . 41 2.14 Ánh x¤ wtot() cho tø abcba ....................... 42 2.15 Mët ô-tô-mát b§t đồng bë . . . . . . . . . . . . . . . . . . . . . . . 45 2.16 Ý nghĩa cõa Until . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 3.1 Sơ đồ thù tự bë phªn V¸t thời gian đưñc cho trong v½ dụ 3.1 . . . 55 3.2 Sơ đồ thù tự bë phªn cõa mët V¸t kho£ng được cho trong v½ dụ 3.2 57 3.3 Sơ đồ thù tự bë phªn cõa V¸t kho£ng (T;J) và và V¸t thời gian (T 0; θ) thỏa (T;J) ............................ 58 3.4 Mët ADA với hàm g¡n thời gian J trong v½ dụ 3.3 . . . . . . . . . 59 3.5 Ngú nghĩa cõa to¡n tû EXI ...................... 63 3.6 Ngú nghĩa cõa to¡n tû UI ....................... 63 4.1 Ki¸n trúc h» thèng . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 4.2 Thời gian và thù tự cõa Mcode(m) và ph²p chi¸u cõa nó tr¶n c¡c phương thùc cõa B . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 5.1 Mët TCIA P với JP (a) = [1; 2];JP (b) = [2; 3];JP (c) = [1; 3] (i) và đồ thị chuyºn tr¤ng th¡i tương ùng (ii) . . . . . . . . . . . . . . . 87 iii
4. 5.2 TCIA Q với JQ(b) = [2; 3];JQ(c) = [1; 3];JQ(d) = [2; 4] (i) và đồ thị chuyºn tr¤ng th¡i tương ùng (ii) là tương th½ch với TCIA P trong V½ dụ 5.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 5.3 K¸t qu£ ph²p t½ch song song giúa P và Q trong H¼nh 5.1 và 5.2 . 90 6.1 H» ph¥n t¡n có y¸u tè thời gian và c¡c thực thi đồng bë và b§t đồng bë cõa nó . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 6.2 Mët V¸t thời gian . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 6.3 C§u h¼nh Foata cõa mët V¸t thời gian trong H¼nh 6.2 . . . . . . . 104 6.4 Đồ thị c§u h¼nh Foata cõa V¸t thời gian được ch¿ ra trong H¼nh 6.2105 iv
5. Danh s¡ch b£ng 2.1 B£ng so s¡nh giúa c¡c công ngh» . . . . . . . . . . . . . . . . . . . 17 2.2 B£ng chuyºn cõa ô-tô-mát b§t đồng bë cõa H¼nh 2.15 . . . . . . . 45 5.1 B£ng chuyºn cõa TCIA P trong v½ dụ 5.1 . . . . . . . . . . . . . . 87 5.2 B£ng chuyºn cõa TCIA Q trong v½ dụ 5.2 . . . . . . . . . . . . . . 89 v
6. B£ng c¡c tø vi¸t t­t Tø vi¸t t­t Tø gèc Gi£i nghĩa-T¤m dịch AA Asynchronous Automata Ô-tô-mát b§t đồng bë ADA Asynchronous Duration Au- Ô-tô-mát kho£ng b§t tomata đồng bë CBSE Component-based Software Công ngh» ph¦n m·m dựa Enginnering tr¶n thành ph¦n CBSD Component-based Software Ph¡t triºn ph¦n m·m dựa Development tr¶n thành ph¦n DTS Distributed Transition Sys- H» dịch chuyºn ph¥n t¡n tems DDTS Duration Distributed Transi- H» dịch chuyºn ph¥n t¡n tion Systems kho£ng TCIA Timed Concurrent Interface Ô-tô-mát giao di»n tương Automata tranh thời gian UTP Unifying Theories of Program- Lý thuy¸t hñp nh§t v· lªp ming tr¼nh (t¤m dịch) TA Timed Automata Ô-tô-mát thời gian LTL Linear Temporal Logic Logic thời gian tuy¸n t½nh TLTL Timed Linear Temporal Logic Logic thời gian tuy¸n t½nh có ràng buëc thời gian rCOS Refinement of Component and Làm mịn thành ph¦n và Object Systems c¡c h» thèng đối tượng COM Component Object Model Mô h¼nh đối tượng thành ph¦n DCOM Distributed Component Ob- Mô h¼nh đối tượng thành ject Model ph¦n ph¦n t¡n CORBA Common Object Request Bro- ker Architecture ORB Object Request Broker OMG Object Management Group Tªp đoàn qu£n lý đối tượng COTS Component Off The Shelf Thành ph¦n thương m¤i có s®n TW Timed Word Tø thời gian vi
7. Tø vi¸t t­t Tø gèc Gi£i nghĩa-T¤m dịch RTS Real-time systems C¡c h» thời gian thực CCS Calculus of Communicating T½nh to¡n c¡c h» thèng Systems giao ti¸p CTL Computational Tree Logic Logic c¥y t½nh to¡n TCTL Timed Computational Tree Logic c¥y t½nh to¡n có Logic thời gian P roc Process Ký hi»u ti¸n tr¼nh wtot word to trace Ký hi»u hàm chuyºn tø "tø" sang "V¸t" ttow trace to word Ký hi»u hàm chuyºn tø "V¸t" sang "tø" BA B¨uchi Automata Ô-tô-mát Bu-khi conf Configuration Ký hi»u c§u h¼nh CG Configuration Graph Ký hi»u đồ thị c§u h¼nh WCET Worst-case Execution Time Thời gian thực thi y¸u nh§t dtot duration to timed Ký hi»u hàm chuyºn thời kho£ng sang thời điểm tT rL timed Trace Language Ngôn ngú V¸t thời gian intv inteval Ký hi»u kho£ng thời gian pref prefix Ký hi»u ti·n tè P roj Project Ký hi»u ph²p chi¸u dur duration Ký hi»u kho£ng Ctr Contract Hñp đồng Comp Component Thành ph¦n Behav Behavior Hành vi ActComp Active Component Thành ph¦n chõ động SysCtr System Contract Hñp đồng h» thèng vii
8. Lời cam đoan Tôi xin cam đoan đây là công tr¼nh nghi¶n cùu do tôi thực hi»n dưới sự hướng d¨n cõa TS. Đặng V«n Hưng và PGS.TS. Nguy¹n Vi»t Hà t¤i bë môn Công ngh» Ph¦n m·m, Khoa Công ngh» Thông tin, Trường Đại học Công ngh», Đại học Quèc gia Hà Nëi. C¡c sè li»u và k¸t qu£ tr¼nh bày trong luªn ¡n là trung thực, chưa được công bè bởi b§t kỳ t¡c gi£ nào hay ở b§t kỳ công tr¼nh nào kh¡c. T¡c gi£ viii
9. Lời c£m ơn Luªn ¡n này được thực hi»n t¤i Trường Đại học Công ngh», Đại học Quèc gia Hà Nëi dưới sự hướng d¨n khoa học cõa TS Đặng V«n Hưng và PGS.TS. Nguy¹n Vi»t Hà. Nghi¶n cùu sinh xin bày tỏ láng bi¸t ơn s¥u s­c tới c¡c Th¦y v· định hướng khoa học, sự quan t¥m, hướng d¨n và c¡c ch¿ b£o kịp thời cho c¡c hướng nghi¶n cùu, t¤o điều ki»n thuªn lñi trong suèt qu¡ tr¼nh nghi¶n cùu t¤i trường. Nghi¶n cùu sinh cũng xin c£m ơn tới c¡c thày cô trong Bë môn Công ngh» Ph¦n m·m. Trong qu¡ tr¼nh thực hi»n luªn ¡n, nghi¶n cùu sinh đã nhªn được sự giúp đỡ nhi»t t¼nh và sự động vi¶n kịp thời cõa c¡c th¦y cô, c¡c nhà khoa học. Đ¥y là nguồn động lực lớn để tôi có thº hoàn thành luªn ¡n. Nghi¶n cùu sinh xin tr¥n trọng c£m ơn L¢nh đạo Trường Đại học Công ngh», Đại học Quèc Gia Hà Nëi đã t¤o nhúng điều ki»n tèt nh§t để nghi¶n cùu sinh có được môi trường nghi¶n cùu tèt nh§t và hoàn thành chương tr¼nh nghi¶n cùu cõa m¼nh. Xin ch¥n thành c¡m ơn Khoa Công ngh» Thông tin, Pháng Đào t¤o và đào t¤o sau đại học và c¡c nhà khoa học thuëc trường Đại học Công ngh» cũng như c¡c nghi¶n cùu sinh kh¡c v· sự hé trñ tr¶n phương di»n hành ch½nh, hñp t¡c có hi»u qu£ trong suèt qu¡ tr¼nh nghi¶n cùu khoa học cõa m¼nh. Nghi¶n cùu sinh xin gûi lời c£m ơn tới Ban L¢nh đạo Trường Đại học D¥n lªp H£i Pháng, Khoa Công ngh» Thông tin và c¡c b¤n đồng nghi»p v¼ đ¢ t¤o nhi·u điều ki»n thuªn lñi hé trñ cho nghi¶n cùu sinh có thời gian và toàn t¥m thực hi»n triºn khai đề tài nghi¶n cùu cõa luªn ¡n. Nghi¶n cùu sinh cũng xin tr¥n trọng c£m ơn c¡c nhà khoa học, t¡c gi£ c¡c công tr¼nh công bè đ¢ tr½ch d¨n trong luªn ¡n v¼ đã cung c§p nguồn tư li»u quý b¡u, nhúng ki¸n thùc li¶n quan trong qu¡ tr¼nh nghi¶n cùu hoàn thành luªn ¡n. Cuèi cùng là sự bi¸t ơn tới Bè Mẹ, vñ con, c¡c anh chị em trong gia đình và nhúng người b¤n th¥n thi¸t đ¢ li¶n tục động vi¶n để duy tr¼ nghị lực, sự c£m thông, chia s´ v· thời gian, sùc khỏe và c¡c kh½a c¤nh cõa cuëc sèng trong c£ qu¡ tr¼nh hoàn thành luªn ¡n. ix
10. Tóm t­t Ch§t lượng dịch vụ cõa mët h» thèng bao gồm thời gian ti¸n hành, tài nguy¶n ti¶u thụ và độ tin cªy cõa dịch vụ, trong đó th¼ ch§t lượng dịch vụ v· thời gian đang được quan t¥m nhi·u, thº hi»n r¬ng thời gian cung ùng dịch vụ tèt hơn. Ràng buëc thời gian trong c¡c h» thèng thường được ph¥n chia thành hai lo¤i là ràng buëc thời gian cùng (hard) và m·m (soft). Luªn ¡n quan t¥m tới c¡c ràng buëc thời gian cùng. Để ch§t lượng dịch vụ tèt, c¡c phương thùc trong h» thèng c¦n được ti¸n hành song song (t«ng tèc độ đáp ùng) n¸u có thº và ph£i có ràng buëc thời gian rã ràng. Ràng buëc thời gian thº hi»n thời gian tèi thiºu và tèi đa mà phương thùc c¦n để có thº cung c§p dịch vụ, tùc là không đưñc gọi phương thùc qu¡ “dày”1, n¸u không có thº s³ g¥y ra t¼nh tr¤ng dịch vụ không đáp ùng được. Luªn ¡n quan t¥m tới phương ph¡p đặc t£ h» thèng có chùa ch§t lượng dịch vụ v· thời gian. Đối tượng nghi¶n cùu cõa luªn ¡n là c¡c h» thèng ph¦n m·m dựa tr¶n thành ph¦n có t½nh tương tranh và có ràng buëc v· thời gian. T½nh tương tranh là mët thuëc t½nh cõa h» thèng trong đó mët sè dịch vụ cõa h» thèng được cho ph²p truy cªp mët c¡ch song song. Ràng buëc v· thời gian trong luªn ¡n là c¡c y¶u c¦u v· thời gian thực thi cõa c¡c hành động trong h» thèng, méi hành động s³ được g­n với mët kho£ng thời gian cho vi»c thực thi cõa nó. Mục đích cõa luªn ¡n là ph¡t triºn mët phương ph¡p h¼nh thùc để đặc t£ và kiºm chùng c¡c giao di»n cõa c¡c thành ph¦n ph¦n m·m có t½nh tương tranh và ràng buëc v· thời gian. Sau đó, luªn ¡n ¡p dụng phương ph¡p được đề xu§t vào vi»c đặc t£, ph¥n t½ch và kiºm chùng c¡c mô h¼nh kh¡c nhau cõa c¡c h» thèng ph¦n m·m dựa tr¶n thành ph¦n. C¡c k¸t qu£ cõa luªn ¡n đạt được như sau. Luªn ¡n đề xu§t lý thuy¸t V¸t thời gian để hé trñ đặc t£ c¡c ràng buëc v· thời gian tr¶n c¡c h» thèng tương tranh thời gian thực. V¸t thời gian là mët sự mở rëng v· thời gian cõa V¸t Mazurkiewicz b¬ng vi»c bê sung vào V¸t Mazurkiewicz mët hàm g¡n nh¢n thời gian. Với vi»c mở rëng này, V¸t thời gian có thº d¹ dàng đặc t£ c¡c hành vi cõa h» thèng tương tranh có ràng buëc thời gian. Trong lý thuy¸t này, luªn ¡n cán đề xu§t kh¡i ni»m V¸t kho£ng. V¸t kho£ng là c¡c V¸t Mazurkiewicz mà méi 1Mªt độ cao tr¶n mët đơn vị thời gian x