در این تحقیق با استفاده از زبان فرمال شبکه های پتری، از بخش ها و جنبه های مختلف لایه مجازی سازی در دیتا سنترها، مدل های فرمال متعددی تهیه شده است. سپس به کمک ابزار ریاضی، رفتار این مکانیزم ها برای تعیین سطح خوش رفتاری سیستم بررسی شده است. برای نیل به این هدف، در ابتدا ابزار مدل سازی فرمال اعم از جبری و مبتنی بر مدل بررسی و مقایسه شده است. سپس با تشریح تکنولوژی مجازی سازی در سیستم های کامپیوتری، یک دیتا سنتر نمونه کوچک مطابق استانداردهای دیتا سنترها طراحی شده و سپس در لایه های مختلف توسط شبکه های پتری مدل گردیده است. این مدل سازی از سطح کاملا انتزاعی[1] (لایه 1) برای کل دیتا سنتر شروع و با طراحی مدل برای زیر سیستم ها و مکانیزم هایی مانند ساختار شبکه، ذخیره سازی و نیز سرویس های سطح بالا مانند HA و Fault Tolerance پایان می یابد. در پایان هر بخش، پس از ارائه و تشریح مدل، به تحلیل و ارزیابی آن و بررسی خصوصیات رفتاری سیستم از روی مدل فرمال آن پرداخته شده است. در نهایت، نتیجه گیری از میزان خوش رفتاری بخش های مختلف این لایه در دیتا سنتر ارائه شده است. فهرست مطالبفصل اول: مقدمه 1فصل دوم: معرفی و بررسی ابزار فرمال برای مدل سازی سیستم ها 122.1. Abstract State Machine (ASM) 142.2. LOTOS 172.2.1.مقدمه ای بر جبر پروسه ها 182.3. VDM-SL 222.4. شبکه های پتری 232.4.1.خصوصیات رفتاری 252.4.1.1. Reachability 262.4.1.2. Boundedness 262.4.1.3. Liveness 262.4.1.4. Reversibility 282.4.1.5. Coverability 282.4.2.زیر مجموعه های شبکه های پتری 292.4.2.1. State Machine (SM) 302.4.2.2. Marked Graph (MG) 302.4.2.3. Free-choice net (FC) 312.4.2.4. Extended Free-choice net (EFC) 312.4.2.5. Asymmetric choice net (AC) 312.4.3.قضایا و فرضیات 322.5. مقایسه و جمع بندی 35فصل سوم: بررسی معماری دیتا سنترها 383.1. Microsoft Hyper-V 393.1.1.بررسی اجزاء معماری Hyper-V 423.1.1.1. APIC 433.1.1.2. Child Partition 433.1.1.3. Hypercall 433.1.1.4. Hypervisor 433.1.1.5. IC 433.1.1.6. I/O stack 443.1.1.7. Root Partition 443.1.1.8. VID 443.1.1.9. VMBus 443.1.1.10. VMMS 443.1.1.11. VMWP 443.1.1.12. VSC 453.1.1.13. VSP 453.1.1.14. WinHv 453.1.1.15. WMI 453.1.2.نقاط ضعف 463.2. Xen 463.2.1.بررسی اجزاء معماری Xen 483.2.1.1. Xen Hypervisor 483.2.1.2. Domain 0 483.2.1.3. Domain U 493.2.1.4. Xenstored 503.2.2.ارتباطات مابین دامنه صفر و دامنه های U 503.3. VMware ESXi 503.3.1.بررسی اجزاء معماری VMware ESX 523.3.1.1. VMkernel 523.3.1.2. File System 523.3.1.3. CIM 533.4. طراحی یک معماری برای دیتا سنتر 543.5. مختصری درباره vSphere 563.5.1.سرویس های زیر ساختی vSphere 583.5.2.سرویس های کاربردی vSphere 593.5.2.1. سرور VMware vCenter 593.5.2.2. Client ها 593.5.2.3. ESX 593.5.2.4. vCenter Server 593.5.2.5. VMFS 593.5.2.6. SMP 603.5.2.7. VCMS 603.5.2.8. VI Client 603.5.2.9. VMware VMotion 603.5.2.10. Storage VMotion 603.5.2.11. VMware HA 613.5.2.12. DRS 623.5.2.13. Consolidated Backup 633.5.2.14. vSphere SDK 633.5.2.15. Fault Tolerance 643.5.3.سرویس های توزیع شده در vSphare 643.5.4.معماری شبکه 643.5.5.معماری محل ذخیره سازی داده ها 663.5.6.معماری سرور مدیریت VirtualCenter 693.5.6.1. User Access Control 703.5.6.2. Core Service 713.6. جمع بندی 71فصل چهارم: ارائه مدل فرمال برای دیتا سنتر و تحلیل آن 724.1. تشریح دیتا سنتر نمونه 734.2. ارائه مدلی از رفتار کلی دیتا سنتر 774.2.1.ارزیابی و تحلیل مدل فرمال 874.2.1.1. Liveness 874.2.1.2. Safeness 874.2.1.3. Reversibility 894.2.2.بررسی لایه های پایینتر مدل فرمال 904.3. بررسی نحوه کار سرویس HA 914.3.1.شرح سرویس VMware HA 914.3.2.ارائه مدل فرمال از نحوه کار سرویس HA 954.3.3.تحلیل و ارزیابی مدل 984.3.3.1. Liveness 994.3.3.2. Safeness 1014.3.3.3. Reversibility 1024.4. بررسی نحوه کار سرویس Fault Tolerance 1064.4.1.تشریح ساختار سرویس Fault Tolerance 1064.4.2.ارائه مدل فرمال از نحوه کار سرویس Fault Tolerance 1104.4.3.تحلیل و ارزیابی مدل 1114.4.3.1. Liveness 1124.4.3.2. Safeness 1134.4.3.3. Reversibility 1134.5. بررسی نحوه کار سرویس VMotion 1144.5.1.تشریح ساختار سرویس VMotion 1144.5.2.ارائه مدل فرمال از نحوه کار سرویس VMotion 1184.5.3.تحلیل و ارزیابی مدل 1194.5.3.1. Liveness 1204.5.3.2. Safeness 1214.5.3.3. Reversibility 1224.6. بررسی ساختار داخلی ESX hypervisor 1244.6.1.تشریح ساختار ESX 1244.6.2.ارائه یک مدل فرمال از نحوه کار ESX 1254.6.3.بررسی و تحلیل مدل 1294.6.3.1. Liveness 1294.6.3.2. Safeness 1314.6.3.3. Reversibility 1324.7. تشریح ساختار سیستم ذخیره سازی در ESX 1334.7.1.تشریح ساختار سیستم ذخیره سازی 1334.7.2.ارائه یک مدل فرمال از نحوه کار سیستم ذخیره سازی در ESX 1384.7.3.بررسی و تحلیل مدل 1444.7.3.1. Liveness 1444.7.3.2. Safeness 1454.7.3.3. Reversibility 1464.8. معماری ساختار شبکه در ESX 1484.8.1.تشریح ساختار شبکه 1484.8.2.ارائه مدل فرمال برای ساختار شبکه در ESX 1554.8.3.بررسی و تحلیل مدل 1614.8.3.1. Reversibility 1614.8.3.2. Liveness 1634.8.3.3. Safeness 1654.9. معماری سوئیچ مجازی در ساختار شبکه 1654.9.1.تحلیل ساختار سوئیچ مجازی 1654.9.2.ارائه یک مدل فرمال برای سوئیچ مجازی 1694.9.3.بررسی و تحلیل مدل 1724.9.3.1. Liveness 1724.9.3.2. Safeness 1734.9.3.3. Reversibility 1744.10. جمع بندی 175فصل پنجم: نتیجه گیری و پیشنهادات 176مراجع 180پیوست: مجموعه کامل مدل های پتری طراحی شده در پایان نامه 186چکیده به زبان انگلیسی 195 فهرست جدول ها عنوان و شماره صفحه جدول 2.1. خلاصه مقایسه ابزار توصیف فرمال 36جدول 3.1. سیستم های عامل قابل پشتیبانی توسط Hyper-V R2 41جدول 3.2. سیستم های عامل قابل پشتیبانی توسط Xen نسخه 3. 47جدول 4.1. گزارهای فعال در وضعیت های M0 الی M15 از مدل پتری 4.30 164جدول 5.1. خلاصه نتایج به دست آمده از تحلیل رفتار زیر سیستم ها و سرویس های VMware ESX177 فهرست شکل ها عنوان صفحه شکل 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شکل 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. نحوه توزیع توکن ها در M3 و M4 112شکل 4.16. گراف پوشای مدل پتری شکل 4.14 114شکل 4.17 مدل پتری نحوه کار سرویس VMotion 118شکل 4.18. گراف نشانه دار (G, ) مربوط به مدل 4.17 120شکل 4.19. گراف پوشای مدل 4.17 123شکل 4.20. مدل پتری طرز کار ESX 125شکل 4.21. گراف جهت دار معادل شبکه پتری 4.20 130شکل 4.22. گراف پوشای کدل پتری 4.20 132شکل 4.23. نمای شماتیک مدل چند لایه ای سیستم ذخیره سازی در ESX]63[ 134شکل 4.24. مدل پتری ارائه شده از نحوه کار سیستم ذخیره سازی در ESX 139شکل 4.25. گراف جهت دار متناظر با مدل پتری 4.24 144شکل 4.26. گراف پوشای شبکه پتری 4.24 146شکل 4.27. نرم افزار تحلیلگر گراف، در حال اجرای الگوریتم اول عمق 147شکل 4.28. نحوه ارتباط کارت شبکه مجازی و سوئیچ مجازی ]62[ 149شکل 4.29. شمای کلی از ساختار شبکه در سرور ESX 153شکل 4.30. مدل پتری تهیه شده از ساختار شبکه در ESX 156شکل 4.31. گراف پوشای مدل پتری شکل 4.30 162شکل 4.32. جستجوی اول عمق گراف شکل 4.31 163شکل 4.33 مدل فرمال از نحوه کار سوئیچ مجازی 170شکل 4.34. گراف جهت دار متناظر با مدل پتری 4.33 173شکل 4.35. گراف پوشای مدل پتری 4.33 174 فصل اول: مقدمه 1.1. بيان مسئله و ضرورت تحقيق نیاز بشر به پردازش و ذخیره سازی اطلاعات در دهه های گذشته همواره رشد صعودی و شتابدار داشته است. به گونه ای که حرکت از سیستم های توزیع شده بر روی سوپرکامپیوترهای گران قیمت به شبکه های بسیار پر قدرت و ارزان در مدت نسبتا کوتاهی صورت گرفته است. همچنین نیاز به مدیریت اطلاعات، پردازش، گردش کار و دیگر ابزار مدیریتی همواره رشد فزاینده داشته است. به طبع این نیاز، ساختار سیستم های کامپیوتری در سطوح فنی و مدیریتی نیز رشد کرده و پیچیده تر شده است.به منظور جوابگویی به این حجم فزاینده درخواست ها و نیاز بازار به منابع پردازش و ذخیره سازی اطلاعات و نیز به منظور ارائه سرویس های مورد نیاز با کیفیت مناسب و قابل رقابت، یکی از بهترین راه های پیشنهاد شده، متمرکز نمودن این منابع و مدیریت صحیح آنها است. به این منظور و برای به حداکثر رساندن کیفیت خدمات و حداقل نمودن هزینه ها یکی از رایج ترین راهکارهای موجود راه اندازی مراکز داده یا دیتا سنتر ها می باشد. در این طرح با آماده سازی زیر ساخت های فیزیکی، امنیتی، شبکه ای، سخت افزاری و نرم افزاری، مجموعه ای از سرورهای قدرتمند برای ارائه سرویس های مورد نیاز مشتریان در نظر گرفته می شود. این سرورها با خطوط بسیار پر سرعت بر حسب نیاز به اینترنت یا شبکه های سازمانی متصل می گردند و با نصب سیستم های عامل و نرم افزارها و سرویس های مورد نیاز به کاربران خدمات لازم را ارائه می نمایند. با وجود چنین مراکزی دیگر سازمان ها و مراکز تجاری، صنعتی، دانشگاهی و غیره نیازی به راه اندازی مراکز سرویس دهی محلی[2] و نیز متحمل شدن هزینه های نگهداری، به روز رسانی و استخدام متخصصین نخواهند داشت. در ادامه به بررسی اجمالی دیتا سنترها خواهیم پرداخت تا بتوانیم طرح پیشنهادی را تشریح نمائیم.تعریف دیتا سنتر: مجموعه ای از سیستمهای پشتیبانی (از جمله زیر ساخت سخت افزاری passive، زیرساخت خنک کننده، زیر ساخت تامین انرژی، اطفاء حریق و غیره)، منابع پردازشی سخت افزاری شامل سرورها، تجهیزات زیرساخت شبکه، زیرساخت ذخیره سازی داده ها و زیرساخت نرم افزاری شامل ابزار یک پارچه سازی[3]، مجموعه ای از سیستم های عامل، مجموعه ای از نرم افزارهای کاربردی شامل سرویس ها، تعدادی پایگاه داده، مجموعه ای از ابزارهای امنیتی نرم افزاری و سخت افزاری و یک ساختار مدیریتی است. این سیستم به کمک خطوط پرسرعت به شبکه های خارجی (Intranet، Extranet یا اینترنت) متصل است ]1[.با توجه به رشد نیازها و احتیاج کاربران به انعطاف پذیری و تحمل خطای بالا در این مراکز پردازشی، در سال های اخیر تکنولوژی مجازی سازی[4] به عنوان پاسخی به این نیازها و بهترین شیوه یکپارچه سازی ارائه شده و بسیار رشد کرده است. در حقیقت، این تکنولوژی به عنوان لایه مدیریت نرم افزاری و سیستم عاملی دیتا سنتر مورد استفاده قرار می گیرد. در ادامه به تشریح تکنولوژی مجازی سازی و نحوه استفاده از آن در این طرح خواهیم پرداخت.تکنولوژی مجازی سازی یکی از جوانترین نظریه های مطرح شده در علم کامپیوتر می باشد که در ده سال اخیر توجه زیادی را به خود جلب نموده است. این تکنولوژی از این بابت بسیار جذاب است که انعطاف پذیری و امکانات خارق العاده ای را بر روی همان بستر سخت افزاری موجود ارائه می دهد و استفاده از آن هزینه بسیار ناچیزی برای سازمان دارد.معماری مجازی سازی، همه منابع پردازشی از جمله سرورها، منابع ذخیره سازی[5] و شبکه را به یک ساختار مجازی نگاشت می دهد. این زیر ساخت با گردآوری همه منابع و نمایش مجموعه ای ساده شده و یکپارچه از آنها، مدیر را در درک بهتر ساختار فنی دیتا سنتر و مدیریت و تغییر آن یاری می رساند. به کمک این ساختار می توان منابع توزیع شده در یک دیتا سنتر را به صورت مجموعه ای یکپارچه از ابزار مدیریت نمود. همچنین می توان از دیتا سنتر برای مصارف گوناگونی استفاده کرد بدون اینکه نگران گوناگونی سخت افزارها و نحوه اتصال آن ها به سیستم باشیم؛ ]2[ و ]3[.از این تکنولوژی برای طراحی زیر ساخت نرم افزاری دیتا سنتر استفاده خواهد شد. با این توضیح که به جای نصب یک سیستم عامل بر روی هر دستگاه سرور، از یک نرم افزار مجازی سازی به نام Hypervisor استفاده می شود. این نرم افزار شبه سیستم عامل به مدیر سیستم اجازه می دهد که به تعداد دلخواه کامپیوتر مجازی[6] بر روی سرور مذکور راه اندازی کرده و سیستم عامل و سرویس های دلخواه را بر روی آن نصب نماید (شکل 1.1). شکل 1.1. نحوه قرارگیری لایه های نرم افزاری بر روی سرور با این ترکیب می توان امکانات بسیار زیادی از جمله قابلیت دسترسی دائمی به سرویس ها (HA)[7] و مقاوم سازی سرویس ها در مقابل خطا[8] که از ضروریات چنین دیتا سنتری می باشد را با کمترین هزینه میسر نمود. همچنین امکان انتقال این کامپیوترهای مجازی در حال کار از روی یک سرور به سرور دیگر را بدون تاخیر زمانی وجود دارد[9].در دیتاسنتری با این ابعاد، اغلب سرویس های در حال کار بسیار حیاتی و حساس بوده و از کار افتادن آن ها هزینه های هنگفت و بعضا جبران ناپذیری برای سازمان مربوطه به دنبال خواهد داشت. به همین دلیل لازم است امکانات حرفه ای را در دیتا سنتر به منظور محافظت از سرویس ها پیاده سازی نمائیم تا در دسترس بودن و سلامت آنها را تضمین کند. شکل 1.2 شمایی کلی از یک دیتا سنتر را با استفاده از معماری یاد شده نشان می دهد. شکل 1.2. شمای کلی دیتا سنتر با معماری مجازی با توجه به نیاز به این مراکز و پیچیدگی ذاتی آنها، ترسیم یک مدل فرمال از ماهیت یک دیتا سنتر، چه پیش از طراحی[10] و چه پس از آن[11]، می تواند در شناخت طرز کار و چگونگی فعالیت چنین مرکزی نقش به سزایی داشته باشد. از جمله این کاربردها می توان به تشخیص بن بست ها[12] و گلوگاه ها[13] قبل از طراحی و محک زدن[14] سیستم بعد از طراحی اشاره نمود. با در دست داشتن این مدل (تصویر فرمال) جریان کنترل در سیستم قابل رویت بوده و در نتیجه رفتار سیستم را می توان بررسی و پیش بینی نمود ]4[. البته باید توجه داشت که در سیستم های واقعی از جمله دیتا سنترها، به دست آوردن مدل جامع تقریبا غیر ممکن بوده و تنها می توان بخش هایی از سیستم را با نادیده گرفتن برخی از پارامترها مدل نمود. هرچقدر مدل به سیستم واقعی نزدیکتر باشد بررسی رفتار سیستم به کمک مدل حاصل دقیقتر و کاربردی تر خواهد بود. در بخش های بعدی با بررسی دقیقتر ماهیت مدل سازی فرمال، با انواع شیوه ها در این حوزه[15] بیشتر آشنا خواهیم شد.به طور کلی متد های فرمال نوع خاصی از شیوه های بیان فرمال مسائل هستند که از آنها برای تشریح و تبیین[16] سیستم های کامپیوتری و همچنین اثبات رفتار آنها[17] در سطح سخت افزار و نرم افزار استفاده می شود. هدف از توضیح رفتار یک سیستم به کمک روش های فرمال، بررسی رفتار و خصوصیات سیستم از جمله میزان حد پذیری[18]، بازگشت پذیری[19] و نیز پارامترهای انتزاعی تر مانند میزان ثبات[20] و پایداری[21] می باشد ]5[.بدیهی است انجام چنین کاری در مورد سیستم های واقعی با توجه به پارامترهای متعدد و ساختار پیچیده آنها بسیار وقت گیر و دشوار است و در بسیاری از مواقع فقط بخش هایی از سیستم را می توان در حد قابل قبولی تشریح و مدل نمود. به همین دلیل و نیز به دلیل هزینه بسیار گزاف این فرایند، استفاده از شیوه های فرمال برای توضیح رفتار سیستم فقط در مورد سیستم های بسیار حساس و گران قیمت صورت می گیرد.در این تحقیق، از زبان شبکه های پتری که ابزاری گرافیکی برای تشریح رفتار سیستم ها می باشد بهره گرفته شده است. این زبان در واقع نوع خاصی از ماشین های متناهی (اتوماتا) می باشد که امکان ترسیم جریان کنترل در سیستم را به صورت ساختار گراف و تعریف مجموعه ها فراهم می کند.
ارائه یک مدل فرمال برای تحلیل زیر ساخت نرم افزاری در دیتا سنترها WORD
در این تحقیق با استفاده از زبان فرمال شبکه های پتری، از بخش ها و جنبه های مختلف لایه مجازی سازی در دیتا سنترها، مدل های فرمال متعددی تهیه شده است. سپس به کمک ابزار ریاضی، رفتار این مکانیزم ها برای تعیین سطح خوش رفتاری سیستم بررسی شده است. برای نیل به این هدف، در ابتدا ابزار مدل سازی فرمال اعم از جبری و مبتنی بر مدل بررسی و مقایسه شده است. سپس با تشریح تکنولوژی مجازی سازی در سیستم های کامپیوتری، یک دیتا سنتر نمونه کوچک مطابق استانداردهای دیتا سنترها طراحی شده و سپس در لایه های مختلف توسط شبکه های پتری مدل گردیده است. این مدل سازی از سطح کاملا انتزاعی[1] (لایه 1) برای کل دیتا سنتر شروع و با طراحی مدل برای زیر سیستم ها و مکانیزم هایی مانند ساختار شبکه، ذخیره سازی و نیز سرویس های سطح بالا مانند HA و Fault Tolerance پایان می یابد. در پایان هر بخش، پس از ارائه و تشریح مدل، به تحلیل و ارزیابی آن و بررسی خصوصیات رفتاری سیستم از روی مدل فرمال آن پرداخته شده است. در نهایت، نتیجه گیری از میزان خوش رفتاری بخش های مختلف این لایه در دیتا سنتر ارائه شده است. فهرست مطالبفصل اول: مقدمه 1فصل دوم: معرفی و بررسی ابزار فرمال برای مدل سازی سیستم ها 122.1. Abstract State Machine (ASM) 142.2. LOTOS 172.2.1.مقدمه ای بر جبر پروسه ها 182.3. VDM-SL 222.4. شبکه های پتری 232.4.1.خصوصیات رفتاری 252.4.1.1. Reachability 262.4.1.2. Boundedness 262.4.1.3. Liveness 262.4.1.4. Reversibility 282.4.1.5. Coverability 282.4.2.زیر مجموعه های شبکه های پتری 292.4.2.1. State Machine (SM) 302.4.2.2. Marked Graph (MG) 302.4.2.3. Free-choice net (FC) 312.4.2.4. Extended Free-choice net (EFC) 312.4.2.5. Asymmetric choice net (AC) 312.4.3.قضایا و فرضیات 322.5. مقایسه و جمع بندی 35فصل سوم: بررسی معماری دیتا سنترها 383.1. Microsoft Hyper-V 393.1.1.بررسی اجزاء معماری Hyper-V 423.1.1.1. APIC 433.1.1.2. Child Partition 433.1.1.3. Hypercall 433.1.1.4. Hypervisor 433.1.1.5. IC 433.1.1.6. I/O stack 443.1.1.7. Root Partition 443.1.1.8. VID 443.1.1.9. VMBus 443.1.1.10. VMMS 443.1.1.11. VMWP 443.1.1.12. VSC 453.1.1.13. VSP 453.1.1.14. WinHv 453.1.1.15. WMI 453.1.2.نقاط ضعف 463.2. Xen 463.2.1.بررسی اجزاء معماری Xen 483.2.1.1. Xen Hypervisor 483.2.1.2. Domain 0 483.2.1.3. Domain U 493.2.1.4. Xenstored 503.2.2.ارتباطات مابین دامنه صفر و دامنه های U 503.3. VMware ESXi 503.3.1.بررسی اجزاء معماری VMware ESX 523.3.1.1. VMkernel 523.3.1.2. File System 523.3.1.3. CIM 533.4. طراحی یک معماری برای دیتا سنتر 543.5. مختصری درباره vSphere 563.5.1.سرویس های زیر ساختی vSphere 583.5.2.سرویس های کاربردی vSphere 593.5.2.1. سرور VMware vCenter 593.5.2.2. Client ها 593.5.2.3. ESX 593.5.2.4. vCenter Server 593.5.2.5. VMFS 593.5.2.6. SMP 603.5.2.7. VCMS 603.5.2.8. VI Client 603.5.2.9. VMware VMotion 603.5.2.10. Storage VMotion 603.5.2.11. VMware HA 613.5.2.12. DRS 623.5.2.13. Consolidated Backup 633.5.2.14. vSphere SDK 633.5.2.15. Fault Tolerance 643.5.3.سرویس های توزیع شده در vSphare 643.5.4.معماری شبکه 643.5.5.معماری محل ذخیره سازی داده ها 663.5.6.معماری سرور مدیریت VirtualCenter 693.5.6.1. User Access Control 703.5.6.2. Core Service 713.6. جمع بندی 71فصل چهارم: ارائه مدل فرمال برای دیتا سنتر و تحلیل آن 724.1. تشریح دیتا سنتر نمونه 734.2. ارائه مدلی از رفتار کلی دیتا سنتر 774.2.1.ارزیابی و تحلیل مدل فرمال 874.2.1.1. Liveness 874.2.1.2. Safeness 874.2.1.3. Reversibility 894.2.2.بررسی لایه های پایینتر مدل فرمال 904.3. بررسی نحوه کار سرویس HA 914.3.1.شرح سرویس VMware HA 914.3.2.ارائه مدل فرمال از نحوه کار سرویس HA 954.3.3.تحلیل و ارزیابی مدل 984.3.3.1. Liveness 994.3.3.2. Safeness 1014.3.3.3. Reversibility 1024.4. بررسی نحوه کار سرویس Fault Tolerance 1064.4.1.تشریح ساختار سرویس Fault Tolerance 1064.4.2.ارائه مدل فرمال از نحوه کار سرویس Fault Tolerance 1104.4.3.تحلیل و ارزیابی مدل 1114.4.3.1. Liveness 1124.4.3.2. Safeness 1134.4.3.3. Reversibility 1134.5. بررسی نحوه کار سرویس VMotion 1144.5.1.تشریح ساختار سرویس VMotion 1144.5.2.ارائه مدل فرمال از نحوه کار سرویس VMotion 1184.5.3.تحلیل و ارزیابی مدل 1194.5.3.1. Liveness 1204.5.3.2. Safeness 1214.5.3.3. Reversibility 1224.6. بررسی ساختار داخلی ESX hypervisor 1244.6.1.تشریح ساختار ESX 1244.6.2.ارائه یک مدل فرمال از نحوه کار ESX 1254.6.3.بررسی و تحلیل مدل 1294.6.3.1. Liveness 1294.6.3.2. Safeness 1314.6.3.3. Reversibility 1324.7. تشریح ساختار سیستم ذخیره سازی در ESX 1334.7.1.تشریح ساختار سیستم ذخیره سازی 1334.7.2.ارائه یک مدل فرمال از نحوه کار سیستم ذخیره سازی در ESX 1384.7.3.بررسی و تحلیل مدل 1444.7.3.1. Liveness 1444.7.3.2. Safeness 1454.7.3.3. Reversibility 1464.8. معماری ساختار شبکه در ESX 1484.8.1.تشریح ساختار شبکه 1484.8.2.ارائه مدل فرمال برای ساختار شبکه در ESX 1554.8.3.بررسی و تحلیل مدل 1614.8.3.1. Reversibility 1614.8.3.2. Liveness 1634.8.3.3. Safeness 1654.9. معماری سوئیچ مجازی در ساختار شبکه 1654.9.1.تحلیل ساختار سوئیچ مجازی 1654.9.2.ارائه یک مدل فرمال برای سوئیچ مجازی 1694.9.3.بررسی و تحلیل مدل 1724.9.3.1. Liveness 1724.9.3.2. Safeness 1734.9.3.3. Reversibility 1744.10. جمع بندی 175فصل پنجم: نتیجه گیری و پیشنهادات 176مراجع 180پیوست: مجموعه کامل مدل های پتری طراحی شده در پایان نامه 186چکیده به زبان انگلیسی 195 فهرست جدول ها عنوان و شماره صفحه جدول 2.1. خلاصه مقایسه ابزار توصیف فرمال 36جدول 3.1. سیستم های عامل قابل پشتیبانی توسط Hyper-V R2 41جدول 3.2. سیستم های عامل قابل پشتیبانی توسط Xen نسخه 3. 47جدول 4.1. گزارهای فعال در وضعیت های M0 الی M15 از مدل پتری 4.30 164جدول 5.1. خلاصه نتایج به دست آمده از تحلیل رفتار زیر سیستم ها و سرویس های VMware ESX177 فهرست شکل ها عنوان صفحه شکل 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شکل 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. نحوه توزیع توکن ها در M3 و M4 112شکل 4.16. گراف پوشای مدل پتری شکل 4.14 114شکل 4.17 مدل پتری نحوه کار سرویس VMotion 118شکل 4.18. گراف نشانه دار (G, ) مربوط به مدل 4.17 120شکل 4.19. گراف پوشای مدل 4.17 123شکل 4.20. مدل پتری طرز کار ESX 125شکل 4.21. گراف جهت دار معادل شبکه پتری 4.20 130شکل 4.22. گراف پوشای کدل پتری 4.20 132شکل 4.23. نمای شماتیک مدل چند لایه ای سیستم ذخیره سازی در ESX]63[ 134شکل 4.24. مدل پتری ارائه شده از نحوه کار سیستم ذخیره سازی در ESX 139شکل 4.25. گراف جهت دار متناظر با مدل پتری 4.24 144شکل 4.26. گراف پوشای شبکه پتری 4.24 146شکل 4.27. نرم افزار تحلیلگر گراف، در حال اجرای الگوریتم اول عمق 147شکل 4.28. نحوه ارتباط کارت شبکه مجازی و سوئیچ مجازی ]62[ 149شکل 4.29. شمای کلی از ساختار شبکه در سرور ESX 153شکل 4.30. مدل پتری تهیه شده از ساختار شبکه در ESX 156شکل 4.31. گراف پوشای مدل پتری شکل 4.30 162شکل 4.32. جستجوی اول عمق گراف شکل 4.31 163شکل 4.33 مدل فرمال از نحوه کار سوئیچ مجازی 170شکل 4.34. گراف جهت دار متناظر با مدل پتری 4.33 173شکل 4.35. گراف پوشای مدل پتری 4.33 174 فصل اول: مقدمه 1.1. بيان مسئله و ضرورت تحقيق نیاز بشر به پردازش و ذخیره سازی اطلاعات در دهه های گذشته همواره رشد صعودی و شتابدار داشته است. به گونه ای که حرکت از سیستم های توزیع شده بر روی سوپرکامپیوترهای گران قیمت به شبکه های بسیار پر قدرت و ارزان در مدت نسبتا کوتاهی صورت گرفته است. همچنین نیاز به مدیریت اطلاعات، پردازش، گردش کار و دیگر ابزار مدیریتی همواره رشد فزاینده داشته است. به طبع این نیاز، ساختار سیستم های کامپیوتری در سطوح فنی و مدیریتی نیز رشد کرده و پیچیده تر شده است.به منظور جوابگویی به این حجم فزاینده درخواست ها و نیاز بازار به منابع پردازش و ذخیره سازی اطلاعات و نیز به منظور ارائه سرویس های مورد نیاز با کیفیت مناسب و قابل رقابت، یکی از بهترین راه های پیشنهاد شده، متمرکز نمودن این منابع و مدیریت صحیح آنها است. به این منظور و برای به حداکثر رساندن کیفیت خدمات و حداقل نمودن هزینه ها یکی از رایج ترین راهکارهای موجود راه اندازی مراکز داده یا دیتا سنتر ها می باشد. در این طرح با آماده سازی زیر ساخت های فیزیکی، امنیتی، شبکه ای، سخت افزاری و نرم افزاری، مجموعه ای از سرورهای قدرتمند برای ارائه سرویس های مورد نیاز مشتریان در نظر گرفته می شود. این سرورها با خطوط بسیار پر سرعت بر حسب نیاز به اینترنت یا شبکه های سازمانی متصل می گردند و با نصب سیستم های عامل و نرم افزارها و سرویس های مورد نیاز به کاربران خدمات لازم را ارائه می نمایند. با وجود چنین مراکزی دیگر سازمان ها و مراکز تجاری، صنعتی، دانشگاهی و غیره نیازی به راه اندازی مراکز سرویس دهی محلی[2] و نیز متحمل شدن هزینه های نگهداری، به روز رسانی و استخدام متخصصین نخواهند داشت. در ادامه به بررسی اجمالی دیتا سنترها خواهیم پرداخت تا بتوانیم طرح پیشنهادی را تشریح نمائیم.تعریف دیتا سنتر: مجموعه ای از سیستمهای پشتیبانی (از جمله زیر ساخت سخت افزاری passive، زیرساخت خنک کننده، زیر ساخت تامین انرژی، اطفاء حریق و غیره)، منابع پردازشی سخت افزاری شامل سرورها، تجهیزات زیرساخت شبکه، زیرساخت ذخیره سازی داده ها و زیرساخت نرم افزاری شامل ابزار یک پارچه سازی[3]، مجموعه ای از سیستم های عامل، مجموعه ای از نرم افزارهای کاربردی شامل سرویس ها، تعدادی پایگاه داده، مجموعه ای از ابزارهای امنیتی نرم افزاری و سخت افزاری و یک ساختار مدیریتی است. این سیستم به کمک خطوط پرسرعت به شبکه های خارجی (Intranet، Extranet یا اینترنت) متصل است ]1[.با توجه به رشد نیازها و احتیاج کاربران به انعطاف پذیری و تحمل خطای بالا در این مراکز پردازشی، در سال های اخیر تکنولوژی مجازی سازی[4] به عنوان پاسخی به این نیازها و بهترین شیوه یکپارچه سازی ارائه شده و بسیار رشد کرده است. در حقیقت، این تکنولوژی به عنوان لایه مدیریت نرم افزاری و سیستم عاملی دیتا سنتر مورد استفاده قرار می گیرد. در ادامه به تشریح تکنولوژی مجازی سازی و نحوه استفاده از آن در این طرح خواهیم پرداخت.تکنولوژی مجازی سازی یکی از جوانترین نظریه های مطرح شده در علم کامپیوتر می باشد که در ده سال اخیر توجه زیادی را به خود جلب نموده است. این تکنولوژی از این بابت بسیار جذاب است که انعطاف پذیری و امکانات خارق العاده ای را بر روی همان بستر سخت افزاری موجود ارائه می دهد و استفاده از آن هزینه بسیار ناچیزی برای سازمان دارد.معماری مجازی سازی، همه منابع پردازشی از جمله سرورها، منابع ذخیره سازی[5] و شبکه را به یک ساختار مجازی نگاشت می دهد. این زیر ساخت با گردآوری همه منابع و نمایش مجموعه ای ساده شده و یکپارچه از آنها، مدیر را در درک بهتر ساختار فنی دیتا سنتر و مدیریت و تغییر آن یاری می رساند. به کمک این ساختار می توان منابع توزیع شده در یک دیتا سنتر را به صورت مجموعه ای یکپارچه از ابزار مدیریت نمود. همچنین می توان از دیتا سنتر برای مصارف گوناگونی استفاده کرد بدون اینکه نگران گوناگونی سخت افزارها و نحوه اتصال آن ها به سیستم باشیم؛ ]2[ و ]3[.از این تکنولوژی برای طراحی زیر ساخت نرم افزاری دیتا سنتر استفاده خواهد شد. با این توضیح که به جای نصب یک سیستم عامل بر روی هر دستگاه سرور، از یک نرم افزار مجازی سازی به نام Hypervisor استفاده می شود. این نرم افزار شبه سیستم عامل به مدیر سیستم اجازه می دهد که به تعداد دلخواه کامپیوتر مجازی[6] بر روی سرور مذکور راه اندازی کرده و سیستم عامل و سرویس های دلخواه را بر روی آن نصب نماید (شکل 1.1). شکل 1.1. نحوه قرارگیری لایه های نرم افزاری بر روی سرور با این ترکیب می توان امکانات بسیار زیادی از جمله قابلیت دسترسی دائمی به سرویس ها (HA)[7] و مقاوم سازی سرویس ها در مقابل خطا[8] که از ضروریات چنین دیتا سنتری می باشد را با کمترین هزینه میسر نمود. همچنین امکان انتقال این کامپیوترهای مجازی در حال کار از روی یک سرور به سرور دیگر را بدون تاخیر زمانی وجود دارد[9].در دیتاسنتری با این ابعاد، اغلب سرویس های در حال کار بسیار حیاتی و حساس بوده و از کار افتادن آن ها هزینه های هنگفت و بعضا جبران ناپذیری برای سازمان مربوطه به دنبال خواهد داشت. به همین دلیل لازم است امکانات حرفه ای را در دیتا سنتر به منظور محافظت از سرویس ها پیاده سازی نمائیم تا در دسترس بودن و سلامت آنها را تضمین کند. شکل 1.2 شمایی کلی از یک دیتا سنتر را با استفاده از معماری یاد شده نشان می دهد. شکل 1.2. شمای کلی دیتا سنتر با معماری مجازی با توجه به نیاز به این مراکز و پیچیدگی ذاتی آنها، ترسیم یک مدل فرمال از ماهیت یک دیتا سنتر، چه پیش از طراحی[10] و چه پس از آن[11]، می تواند در شناخت طرز کار و چگونگی فعالیت چنین مرکزی نقش به سزایی داشته باشد. از جمله این کاربردها می توان به تشخیص بن بست ها[12] و گلوگاه ها[13] قبل از طراحی و محک زدن[14] سیستم بعد از طراحی اشاره نمود. با در دست داشتن این مدل (تصویر فرمال) جریان کنترل در سیستم قابل رویت بوده و در نتیجه رفتار سیستم را می توان بررسی و پیش بینی نمود ]4[. البته باید توجه داشت که در سیستم های واقعی از جمله دیتا سنترها، به دست آوردن مدل جامع تقریبا غیر ممکن بوده و تنها می توان بخش هایی از سیستم را با نادیده گرفتن برخی از پارامترها مدل نمود. هرچقدر مدل به سیستم واقعی نزدیکتر باشد بررسی رفتار سیستم به کمک مدل حاصل دقیقتر و کاربردی تر خواهد بود. در بخش های بعدی با بررسی دقیقتر ماهیت مدل سازی فرمال، با انواع شیوه ها در این حوزه[15] بیشتر آشنا خواهیم شد.به طور کلی متد های فرمال نوع خاصی از شیوه های بیان فرمال مسائل هستند که از آنها برای تشریح و تبیین[16] سیستم های کامپیوتری و همچنین اثبات رفتار آنها[17] در سطح سخت افزار و نرم افزار استفاده می شود. هدف از توضیح رفتار یک سیستم به کمک روش های فرمال، بررسی رفتار و خصوصیات سیستم از جمله میزان حد پذیری[18]، بازگشت پذیری[19] و نیز پارامترهای انتزاعی تر مانند میزان ثبات[20] و پایداری[21] می باشد ]5[.بدیهی است انجام چنین کاری در مورد سیستم های واقعی با توجه به پارامترهای متعدد و ساختار پیچیده آنها بسیار وقت گیر و دشوار است و در بسیاری از مواقع فقط بخش هایی از سیستم را می توان در حد قابل قبولی تشریح و مدل نمود. به همین دلیل و نیز به دلیل هزینه بسیار گزاف این فرایند، استفاده از شیوه های فرمال برای توضیح رفتار سیستم فقط در مورد سیستم های بسیار حساس و گران قیمت صورت می گیرد.در این تحقیق، از زبان شبکه های پتری که ابزاری گرافیکی برای تشریح رفتار سیستم ها می باشد بهره گرفته شده است. این زبان در واقع نوع خاصی از ماشین های متناهی (اتوماتا) می باشد که امکان ترسیم جریان کنترل در سیستم را به صورت ساختار گراف و تعریف مجموعه ها فراهم می کند.