در این زبان می توان از سودوکدهای ساده استفاده نمود بنابراین نحو[39] زبان برای اکثر افراد قابل درک است. بر خلاف بسیاری از ابزار، می توان مدل طرح شده به ASM را مستقیما اجرا نمود تا نتیجه رفتار سیستم مشخص گردد. همچنین از این ابزار می توان برای مدل کردن طیف وسیعی از سیستم ها استفاده کرد. از جمله می توان به سیستم های تسلسلی، موازی، توزیع شده، real time، سیستم های متناهی و نامتناهی و غیره اشاره نمود که نشان دهنده انعطاف پذیری ابزار می باشد. در ادامه نمونه ای از نحو زبان ASM آورده شده است. این بخش چگونگی انتقال پیام مابین Agent ها را نشان می دهد. ]14[. class COMMUNICATOR Program() = let availableMsgs = {m | m in me.mailbox where ReadyToDeliver(m)} let selectedMsgs = chooseSubset(availableMsgs) forall msg in selectedMsgs me.mailbox(msg) := false //delete the message let resolvedMsgs = ResolveMessage(msg) //resolve the message forall m in resolvedMsgs let a = Recipient(m) if a <> undef then // if recipient found InsertMessage(a,m) // forward the message else skip // else ignore message برای مطالعه بیشتر به ]29[ الی ]32[ مراجعه کنید. LOTOS LOTOS[40] توسط سازمان ISO برای بیان فرمال استاندارد های مربوط به OSI ساخته شد. این زبان به عنوان به عنوان یک FDT[41] تحت استاندارد ISO/IEC 8807 در سال 1989 ارائه گردید[42]. LOTOS یک زبان توصیف فرمال مبتنی بر روابط جبری است که برای توصیف سیستم های موازی و توزیع شده مناسب می باشد ]15[. در واقع دو بخش اصلی تشکیل دهنده LOTOS عبارتست از ADT[43] و جبر پروسه ها. به دلیل پشتیبانی از گونه های داده ای انتزاعی، این زبان می تواند تبادل اطلاعات و در نتیجه رابطه بین اجرا را به خوبی توصیف نماید. همچنین به دلیل جبری بودن، خواص عملکردی سیستم را توصیف می نماید. به علاوه، پشتیبانی از عملگرهای --poral باعث می شود که این زبان توانایی توصیف خواص رفتاری و جنبه های زمانی سیستم ها را نیز داشته باشد. مقدمه ای بر جبر پروسه ها[44] ]16[ در این جبر، اجزای سیستم به صورت پروسه های انتزاعی نمایش داده می شوند که با یکدیگر ارتباط دارند. پروسه ها به صورت جعبه سیاه دیده می شوند که تنها رفتار خارجی آنها مورد بررسی قرار می گیرد. همچنین پروسه ها به کمک مکانیزم interaction point با یکدیگر رابطه برقرار می کنند. در LOTOS به این نقاط event gate یا به اختصار gate گفته می شود (شکل 2.3). شکل 2.3. نقطه gate در جبر پروسه ها ]4[ Event نشان دهنده یک همگامی[45] بین دو یا چند پروسه است. به طور کلی سه نوع event تعریف شده اند: Pure synchronization: هیچ مقداری بین پروسه ها تبادل نمی شود. Value establishment: مقادیر ارائه شده توسط یک یا چند پروسه از سوی بقیه مورد پذیرش نیست. Value negotiation: مقادیر از سوی یک یا چند پروسه مورد قبول است. همچنین یک عبارت رفتاری[46] انتخابی از بین مجموعه ای از event ها است که برای یک محیط مطرح می گردد. در شرایطی که امکان همگام سازی بین eventهای پیشنهاد شده در یک محیط وجود نداشته باشد یک بن بست[47] رخ داده است. همچنین اگر هیچ پیشنهادی در محیط مطرح نشده باشد یک livelock رخ می دهد (مانند یک حلقه بینهایت). همچنین LOTOS مفهوم ترتیب زمانی eventها را نیز به قواعد جبری موجود اضافه نموده است. این زبان از عملگرهای --poral برای ترکیب عبارات رفتاری و به دست آوردن عبارات رفتاری پیچیده تر استفاده می کند. در عین حال این عملگرها از قواعد خوش تعریف پیروی می نمایند که تفسیر صریح و یکسانی را برای افراد ممکن می سازد. به عنوان خلاصه ای از خصوصیات LOTOS، می توان آنرا تعریف فرمالی از ترکیب داده و کنترل، بر مبنای جبر پروسه ها دانست که همزمانی[48] یکی خصوصیات ذاتی آن است. همچنین قواعد LOTOS به دلیل عملیاتی بودن قابل تفسیر و اجرا[49] می باشد و ماژولار است ]17[. در ادامه مثالی از مدلسازی مساله تولید کننده- مصرف کننده[50] با این زبان آورده شده است. در این مساله سه ماژول تولید کننده، مصرف کننده و کانال که وظیفه هماهنگ سازی این دو را به عهده دارد حضور دارند. لازم به ذکر است که تغییراتی در صورت مساله به وجود آمده تا خصوصیات LOTOS بهتر نشان داده شود. ازآن جمله، تولید کننده می تواند دو خروجی را به صورت همزمان یا غیر همزمان تولید نماید و سپس متوقف شود. همچنین مصرف کننده پس از مصرف ترتیبی یا همزمان آنها متوقف می گردد (شکل 2.4). شکل 2.4. مدل تولید کننده- مصرف کننده به کمک LOTOS ]17[ برای کنترل پیچیدگی مساله، در ابتدا عمل تجزیه[51] را روی این سه بخش انجام داده و هر یک را به عنوان یک پروسه مستقل تشریح می کنیم. سپس آنرا را با هم ترکیب می نمائیم. با توجه به تعاریف pc1 و pc2 به عنوان کانال های تولید کننده و cc1 و cc2 به عنوان کانال های مصرف کننده و همچنین عملگرهای انتخاب ([]) و فعال سازی[52] (>>) می توان پروسه های فوق را به صورت زیر تعریف نمود: پروسه تولید کننده: process Producer [pc1, pc2] : exit := pc1; pc2; exit endproc پروسه کانال: process Channel [ pc1, pc2, cc1, cc2] : exit := pc1; ( pc2; cc1; exit [] cc1; pc2; exit ) >> cc2; exit endproc پروسه مصرف کننده: process Consumer [cc1, cc2] : exit := cc1; cc2; exit endproc در این بین می توان جزئیات اجرایی بیشتر مانند عملکرد داخلی هریک از پروسه ها را با عملگرهای بیشتری مدل نمود به عنوان مثال مساله گم شدن یکی از ورودی ها به کانال به شکل زیر قابل توصیف است: process Channel [pc1, pc2, cc1, cc2] : exit := pc1; ( pc2 ; cc1; exit [] cc1; pc2; exit [] i; pc2; exit ) >> ( cc2; exit [] i; exit) Endproc در نهایت با تعریف عملگر میانه گزاری[53] (|||) برای شبیه سازی توازی[54] بین پروسه ها می توان ترکیب سه پروسه یاد شده را به شکل زیر نوشت: specification Producer_Consumer [ pc1, pc2, cc1 cc2 ] : exit behavior ( Producer [ pc1, pc2 ] ||| Consumer [ cc1, cc2 ] ) || Channel [pc1, pc2, cc1, cc2] where process Producer [ out1, out2 ] : exit := . . . (*As defined previously*) process Consumer [ in1, in2 ] : exit := . . . (*As defined previously *) process Channel [ le1, le2, , re1, re2 ] : exit := . . . (*As defined previously *) endspec برای جزئیات بیشتر در مورد مثال فوق و عملگرهای زبان LOTOS به ]17[ و برای مطالعه بیشتر در مورد زبان LOTOS به ]33[ الی ]34[ مراجعه کنید. VDM-SL VDM-SL[55] ابزاری برای توصیف مسائل نرم افزاری است که به صورت مجرد و مستقل از جزییات ماشین ابداع شده است. با توجه به اینکه VDM یک زبان بوده و دارای semantic فرمال می‌باشد، ابزای برای ارزیابی آن نیز ارایه شده است که می‌توان الگوریتم های مدل شده در این زبان را ارزیابی نمود. همچنین ابزاری برای اجرای سیستم مدل شده و مشاهده نتیجه تست برای آن پیش‌بینی شده تا کسانی که با VDM آشنایی ندارند بتوانند سیستم مورد نظر خود را بررسی کنند. با این حال این زبان قابلیت مدل سازی سیستم‌های موازی را ندارد. با توجه یه اینکه VDM یک زبان model-based است به طور کلی تفاوت بین این گروه از ابزار فرمال و متدهای جبری را می توان اینگونه توضیح داد که در گروه اول، ما عملیات در یک سیستم را بر اساس اینکه چه تأثیری بر مقادیر می گزارند توصیف می کنیم. در مقابل در ابزار جبری، خصوصیات عملیات را به صورت مجرد شرح می دهیم ]18[. با توجه به اینکه بیشترین توان VDM در مدل سازی سیستم های خطی است، به نظر می رسد این زبان بیشتر به توصیف خصوصیات کارکردی سیستم می پردازد. بنابراین بخش بزرگی از توصیف به بیان انواع داده‌ای ساده و مجرد و نیز ADT ها مربوط است. در چنین حالتی بسیاری از ساختار های عبارات جبری قابل نگاشت به این زبان هستند. در ادامه مدل ساده‌ای از VDM برای مدل سازی حساب بانکی آورده شده است ]18[: در این مثال مشتری با CustNum و حساب با AccNum مدل می شود. AccNum = token; CustNum = token; Balance = int; Overdraft = nat; AccData :: owner : CustNum balance : Balance state Bank of accountMap : map AccNum to AccData overdraftMap : map CustNum to Overdraft inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and a.balance >= -overdraftMap(a.owner) برای مطالعه بیشتر به ]35[ الی ]36[ مراجعه کنید. شبکه های پتری شبکه های پتری[56] یکی از قدیمیترین زبان های فرمال برای توصیف و ارزیابی سیستم ها است. از بارزترین خصوصیات این زبان می توان به توانایی آن برای توصیف سیستم های موازی اشاره نمود. همچنین به دلیل پختگی[57]، این زبان مکانیزم هایی برای بیان جنبه های کارکردی و رفتاری سیستم ارائه می نماید. همچنین علاوه بر توانایی توصیف سیستم ها، می تواند شیوه هایی برای تحلیل[58] و ارزیابی[59] و نیز در نهایت اثبات فرمال آنها[60] ارائه نماید ]19[ الی ]22[. بر اساس تعریف، یک شبکه پتری به صورت زیر به شکل فرمال تعریف می شود ]23[: مجموعه متناهی از موقعیت ها[61] مجموعه متناهی از گزارها[62] مجموعه ای از لبه های گراف[63] (روابط بین pها و tها) W: {1, 2, 3, …} تابع وزن گذاری روابط وضعیت اولیه سیستم. همچنین ضروری است : به عنوان مثال مدل ساده ای از یک پروتکل ارتباطی در شکل 2.5 نشان داده شده است. شکل 2.5. مثالی از مدل سازی یک پروتکل به کمک شبکه های پتری ]23[ در شکل بالا، وضعیت شروع = (1,0,0,1,0,0,0,0) می باشد که به معنی فعال بودن موقعیت های p1 و p4 است. بنابراین گزارهای t1 و t5 به ترتیب فعال[64] هستند. باید توجه داشت که فعال بودن یک گزار لزوما به معنی اجرا شدن[65] آن نیست بلکه اجرا شدن به رخ دادن اتفاق در سیستم واقعی بر می گردد. همچنین اجرا شدن t1 و t5 به ترتیب توکن های p1 و p4 را حذف کرده و توکن هایی به p2 و p5 اضافه می کند. خصوصیات رفتاری[66] با تعریف وضعیت شروع[67] به عنوان وضعیت اولیه سیستم ، خصوصیات رفتاری در واقع جنبه هایی از سیستم هستند که به این وضعیت شروع وابسته هستند و در موقعیت های اجرایی سیستم تغییر می کنند. در شبکه (N, M0) (شبکه پتری N با وضعیت شروع )، مجموعه تمام دنباله های گزارهای قابل اجرا که از وضعیت M0 شروع می شوند را با L(N, M0) و یا به شکل ساده تر با L(M0)[68] نشان می دهند. به کمک پارامترهای زیر می توان جنبه های رفتاری سیستم توصیف نمود ]23[ و ]24[: Reachability طبق تعریف، وضعیت سیستم در ، از وضعیت ، reachable خواهد بود اگر دنباله ای از اجرای گزارها[69] وجود داشته باشد که را به ببرد. مجموعه وضعیت های قابل دسترسی از طریق را با مجموعه نشان میدهیم. Boundedness شبکه پتری (N,)، k-bounded یا به اختصار bounded خواهد بود اگر تعداد توکن های موجود در هر place، برای همه وضعیت های قابل دستیابی از وضعیت شروع، از تعداد محدود k تجاوز نکند. به عبارت دیگر . همچنین یک شبکه پتری 1-bounded، شبکه پتری ایمن[70] نامیده می شود. Liveness این مفهوم در ارتباط نزدیک با مفهوم عدم وجود بن بست در سیستم عامل ها می باشد. شبکه پتری (N,)، live خوانده می شود (به عبارت دیگر وضعیت یک وضعیت live برای N شمرده می شود) اگر، بدون توجه به اینکه چه وضعیتی از پیش می آید، در نهایت اجرای تمام گزارهای شبکه با دنبال کردن دنباله ای از گزارها ممکن باشد. این بدان معنی است که یک شبکه پتری live عملیات بدون بن بست را تضمین می کند بدون اینکه ترتیب اجرای گزارها مهم باشد. به عنوان نمونه، شبکه شکل 2.6 دارای خصوصیت Liveness نمی باشد زیرا در صورتی که گزار t1 در ابتدا اجرا شود، دیگر هیچ یک از گزارها امکان اجرا شدن نخواهند داشت. شکل 2.6. نمونه ای از شبکه پتری non-Live ]23[ Liveness خصوصیتی ایده آل برای بسیاری از سیستم ها است. با این حال اثبات و فراهم کردن کامل این خصوصیت دشوار برای بسیاری از سیستم های پیچیده غیر ممکن و هزینه بر است. سیستم عامل کامپیوترهای بزرگ نمونه ای از چنین سیستم هایی است. بنابراین در عمل این خصوصیت نادیده گرفته شده و چندین سطح از Liveness برای شبکه ها در نظر گرفته می شود. بر این اساس سطح Liveness گزار t در شبکه پتری (N,) یکی از موارد زیر خواهد بود: Dead (L0-live) اگر t هیچ گاه و در هیچ یک از دنباله های اجرای L(M0) اجرا نشود. L1-live (probably fireable) اگر t حداقل یک بار و در یکی از دنباله های اجرای L(M0) بتواند اجرا شود. L2-live اگر با در نظر گرفتن عدد مثبت k، گزار t بتواند حداقل k بار در دنباله های اجرای مختلف L(M0) اجرا شود. L3-live اگر t به دفعات نامحدودی در تعدادی از دنباله های اجرای L(M0) ظاهر شود. L4-live (Live) اگر t در هر وضعیت M در R(M0) در مرتبه L1-live باشد. ■ گفته می شود شبکه پتری (N,)، Lk-live است اگر همه گزارهای موجود در شبکه حداقل از مرتبه Lk-live باشند و k=0,1,2,3,4. همچنین L4-liveness قویترین سطح live بودن سیستم و و معادل مفهومی است که در ابتدای بخش توضیح داده شد. به سادگی می توان دریافت که یک گزار یا شبکه که در سطح k، live است، لزوما در سطح k-1 نیز live خواهد بود. به عبارت دیگر رابطه دلالت بین آنها به این شکل برقرار است: L4-liveness => L3-liveness => L2-liveness => L1-liveness گفته می شود گه یک گزار دقیقا Lk-live است اگر این گزار Lk-live باشد ولی L(k+1)-live نباشد، K=1,2,3. Reversibility شبکه (N,)، reversible است اگر برای هر وضعیت M، از طریق M قابل دستیابی (reachable) باشد. Coverability در شبکه (N,) گفته می شود وضعیت M قابل پوشش است اگر وضعیت در وجود داشته باشد به طوری که . Home state وضعیت در شبکه (N,)، Home state نامیده می شود اگر برای هر وضعیت M در ، از M قابل دسترسی باشد. زیر مجموعه های شبکه های پتری تعریف: یک شبکه پتری، شبکه اولیه[71] نامیده می شود در صورتی که وزن تمام لبه های آن 1 باشد. با این تعریف در این بخش شبکه های اولیه ای را معرفی می کنیم که دارای خواص مشترکی هستند. البته باید توجه داشت که شبکه های اولیه و غیر اولیه هر دو دارای قدرت مدلسازی یکسانی هستند و تفاوت آنها در راحتی و سرعت استخراج و اثبات خصوصیات است. در این بخش از نشانه گذاری زیر به عنوان مقدمه استفاده می کنیم. در اینجا F مجموعه همه لبه های شبکه پتری است: •t= {p| (p,t) F} مجموعه موقعیت های ورودی به t t•= {p| (t,p) F} مجموعه موقعیت های خروجی از t •p= {t| (t,p)F} مجموعه گزارهای ورودی به p p•= {t| (p,t)F} مجموعه گزارهای خروجی از p مثال هایی از نشانه های گفته شده در شکل 2.7 نشان داده شده است. با این تعریف می توانیم زیر مجموعه های شبکه های پتری را با اعمال قوانینی در ساختار آنها مشخص کنیم. در این تحقیق فرض شده است که در هیچ یک از شبکه های مورد بحث، موقعیت یا گزار ایزوله وجود ندارد یعنی گزار یا موقعیتی با شرایط •p= p•= Ø یا •t= t•= Ø وجود ندارد. شکل 2.7. نشانه گزاری برای: a) مجموعه موقعیت های ورودی و خروجی برای t و b) مجموعه گزارهای ورودی و خروجی برای p ]23[ با مقدمه گفته شده، کلاس های زیر را برای شبکه های پتری داریم: State Machine (SM) یک شبکه پتری اولیه با این شرط که هر گزار t دقیقا یک موقعیت ورودی و یک موقعیت خروجی داشته باشد. یعنی: |•t| = |t•| = 1for all t T. Marked Graph (MG) یک شبکه پتری اولیه با این شرط که هر موقعیت p دقیقا یک گزار ورودی و یک گزار خروجی داشته باشد. یعنی: |•p| = |p•| = 1for all p P. Free-choice net (FC) یک شبکه پتری اولیه است که در آن هر لبه متصل به یک موقعیت، یا یک لبه خروجی یکتا از یک گزار و یا یک لبه ورودی یکتا به یک گزار است. یعنی: For all , |p•| 1 or •(p•) = {p} که معادل است با: For all Extended Free-choice net (EFC) یک شبکه پتری اولیه است که: for all Asymmetric choice net (AC) این کلاس که به عنوان شبکه ساده[72] هم شناخته می شود، یک شبکه پتری اولیه است که : for all . مثال هایی از کلاس های تشریح شده که تفاوت های کلیدی این زیر مجموعه های شبکه پتری را نشان می دهد در شکل 2.8 آمده است. شکل 2.8. مثال هایی از زیر مجموعه های شبکه های پتری ]23[ قضایا و فرضیات ]23[ با یادآوری این نکته که شبکه اولیه به شبکه ای گفته می شود که وزن همه لبه های آن 1 باشد، قضیه های زیر را داریم: قضیه 1: اگر شبکه پتری عادی (N, )، Live و Safe باشد، نباید در آن موقعیت source یا sink و نیز گزار source یا sink وجود داشته باشد یعنی: . □ با بسط دادن این قضیه می توان گفت اگر شبکه پتری متصل (N, )، live و safe باشد، آنگاه شبکه N یک شبکه متصل قوی[73] است. قضیه 2: اگر درخت پوشای شبکه پتری (N, ) را به عنوان T در نظر بگیریم، شبکه (N,)، Safe خواهد بود اگر و تنها اگر فقط مقادیر 0 و 1 در برچسب لبه های T وجود داشته باشد. □ قضیه 3: اگر درخت پوشای شبکه پتری (N, ) را به عنوان T در نظر بگیریم، گزار t یک بن بست[74] است اگر و تنها اگر t به عنوان برچسب یک لبه در T ظاهر نشود. □ قضیه 4: یک state machine، (N, )، live است اگر و تنها اگر این شبکه متصل قوی بوده و M0 حداقل یک توکن داشته باشد. □ قضیه 5: یک state machine، (N,)، safe است اگر و تنها اگر M0 حداکثر یک توکن داشته باشد. همچنین شرط لازم و کافی برای اینکه یک live state machine، (N, )، safe نیز باشد این است که M0 دقیقا یک توکن داشته باشد. □ در شبکه های marked graph، هر موقعیت دقیقا یک لبه ورودی و یک لبه خروجی با وزن واحد دارد. بنابراین گراف نشانه دار (N,) را می توان با گراف نشانه دار جهت دار[75] (G, ) نشان داد که در آن لبه ها معادل موقعیت ها و گره ها معادل گزارها هستند. شکل 2.9 مثالی از مدل پتری یک پروتکل ارتباطی در شبکه های کامپیوتری (الف) و گراف نشانه دار متناظر با آن (ب) را نشان می دهد. شکل 2.9. یک شبکه پتری و گراف نشانه دار مربوط به آن ]23[ اجرای یک گره (گزار) در یک marked graph شامل حذف شدن یک توکن از از لبه های ورودی (موقعیت های ورودی) و اضافه شدن یک توکن به لبه های خروجی (موقعیت های خروجی) می باشد. اگر یک گره بر روی یک مدار جهت دار[76] یا حلقه قرار داشته باشد، آنگاه دقیقا یکی از لبه های ورودی و یکی از لبه های خروجی آن متعلق به حلقه مذکور خواهد بود. متقابلا، اگر گره ای بر روی یک حلقه قرار نداشته باشد، هیچ یک از لبه های متصل به آن متعلق به مدار جهت دار مذکور نخواهد بود. با توجه به مقدمه گفته شده، قضایای زیر را در مورد خصوصیات نامتغیر[77] توکن ها در marked graph داریم: قضیه 6: در یک marked graph، تعداد توکن ها در یک مدار جهت دار تحت اجرای هر گزاری، نا متغیر است؛ یعنی برای هر مدار جهت دار C و هر وضعیت M در R(M0) داریم: M(C) = M0(C) که در اینجا M(C) نشان دهنده مجموع تعداد توکن ها در C است. □ بر اساس قضیه 6، اگر در وضعیت اولیه شبکه، توکنی در یک مدار جهت دار وجود نداشته باشد، این حلقه بدون توکن باقی خواهد ماند. بنابراین هیچ یک از گره ها (گزار) در آن امکان اجرا شدن نخواهند داشت. از سوی دیگر اگر یک گره هیچ گاه طی هیچ وضعیتی امکان اجرا شدن نداشته باشد (L0-live transition)، می توان با بررسی معکوس دنباله گزارها، مدار مستقیم بدون توکن را پیدا کرد. بر این اساس قضیه 7 را داریم: قضیه 7: گراف نشانه دار (G, )، live است اگر و تنها اگر در وضعیت M0، حداقل یک توکن در هریک از مدارهای جهت دار G وجود داشته باشد. □ قضیه 8: گراف نشانه دار live (G, )، safe خواهد بود اگر و تنها اگر هر لبه ای (موقعیت) در این گراف متعلق به مدار جهت دار C باشد به طوری که M0(C) = 1 . □ لم 1: با استفاده از گراف پوشای مدل پتری (N,M0) تعدادی از خصوصیات آن را می توان بررسی نمود. از آن جمله می توان به موارد زیر اشاره کرد: شبکه (N,M0) ، bounded و در نتیجه R(M0) متناهی است اگر و تنها اگر مقدار (تعداد بی نهایت توکن در یک موقعیت) در هیچ یک از برچسب های گره های گراف وجود نداشته باشد. شبکه (N,M0)، safe است اگر و تنها اگر فقط مقادیر 0 و 1 در برچسب گره های گراف دیده شود. گزار t در شبکه (N,M0) ، dead خواهد بود اگر و تنها اگر این گزار به صورت برچسب یک لبه در گراف پوشا ظاهر نشود. اگر وضعیت M از طریق M0 قابل دسترسی (reachable) باشد. آنگاه در گراف گره ای با برچسب وجود دارد به طوری که □ برای مطالعه بیشتر قضایا و فرضیات به ]25[ الی ]28[ مراجعه کنید. جمع بندی در فصل دو، با تکیه بر مطالعات انجام شده در زمینه ابزار توصیف فرمال سیستم ها، چهار ابزار مختلف را انتخاب و بررسی نمودیم. هر یک از این چهار ابزار، خواه مبنی بر ابزار ریاضی مانند گراف باشند و یا مبتنی بر روابط جبری، به طراح در به دست آوردن تصویری قابل درک از سیستم واقعی کمک می کنند. این تصویر می تواند با متد های قابل دفاع مورد بررسی و تحلیل قرار گرفته و ظرفیت ها و مشکلات سیستم را از جنبه های زیادی به طراح نشان دهد.  

 نکته مهم : هنگام انتقال متون از فایل ورد به داخل سایت بعضی از فرمول ها و اشکال (تصاویر) درج نمی شود یا به هم ریخته می شود یا به صورت کد نشان داده می شود ولی در سایت اصلی می توانید فایل اصلی را با فرمت ورد به صورت کاملا خوانا خریداری کنید: سایت مرجع پایان نامه ها (خرید و دانلود با امکان دانلود رایگان نمونه ها) : jahandoc.com   با توجه به تنوع سیستم های دنیای واقعی و خصوصیات بی شمار آنها، به طبع، ابزار فرمال متنوعی نیز برای بررسی آنها ابداع شده است. به عنوان نمونه بسیاری از ابزار مدلسازی فرمال قادر به نشان دادن دقیق خصوصیات سیستم های غیر موازی هستند. در مقابل بسیاری می توانند خصوصیات سیستم های موازی را که بسیار پیچیده ترند نشان دهند. همچنین خصوصیات ساختاری و رفتاری سیستم ها و نحوه برخورد آنها با زمان مسائل پیچیده ای است که باید در مدل سازی سیستم با ابزار فرمال مد نظر داشت. با توجه به توضیحات ارائه شده در بخش های گذشته، می توان جدول مقایسه ای برای چهار ابزار توصیف فرمال مذکور به صورت جدول 2.1 ارائه داد. جدول 2.1. خلاصه مقایسه ابزار توصیف فرمال ردیف خصوصیت ابزار توصیف فرمال ASM LOTOS VDM-SL Petri nets 1 پارادایم مبتنی بر جبر مبتنی بر جبر مبتنی بر مدل مبتنی بر مدل 2 سطح فرمالیتی فرمال فرمال فرمال فرمال 3 ابزار گرافیکی برای نمایش ندارد ندارد ندارد دارد 4 قابلیت توصیف سیستمهای موازی ندارد دارد ندارد دارد 5 قابلیت بیان[78] ضعیف ضعیف ضعیف قوی 6 قابلیت انتزاع پذیری متوسط متوسط متوسط قوی 7 پشتیبانی از شئی گرایی ندارد دارد ندارد دارد 8 قابلیت تبدیل به کد اجرایی دارد دارد دارد دارد 9 استفاده از متغیرها بله بله بله بله 10 قابلیت توصیف سیستم های غیر تعینی[79] ندارد دارد ندارد دارد 11 قابلیت اثبات پذیری دارد دارد دارد دارد 12 امکان بررسی مدل[80] ندارد ندارد دارد دارد با توجه به نتایج به دست آمده از مقایسه ابزار مذکور و ماهیت سیستم مورد بررسی، در این تحقیق از زبان شبکه های پتری برای مدل سازی فرمال سیستم استفاده خواهد شد. به همین دلیل در این فصل در مورد این ابزار تمرکز و بررسی بیشتری به کار رفته است. همچنین در پایان کلیه قضایا و فرضیاتی که در طول تحقیق از آنها بهره گرفته می شود آمده است. در فصل بعد به تشریح تکنولوژی مجازی سازی خواهیم پرداخت. این تکنولوژی برای ساخت لایه نرم افزاری دیتا سنتر به کار خواهد رفت. در نهایت در فصل چهار، مدل های فرمالی در چند لایه از دیتا سنتری که به کمک این تکنولوژی ساخته شده طراحی خواهیم کرد. فصل سوم: بررسی معماری دیتا سنترها در این بخش لازم است معماری زیر ساخت نرم افزاری دیتا سنترها را بررسی و تحلیل نمائیم. این تحلیل پیش نیاز ما در طراحی مدل فرمال این زیر ساخت خواهد بود. به این منظور، در ابتدا معماری نرم افزارهای مدیریت ماشین های مجازی تحت عنوان نرم افزارهای Hypervisor را بررسی و تشریح می نمائیم ]37[ و ]38[. در حال حاضر سه نرم افزار مطرح در این زمینه، بیشترین سهم بازار سیستم های مجازی سازی را در اختیار دارند. این سه محصول عبارتند از: Microsoft Hyper-V Xen VMware ESXi از دیدگاه های مختلفی می توان hypervisor ها را با یکدیگر مقایسه نمود. از آن جمله می توان به پیاده سازی سرویس مجازی سازی کامل[81] در مقابل مجازی سازی ضمنی[82] اشاره کرد. در حالت اول، سخت افزار به طور کامل شبیه سازی می گردد و انتزاع کاملی از آن برای ماشین های مجازی ایجاد می گردد. به این ترتیب سیستم های عامل میهمان[83] نیازی به اصلاح برای کار بر روی این ماشین مجازی نخواهند داشت. همچنین آنها و نرم افزارهای در حال اجرا بر روی آنها هیچ اطلاعی از وجود ماشین مجازی نخواهند داشت. در نتیجه پیاده سازی به شکل کامل امکان مهاجرت نرم افزارها و سیستم های عامل میهمان بین ماشین های فیزیکی را میسر می سازد. همچنین با ایزوله کردن نرم افزارها و سیستم عامل ها، امنیت هر یک از آنها در حد بالایی تامین خواهد شد. در عین حال این شکل از مجازی سازی مشکلات کاهش کارایی را نیز به دنبال دارد. زیرا hypervisor مجبور است تصویر کاملی از هر ماشین مجازی و سیستم عامل میهمان نصب شده بر روی آن را نگه دارد. به عنوان مثال حتی BIOS شبیه سازی می گردد. بنابراین منابع بیشتری صرف مدیریت و اجرای hypervisor خواهد شد. در مقابل، پیازی سازی مجازی سازی به شکل ضمنی اجازه دسترسی سیستم های عامل میهمان را به بخش هایی از منابع بدون شبیه سازی آنها فراهم می کند. در این حالت لازم است روی سیستم های عامل میهمان اصلاحاتی صورت گیرد تا امکان برقراری ارتباط با hypervisor را داشته باشند. در نتیجه آنها از وجود ماشین مجازی مطلع خواهند بود. این روش در کنار برخی از مشکلات امنیتی، عموما از سیستم های عامل closed-source پشتیبانی نمی کند زیرا امکان انجام اصلاحات لازم برای کار در ماشین مجازی در مورد آنها وجود ندارد ]39[. نرم افزارهای Hyper-V و Xen به صورت مجازی سازی ضمنی و ESX به صورت مجازی سازی مطلق پیاده سازی شده اند. در ادامه به بررسی معماری هر یک از این سه محصول می پردازم و در نهایت برای مدل سازی روابط بر روی VMware ESX متمرکز خواهیم شد. Microsoft Hyper-V توضیحات زیر از سایت رسمی اسناد فنی شرکت میکروسافت (MSDN) برداشت شده است ]40[. Hyper-V یک تکنولوژی مجازی سازی مبتنی بر Hypervisor است که برای Windows server 2008 نسخه 64 بیتی ساخته شده است. اولین مفهوم مطرح در این تکنولوژی نوعی از جدا سازی[84] به نام پارتیشن است. در واقع Hyper-V از این بخش های جدا شده برای نگهداری اطلاعات و اجرای سیستم عامل های مختلف استفاده می کند. وجود حداقل یک پارتیشن ضروری است که پارتیشن ریشه یا والد[85] نامیده می شود. در این پارتیشن یک سیستم عامل Windows server 2008 نصب و اجرا می گردد که وظیفه مدیریت دیگر سیستم عامل های مهمان و برقراری ارتباط آنها با سخت افزارهای فیزیکی را بر عهده دارد. پارتیشن ریشه تنها پارتیشنی است که دسترسی مستقیم به سخت افزار فیزیکی را دارد و از طریق رابط برنامه نویسی[86] hypercall سیستم عامل های میهمان را ایجاد می کند. سیستم عامل های میهمان با تصویری از پردازنده و وقفه ها[87] و در فضای محدودی از حافظه کار می کنند. در واقع hypervisor وقفه ها را برای سیستم عامل ترجمه کرده و به پارتیشن متناظر ارسال می کند. همچنین سیستم عامل ها (میهمان) به کمک ماژول VDev [88] با تصویری از سخت افزارهای جانبی کار می کنند که توسط hypervisor اجرا می شود. درخواست سیستم عامل از سخت افزار[89] مجازی توسط VMBus[90] که یک کانال ارتباطی منطقی بین پارتیشن ها است به hypervisor و یا پارتیشن ریشه منتقل می شود و از آنجا به سخت افزار واقعی انتقال می یابد. به عبارت دقیقتر، ماژول VSC[91] بر روی سیستم عامل میهمان درخواست خود را از طریق VMBus برای ماژول VSP[92] بر روی سیستم عامل میزبان در پارتیشن ریشه ارسال می نماید. همچنین می توان از امکان Enlightened I/O برای افزایش سرعت و کارایی دستیابی به سخت افزارهای جانبی مانند دیسک، رابط شبکه و غیره استفاده نمود. در واقع این تکنولوژی، پیاده سازی پروتکل های سطح بالا (مانند SCSI) است که برای استفاده در محیط مجازی آماده پیاده سازی پروتکل های سطح بالا (مانند SCSI) است که برای استفاده در محیط مجازی آماده شده اند[93]. این پروتکل ها با استفاده مستقیم از VMBus، لایه های میانی شبیه سازی[94] سخت افزارها و نیاز به راه اندازها[95] را از بین می برند. اما استفاده از این امکان به راه اندازی سرویس های مجتمع سازی[96] نیاز دارد که برای چند سیستم عامل مشخص موجود است. لیست سیستم های عاملی که توسط Hyper-V پشتیبانی می شوند در جدول 3.1 آورده شده است. جدول 3.1. سیستم های عامل قابل پشتیبانی توسط Hyper-V R2 ]42[ Guest OS Virtual processors Edition(s) Windows 71,2 or 4 Both x86-32 and x86-64, all editions except home editions Windows Server 2008 R21,2 or 4 Web, Standard, Enterprise, Datacenter Windows Server 20081,2 or 4 Both x86 and x64, Web, HPC, Standard, Enterprise, Datacenter, with or without Hyper-V Linux (only including SUSE Linux Enterprise Server 10 with SP3 or version 11 and Red Hat Linux versions 5.2-5.5) 1,2 or 4 Both x86 and x64 Windows Server 20031 or 2 Both x86 and x64, Standard, Enterprise, Datacenter, SP2 required Windows Server 2003 R21 or 2 Web, Standard, Enterprise, Datacenter, both x86 and x64 except for Web whose 64-bit version is not supported Windows Vista1 or 2 Both x86 and x64, all editions except home editionsOthers 1 N/A شمایی از معماری Hyper-V در شکل 3.1 آورده شده است. شکل 3.1. معماری سطح بالای Hyper-V ]40[ بررسی اجزاء معماری Hyper-V در ادامه به توضیح مختصری درباره بخش ها و اصطلاحات این معماری می پردازیم. APIC[97] ماژولی که امکان اولویت بندی وقفه ها را فراهم می سازد. Child Partition پارتیشنی که حاوی یک سیستم عامل میهمان است. تمام دسترسی های لازم به منابع فیزیکی سیستم مانند حافظه و وسایل جانبی توسط VMBus و hypervisor برای این پارتیشن فراهم می گردد. Hypercall رابطی برای ارتباط با hypervisor است که از طریق آن سیستم های عامل میهمان می توانند به ابزار بهینه hypervisot دست یابند. Hypervisor یک لایه نرم افزاری که مابین سخت افزار و یک یا چند سیستم عامل قرار می گیرد و وظیفه اصلی آن فراهم آوردن فضای مجزایی به نام پارتیشن برای اجرای هر یک از سیستم های عامل است. Hypervisor دسترسی به سخت افزار را کنترل و مدیریت می کند. IC[98] ماژولی است که امکان ارتباط سیستم های عامل میهمان را با یکدیگر و با hypervisor فراهم می آورد. I/O stack همان پشته ورودی و خروجی است. Root Partition پارتیشنی است که سیستم عامل آن وظایف مدیریتی در سطح ماشین را انجام می دهد که عبارتند از راه انداز سخت افزارهای جانبی، مدیریت انرژی مصرفی و اضافه و حذف کردن دستگاه های در حال کار. این پارتیشن تنها پارتیشنی است که دسترسی مستقیمی منابع فیزیکی سیستم دارد. VID[99] عملیاتی مانند سرویس های مدیریت پارتیشن ها، سرویس مدیریت پردازنده های مجازی، و سرویس مدیریت حافظه برای پارتیشن ها را ارائه می دهد. VMBus یک مکانیزم ارتباطی مبتنی بر کانال برای ارتباط پارتیشن ها و دستگاه ها فراهم می آورد. VMMS[100] مدیریت وضعیت همه ماشین های مجازی در پارتیشن های فرزند را بر عهده دارد. VMWP[101] یک بخش user mode در پشته مجازی سازی است. با این تعریف که پروسه ایجاد کننده[102] یک سرویس مدیریت ماشین ها مجازی در پارتیشن ریشه (windows server 2008) ایجاد می کند که به کمک آن می توان سیستم های عامل میهمان را مدیریت نمود، سرویس VMWP یک پروسه ایجاد کننده مجزا برای هر یک از پارتیشن های فرزند ایجاد می کند. VSC[103] یک ماژول ترکیبی که که در پارتیشن فرزند قرار می گیرد و نحوه استفاده از منابع سخت افزاری را که توسط سرویس دهنده مجازی (VSP) ارائه شده بهینه می نماید. VSC با VSP متناظر خود در پارتیشن ریشه از طریق VMBus ارتباط برقرار می کند تا به درخواست های I/O پارتیشن فرزند سرویس دهد. VSP[104] سرویسی که در پارتیشن ریشه قرار می گیرد و از درخواست های پارتیشن های فرزند که از طریق VMBus مطرح می شود پاسخ می دهد. WinHv[105] این ماژول پلی بین راه اندازهای سیستمهای عامل موجود در پارتیشن ها و hypervisor است که به راه اندازها امکان می هد تا از طریق رابط فراخوانی استاندارد ویندوز، hypervisor را صدا بزنند. WMI[106] ابزار مدیریت ویندوز مجموعه ای از API ها هستند که سرویس مدیریت ماشین های مجازی برای مدیریت و کنترل ماشین ها ارائه می دهد. نقاط ضعف در مجموع می توان گفت که Hyper-V زیر ساخت نسبتا سبکی برای پیاده سازی ساختار مجازی سازی است. در عین حال به دلیل نیاز به وجود بخشی از معمای در سیستم های عامل میهمان، اجرای آنها کاملا مستقل از hypervisor نخواهد بود. در عمل نیز می بینیم که Hyper-V از تعداد محدودی از سیستم های عامل به عنوان میهمان پشتیبانی می کند تعدادی از آنها در جدول 3.1 آمده است. همچنین نیاز به وجود یک سیستم عامل میزبان[107] هنوز هم وجود دارد. به این معنی که یک Windows server 2008 باید در پارتیشن ریشه نصب گردد تا بتواند درخواست های سیستم های عامل میهمان از سخت افزارهای مجازی را به سخت افزارهای فیزیکی منتقل نماید ]43[. برای مطالعه بیشتر در مورد Microsoft Hyper-V به ]44[ الی ]48[ مراجعه کنید. Xen در این بخش به تشریح کلیات معماری نرم افزار مجازی سازی Xen خواهیم پرداخت ]49[ و ]50[. این hypervisor معروفترین نرم افزار مجازی سازی با متن باز است که شرکت ها و سازمان های متعددی با بومی سازی از آن برای پیاده سازی زیر ساخت مجازی خود استفاده کرده اند. Xen به صورت یک مجازی ساز ضمنی پیاده سازی شده است بنابراین برای سیستم های عامل میهمان برای کار با آن نیاز به یک سری تغییراتی دارند. لیست سیستم های عاملی که توسط Xen 3.0 پشتیبانی می شوند در جدول 3.2 آورده شده است. جدول 3.2. سیستم های عامل قابل پشتیبانی توسط Xen نسخه 3 Operating Sys-- Runs as Dom0 (host os) Runs as DomU (guest os) Linux 2.6 Yes Yes NetBSD 3.1 No Yes NetBSD 4.0_BETA2 and -CURRENT Yes Yes FreeBSD 5.3 No currently broken? Actively being worked on FreeBSD 7-CURRENT no can be patched; works. Plan 9 No currently broken? ReactOS No planned, development stalled Solaris 10 Unknown Yes Un-Modified OS No Initial support for unmodified guests when using Intel VTX hardware, e.g. Windows این hypervisor از بخش های مختلفی تشکیل شده که در ادامه به تشریح آنها می پردازیم. همچنین شمایی کلی از آن در شکل 3.2 آمده است. شکل 3.2. شمایی از معماری Xen ]51[ بررسی اجزاء معماری Xen در این بخش اجزاء تشکیل دهنده معماری Xen که به طور شماتیک در شکل 3.2 آمده است را بیشتر بررسی می کنیم. Xen Hypervisor این بخش اولین لایه مجرد نرم افزار مجازی سازی است که مستقیما بر روی سخت افزار و زیر همه سیستم های عامل قرار گرفته است. Xen Hypervisor مسئول زمان بندی پردازنده و مدیریت حافظه برای ماشین های مجازی است که روی آن در حال اجرا هستند. همچنین این بخش هیچ گونه درکی از پروتکل های شبکه، دستگاه های ذخیره سازی خارجی، ویدئو و دیگر ورودی/ خروجی های استاندارد ماشین ندارد.