فهرست مطالب
عنوان صفحه
فصل اول: مقدمه 1
1.1 . بيان مسئله و ضرورت تحقيق 1
1.2 . دامنه تحقيق 7
1.3 . پيشينه تحقيق 7
1.4 . اهداف تحقيق 8
1.5 . سوالات تحقيق 8
1.6 . مراحل و روش تحقيق 9
1.7 . دستاوردهای تحقيق 10
1.8 . نگاهی کلی بر پایان نامه 10
فصل دوم: معرفی و بررسی ابزار فرمال برای مدل سازی سيستم ها 12
2.1 . Abstract State Machine (ASM) 14
2.2 . LOTOS 17
2.2.1 . مقدمه ای بر جبر پروسه ها 18
2.3 . VDM-SL 22
2.4 . شبکه های پتری 23
2.4.1 . خصوصيات رفتاری 25
2.4.1.1 . Reachability 26
2.4.1.2 . Boundedness 26
2.4.1.3 . Liveness 26
2.4.1.4 . Reversibility 28
2.4.1.5 . Coverability 28
IX
2.4.2 . زیر مجموعه های شبکه های پتری 29
2.4.2.1 . State Machine (SM) 30
2.4.2.2 . Marked Graph (MG) 30
2.4.2.3 . Free-choice net (FC) 31
2.4.2.4 . Extended Free-choice net (EFC) 31
2.4.2.5 . Asymmetric choice net (AC) 31
2.4.3 . قضایا و فرضيات 32
2.5 . مقایسه و جمع بندی 35
فصل سوم: بررسی معماری دیتا سنترها 38
3.1 . Microsoft Hyper-V 39
3.1.1 . بررسی اجزاء معماری Hyper-V 42
3.1.1.1 . APIC 43
3.1.1.2 . Child Partition 43
3.1.1.3 . Hypercall 43
3.1.1.4 . Hypervisor 43
3.1.1.5 . IC 43
3.1.1.6 . I/O stack 44
3.1.1.7 . Root Partition 44
3.1.1.8 . VID 44
3.1.1.9 . VMBus 44
3.1.1.10 . VMMS 44
3.1.1.11 . VMWP 44
3.1.1.12 . VSC 45
3.1.1.13 . VSP 45
3.1.1.14 . WinHv 45
3.1.1.15 . WMI 45
3.1.2 . نقاط ضعف 46
3.2 . Xen 46
3.2.1 . بررسی اجزاء معماری Xen 48
3.2.1.1 . Xen Hypervisor 48
3.2.1.2 . Domain 0 48
3.2.1.3 . Domain U 49
3.2.1.4 . Xenstored 50
3.2.2 . ارتباطات مابين دامنه صفر و دامنه های U 50
X
3.3 . VMware ESXi 50
3.3.1 . بررسی اجزاء معماری VMware ESX 52
3.3.1.1 . VMkernel 52
3.3.1.2 . File System 52
3.3.1.3 . CIM 53
3.4 . طراحی یک معماری برای دیتا سنتر 54
3.5 . مختصری درباره vSphere 56
3.5.1 . سرویس های زیر ساختی vSphere 58
3.5.2 . سرویس های کاربردی vSphere 59
3.5.2.1 . سرور VMware vCenter 59
3.5.2.2 . Client ها 59
3.5.2.3 . ESX 59
3.5.2.4 . vCenter Server 59
3.5.2.5 . VMFS 59
3.5.2.6 . SMP 60
3.5.2.7 . VCMS 60
3.5.2.8 . VI Client 60
3.5.2.9 . VMware VMotion 60
3.5.2.10 . Storage VMotion 60
3.5.2.11 . VMware HA 61
3.5.2.12 . DRS 62
3.5.2.13 . Consolidated Backup 63
3.5.2.14 . vSphere SDK 63
3.5.2.15 . Fault Tolerance 64
3.5.3 . سرویس های توزیع شده در vSphare 64
3.5.4 . معماری شبکه 64
3.5.5 . معماری محل ذخيره سازی داده ها 66
3.5.6 . معماری سرور مدیریت VirtualCenter 69
3.5.6.1 . User Access Control 70
3.5.6.2 . Core Service 71
3.6 . جمع بندی 71
فصل چهارم: ارائه مدل فرمال برای دیتا سنتر و تحليل آن 72
4.1 . تشریح دیتا سنتر نمونه 73
4.2 . ارائه مدلی از رفتار کلی دیتا سنتر 77
XI
4.2.1 . ارزیابی و تحليل مدل فرمال 87
4.2.1.1 . Liveness 87
4.2.1.2 . Safeness
87
4.2.1.3 . Reversibility 89
4.2.2 . بررسی لایه های پایينتر مدل فرمال 90
4.3 . بررسی نحوه کار سرویس HA 91
4.3.1 . شرح سرویس VMware HA 91
4.3.2 . ارائه مدل فرمال از نحوه کار سرویس HA 95
4.3.3 . تحليل و ارزیابی مدل 98
4.3.3.1 . Liveness 99
4.3.3.2 . Safeness
101
4.3.3.3 . Reversibility 102
4.4 . بررسی نحوه کار سرویس Fault Tolerance 106
4.4.1 . تشریح ساختار سرویس Fault Tolerance 106
4.4.2 . ارائه مدل فرمال از نحوه کار سرویس Fault Tolerance 110
4.4.3 . تحليل و ارزیابی مدل 111
4.4.3.1 . Liveness 112
4.4.3.2 . Safeness
113
4.4.3.3 . Reversibility 113
4.5 . بررسی نحوه کار سرویس VMotion 114
4.5.1 . تشریح ساختار سرویس VMotion 114
4.5.2 . ارائه مدل فرمال از نحوه کار سرویس VMotion 118
4.5.3 . تحليل و ارزیابی مدل 119
4.5.3.1 . Liveness 120
4.5.3.2 . Safeness
121
4.5.3.3 . Reversibility 122
4.6 . بررسی ساختار داخلی ESX hypervisor 124
4.6.1 . تشریح ساختار ESX 124
XII
4.6.2 ارائه یک مدل فرمال از نحوه کار . ESX 125
4.6.3 . بررسی و تحليل مدل 129
4.6.3.1 . Liveness
129
4.6.3.2 . Safeness
131
4.6.3.3 . Reversibility 132
4.7 . تشریح ساختار سيستم ذخيره سازی در ESX 133
4.7.1 . تشریح ساختار سيستم ذخيره سازی 133
4.7.2 . ارائه یک مدل فرمال از نحوه کار سيستم ذخيره سازی در ESX 138
4.7.3 . بررسی و تحليل مدل 144
4.7.3.1 . Liveness 144
4.7.3.2 . Safeness
145
4.7.3.3 . Reversibility 146
4.8 . معماری ساختار شبکه در ESX 148
4.8.1 . تشریح ساختار شبکه 148
4.8.2 . ارائه مدل فرمال برای ساختار شبکه در ESX 155
4.8.3 . بررسی و تحليل مدل 161
4.8.3.1 . Reversibility 161
4.8.3.2 . Liveness 163
4.8.3.3 . Safeness
165
4.9 . معماری سوئيچ مجازی در ساختار شبکه 165
4.9.1 . تحليل ساختار سوئيچ مجازی 165
4.9.2 . ارائه یک مدل فرمال برای سوئيچ مجازی 169
4.9.3 . بررسی و تحليل مدل 172
4.9.3.1 . Liveness 172
4.9.3.2 . Safeness
173
4.9.3.3 . Reversibility 174
4.10 . جمع بندی 175
XIII
فصل پنجم: نتيجه گيری و پيشنهادات 176
مراجع 180
پيوست: مجموعه کامل مدل های پتری طراحی شده در پایان نامه 186
چکيده به زبان انگليسی 195
فهرست جدول ها
عنوان و شماره صفحه
جدول 2.1 . خلاصه مقایسه ابزار توصيف فرمال 36
جدول 3.1 . سيستم های عامل قابل پشتيبانی توسط Hyper-V R2 41
جدول 3.2 . سيستم های عامل قابل پشتيبانی توسط Xen نسخه 3 . 47
جدول 4.1 . گزارهای فعال در وضعيت های 0M الی 15M از مدل پتری 4.30 164
جدول 5.1 . خلاصه نتایج به دست آمده از تحليل رفتار زیر سيستم ها و سرویس های VMware ESX 177
XIV
فهرست شکل ها
عنوان صفحه
شکل 1.1 . نحوه قرارگيری لایه های نرم افزاری بر روی سرور 4
شکل 1.2 . شمای کلی دیتا سنتر با معماری مجازی 5
شکل 2.1 . مثال هایی از زبان های فرمال و تقسيم بندی آنها ]10[ 13
شکل 2.2 . روال طراحی یک سيستم نمونه به کمک زبان های فرمال ]10[ 14
شکل 2.3 . نقطه gate در جبر پروسه ها ]4[ 18
شکل 2.4 . مدل توليد کننده- مصرف کننده به کمک LOTOS ]17[ 19
شکل 2.5 . مثالی از مدل سازی یک پروتکل به کمک شبکه های پتری ]23[ 25
شکل 2.6 . نمونه ای از شبکه پتری non-Live ]23[ 27
شکل 2.7 . نشانه گزاری برای: a( مجموعه موقعيت های ورودی و خروجی برای t و b( مجموعه گزارهای ورودی و
خروجی برای p ]23[ 30
شکل 2.8 . مثال هایی از زیر مجموعه های شبکه های پتری ]23[ 32
شکل 2.9 . یک شبکه پتری و گراف نشانه دار مربوط به آن ]23[ 33
شکل 3.1 . معماری سطح بالای Hyper-V ]40[ 42
شکل 3.2 . شمایی از معماری Xen ]51[ 47
شکل 3.3 . نحوه سرویس دهی به ماشين ميزبان توسط Qemu-DM ]51[ 49
شکل 3.4 . شمایی از معماری VMware ESXi ]3[ 52
شکل 3.5 . ساختار شماتيک مدیریت CIM ]3[ 54
XV
شکل 3.6 . مثالی از مفاهيم ميزبان، کلاستر و مخزن منابع ]60[ 58
شکل 3.7 . طرز کار سرویس HA ]61[ 62
شکل 3.8 . شمایی از معماری شبکه در محيط مجازی ]60[ 65
شکل 3.9 . شمایی از معماری ذخيره سازی ]60[ 66
شکل 3.10 . طرز کار RDM ]60[ 68
شکل 3.11 . شمایی از ساختار سرور مدیریت VirtualCenter ]60[ 70
شکل 4.1 . زیر ساخت دیتا سنتر مجازی ]63[ 73
شکل 4.2 . یک الگوی نمونه برای زیر ساخت دیتا فيزیکی سنتر ]60[ 75
شکل 4.3 . ساختار شماتيک دیتا سنتر نمونه 76
شکل 4.4 . مدل پتری طراحی شده برای دیتا سنتر نمونه 78
شکل 4.5 . گراف پوشا برای مدل پتری شکل 4.4 88
شکل 4.6 . نتيجه تحليل فضای حالت به وسيله نرم افزار PIPE 89
شکل 4.7 . مدل پتری نحوه کار سرویس HA 96
شکل 4.8 . عضویت شبکه 4.7 در زیرکلاس های شبکه های پتری 100
شکل 4.9 . گراف پوشای مدل 4.7 101
شکل 4.10 . نتيجه تحليل فضای حالت بر روی مدل 102
شکل 4.11 . نحوه توزیع توکن در وضعيت S8 103
شکل 4.12 . شبيه سازی شبکه پتری شکل 4.7 104
شکل 4.13 . چندین نمونه از شبيه سازی اجرای شبکه پتری 105
شکل 4.14 . مدل پتری نحوه کار سرویس Fault Tolerance 110
شکل 4.15 . نحوه توزیع توکن ها در 3M و 4M 112
شکل 4.16 . گراف پوشای مدل پتری شکل 4.14 114
شکل 4.17 مدل پتری نحوه کار سرویس VMotion 118
شکل 4.18 . گراف نشانه دار (G,