پیشینه تحقیق ابزار فرمال مدل سازی سیستم ها و معرفی نرم افزارهای مدیریت ماشین های مجازی دارای ۵۰ صفحه می باشد فایل پیشینه تحقیق به صورت ورد  word و قابل ویرایش می باشد. بلافاصله بعد از پرداخت و خرید لینک دنلود فایل نمایش داده می شود و قادر خواهید بود  آن را دانلود و دریافت نمایید . ضمناً لینک دانلود فایل همان لحظه به آدرس ایمیل ثبت شده شما ارسال می گردد.

فهرست مطالب

فصل اول: مروری بر ابزار فرمال مدل سازی سیستم ها    ۵
ASM 2-1    ۷
LOTOS2-2-    ۱۰
۲-۲-۱-مقدمه ای بر جبر پروسه ها ]۱۶[    ۱۰
VDM-SL2-3-    ۱۴
۲-۴-شبکه های پتری    ۱۶
۲-۴-۱-خصوصیات رفتاری    ۱۸
Reachability2-4-1-1-    ۱۸
Boundedness2-4-1-2-    ۱۸
Liveness2-4-1-3    ۱۹
Reversibility2-4-1-4-    ۲۰
Coverability2-4-1-5-    ۲۱
۲-۴-۲-زیر مجموعه های شبکه های پتری    ۲۱
State Machine (SM)2-4-2-1-    ۲۲
Marked Graph (MG) 2-4-2-2-    ۲۳
Free-choice net (FC) 2-4-2-3-    ۲۳
Extended Free-choice net (EFC) 2-4-2-4-    ۲۳
Asymmetric choice net (AC) 2-4-2-5-    ۲۳
۲-۴-۳-قضایا و فرضیات ]۲۳[    ۲۴
۲-۵-جمع بندی    ۲۷
فصل دوم: معماری نرم افزارهای مدیریت ماشین های مجازی ( نرم افزارهای  Hypervisor)    ۲۹
Microsoft Hyper-V3-1-    ۳۰
۳-۱-۱-بررسی اجزاء معماری Hyper-V    ۳۳
APIC3-1-1-1-    ۳۴
Child Partition3-1-1-2-    ۳۴
Hypercall3-1-1-3-    ۳۴
Hypervisor3-1-1-4-    ۳۴
IC3-1-1-5-    ۳۴
I/O stack3-1-1-6-    ۳۴
Root Partition3-1-1-7-    ۳۵
VID3-1-1-8-    ۳۵
VMBus3-1-1-9-    ۳۵
VMMS3-1-1-10-    ۳۵
VMWP3-1-1-11-    ۳۵
VSC3-1-1-12-    ۳۶
VSP3-1-1-13-    ۳۶
WinHv3-1-1-14-    ۳۶
WMI3-1-1-15-    ۳۶
۳-۱-۲-نقاط ضعف    ۳۶
Xen3-2-    ۳۷
۳-۲-۱-بررسی اجزاء معماری Xen    ۳۸
Xen Hypervisor3-2-1-1-    ۳۹
Domain 03-2-1-2-    ۳۹
Domain U3-2-1-3-    ۳۹
Xenstored3-2-1-4-    ۴۰
۳-۲-۲-ارتباطات مابین دامنه صفر و دامنه های U    ۴۱
VMware ESXi3-3-    ۴۱
۳-۳-۱-بررسی اجزاء معماری VMware ESX    ۴۲
VMkernel3-3-1-1-    ۴۳
File System3-3-1-2-    ۴۳
CIM3-3-1-3-    ۴۳

مراجع    ۴۶

منابع

۱-Yaozu Dong et. All, “Extending Xen with Intel Virtualization Technology”, Intel Technology Journal, Vol. 10, Issue 3, ISSN: 1535-864X, Aug. 2006.

۲-Ian Pratt, “Xen Status Report”, Description and status report on the Xen 3.0 development, University of Cambridge, April 2005.

۳-Fengzhe Zhang, Jin Chen, Binyu Zang, “CloudVisor: Retrofitting Protection of Virtual Machines in Multi-tenant Cloud with Nested Virtualization”, Proceedings of Symposium on Operating Systems Principles (SOSP-2011), Cascais, Portugal, October 2011.

۴-W.M.P. van der Aalst, K.M. van Hee, G.J. Houben, “Modelling and Analysing Workflow using a Petri-net based approach”, Proceedings of Second Workshop on Computer-supported Cooperative Work, Petri nets related formalisms, pp. 31-50, 1994.

۵-Emine G. Aydal, Richard F. Paige, Mark Utting, Jim Woodcock, “Putting Formal Specifications under the Magnifying Glass: Model-based Testing for Validation”, IEEE Proc. ICST ’۰۹ on Software Testing Verification and Validation, 2009, ISBN: 978-0-7695-3601-9

۶-Diwaker Gupta, Ludmila Cherkasova, Rob Gardner, Amin Vahdat, “Enforcing Performance Isolation Across Virtual Machines in Xen”, Proceedings of the 7th ACM/IFIP/USENIX Middleware Conference. Melbourne, Australia, Nov. 2006.

۷-John Fitzgerald, Peter Gorm Larsen and Shin Sahara, “Technical report series: Modeling and Analysis in VDM”, Proceedings of the Fourth VDM/Overture Workshop, University of Newcastle upon Tyne, No. CS-TR-1099,  May 2008.

۸-Massimo, “A brief architecture overview of VMware ESX, XEN and MS Viridian”, [Online]. Available.

۹-VMeare, “A Performance Comparison of Hypervisors”, VMware Inc., Performance study, Revision: 20070201 Item: PS-004-INF-01-002, 2007.

۱۰-Tim Abels, Puneet Dhawan, Balasubramanian Chandrasekaran, “An Overview of Xen Virtualization”, Dell Power Solutions, Aug. 2005.

۱۱-Microsoft Inc., CA Inc., “Protecting your Virtualized Server Investment ”, White paper, May 2010.

۱۲-Ray Weinstein, Burk Buechler, “HigHly AvAilAble virtuAlizAtion WitH Microsoft Hyper-v And scvMM 2008”, Dell Power Solutions, Nov. 2008.

۱۳-Robert Larson, Janique Carbone et.All, “Windows Server 2008 Hyper-V Resource Kit”, Microsoft Press, ISBN: 0-7356-2517-4, June 2009.

۱۳-Ian Pratt, “Xen and the Art of Virtualization”, University of Cambridge and Founder of XenSource Inc., 2006.

فصل اول: مروری بر ابزار فرمال مدل سازی سیستم ها

طبق آمار سایت های غیر رسمی[۱] در حدود ۱۰۰ متد فرمال به صورت زبان، notation و ابزار وجود دارد که به منظور تشریح فرمال سیستم ها و مسائل از آنها استفاده می شود. پارامترهای زیادی وجود دارد که نقاط قوت و ضعف هر یک از ابزار مذکور را نسبت به دیگران تعیین می نماید اما در این بین تعدادی از این مصادیق به دلایلی عمومیت بیشتری یافته اند و بیشتر در مورد بررسی و به روز رسانی قرار گرفته اند.

به طور کلی می توان ابزار توصیف فرمال[۲] را به دو گروه متدهای جبری و متدهای مبتنی بر مدل تقسیم بندی نمود ]۵[ و ]۱۰[. اگر فرض نمائیم که بهترین شیوه شناخت و توصیف سیستم ها شکستن آنها به بخش های کوچکتر و ساده تر[۳] برای کنترل پیچیدگی سیستم است، از بررسی شیوه توصیف هریک از این دو نوع ابزار می توان نتیجه گرفت که متدهای جبری برای توصیف interface بین بخش های سیستم مذکور مناسب است زیرا خصوصیات کارکردی[۴] یا ساختاری[۵] سیستم را به نحو مطلوبی نشان می دهد. با این حال این ابزار برای تشریح رفتار سیستم چندان کارآمد نیست. به منظور توصیف خصوصیات رفتاری یک سیستم[۶] از ابزار مدل سازی فرمال استفاده می گردد.

به طور کلی استفاده از توصیف فرمال سیستم ها قبل از طراحی و پیاده سازی، همراه با مشکلاتی مانند هزینه بر بودن، زمان بر بودن و نیز دشواری و پیچیدگی در بیان و ارزیابی آن است. این موانع باعث شده است تا این شیوه توسعه برخلاف آنچه که در دهه ۱۹۸۰  پیش بینی می شد، پرکاربرد ترین شیوه توسعه سیستم های نرم افزاری و سخت افزاری نشود. با این حال مزایای این روش پیاده سازی که کاهش محسوس خطاهای سیستم در هنگام طراحی و پیاده سازی است باعث شده است که در طراحی سیستم های حیاتی و گران قیمت مورد استفاده قرار گیرد.

همانگونه که دیده می شود، برقراری درک دقیقی از نیازمندیهای سیستم[۱] ، طراحی معماری و نیز توصیف (درک) فرمال سیستم به شکلی با یکدیگر ادغام شده اند که بازخورد هر مرحله از توصیف به کامل تر شدن طراحی در همان مرحله کمک می کند. بنابراین در پایان فاز توصیف فرمال، حداقل میزان خطا و حالات پیش بینی نشده در سیستم وجود خواهد داشت. درصد این خطا مستقیما به میزان توانایی ابزار توصیف در بررسی و تبیین جنبه های مختلف کارکردی و رفتاری سیستم باز می گردد ]۱۱[.

در ادامه سعی می کنیم تعدادی از این ابزار فرمال را تشریح کرده و با هم مقایسه نمائیم. بعضی از نمونه ها تنها به صورت متد بوده و بعضی دیگر دارای گرامر نیز می باشند و زبان هستند.

 ASM 2-1

ASM[2] از ساختارهای کلاسیک ریاضی برای توصیف فرمال سیستم استفاده می کند بنابراین بسیار دقیق است. با این توضیح که ASM متدی مبتنی بر جبر رابطه ای و مناسب برای توصیف سیستم های تسلسلی است. باید توجه داشت که اگر در توصیف مسائل، semantic متد به کار رفته مبهم باشد توصیف حاصل واضح تر از تعریف اولیه سیستم نخواهد بود. بنابراین ASM با یک تعریف ریاضی، وضوح و یگانگی درک مفهوم مورد نظر را تضمین می کند[۳]. ASM شکل خاصی از finite-state automata است که از مجموعه ای از ساختار های داده ای[۴] و توابع ریاضی تشکیل شده است و برای توصیف الگوریتم ها بر اساس حالات[۵] آنها به کار می رود ]۱۲[.

در واقع ASM یک ساختار قراردادی ساده یا پیچیده از قواعد ریاضی است که از مجموعه ای از دامنه ها (یا مجموعه ها که هر یک نوع مشخصی از اشیا را نشان می دهند) و توابع و روابط قراردادی بر روی آنها تعریف شده اند ]۱۳[. همانگونه که دیده می شود این مجموعه بسیار انتزاعی و مستقل از نوع مساله است.

دستیابی به سطوح بالایی از انتزاع از مهمترین مزایای ASM است.

در ادامه نمونه از تعریف فرمال ASM را برای سیستم PVM[6] مشاهده می کنیم ]۱۲[:

master : HOST

مشخص کننده ی ماشینی است که PVM روی آن اجرا می شود و و نقش کلیدی در مدیریت و نگهداری پیکره پویای PVM دارد.

arch : HOST → ARCH

تابع arch که معماری هر یک از HOSTها را مشخص می کند. این معماری عضوی از مجموعه انتزاعی ARCH است.

daemon : HOST → DAEMON

این تابع برای هر عضو از مجموعه HOST، پروسه ای از مجموعه DAEMON را مشخص می کند که وظیفه مدیریت برنامه های آن هاست و نیز ارتباطات بین پروسه ها را برعهده دارد. این daemon به کمک مجموعه ای از پروسه ها بر روی host پیاده سازی می شود.

[۱] system requirements specification

[۲] Abstract State Machine

[۳] Well-understoodness

[۴] Data Structure

[۵] States

[۶] Parallel Virtual Machine

[۱] http://formalmethods.wikia.com/wiki/VL#WikiaArticle

[۲] Formal Specification

[۳] Component

[۴] Functional Properties

[۵] Structural properties

[۶] Behavioral Properties

[۷] Sequential

[۸] Concurrent

تمامی فایل های پیشینه تحقیق و پرسشنامه و مقالات مربوطه به صورت فایل دنلودی می باشند و شما به محض پرداخت آنلاین مبلغ همان لحظه قادر به دریافت فایل خواهید بود. این عملیات کاملاً خودکار بوده و توسط سیستم انجام می پذیرد. جهت پرداخت مبلغ شما به درگاه پرداخت یکی از بانک ها منتقل خواهید شد، برای پرداخت آنلاین از درگاه بانک این بانک ها، حتماً نیاز نیست که شما شماره کارت همان بانک را داشته باشید و بلکه شما میتوانید از طریق همه کارت های عضو شبکه بانکی، مبلغ  را پرداخت نمایید.