منبع پایان نامه درباره مدل سازی

دانلود پایان نامه

hannel [ le1, le2, , re1, re2 ] : exit := . . . (*As defined previously *)
endspec

برای جزئیات بیشتر در مورد مثال فوق و عملگرهای زبان LOTOS به ]17[ و برای مطالعه بیشتر در مورد زبان LOTOS به ]33[ الی ]34[ مراجعه کنید.

VDM-SL

VDM-SL55 ابزاری برای توصیف مسائل نرم افزاری است که به صورت مجرد و مستقل از جزییات ماشین ابداع شده است. با توجه به اینکه 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[:

P={p_1, p_2, …, p_m}
مجموعه متناهی از موقعیت ها61
T={t_1, t_2, …, t_n}
مجموعه متناهی از گزارها62

F⊆(P×T)∪(T×P)
مجموعه ای از لبه های گراف63 (روابط بین pها و tها)
W: → {1, 2, 3, …}
تابع وزن گذاری روابط
M_0:P →{0, 1, 2, …}
وضعیت اولیه سیستم.
همچنین ضروری است :
P∩T=∅ and P∪T≠∅

به عنوان مثال مدل ساده ای از یک پروتکل ارتباطی در شکل 2.5 نشان داده شده است.

شکل 2.5. مثالی از مدل سازی یک پروتکل به کمک شبکه های پتری ]23[

در شکل بالا، وضعیت شروع M_0= (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 با وضعیت شروع M_0)، مجموعه تمام دنباله های گزارهای قابل اجرا که از وضعیت M0 شروع می شوند را با L(N, M0) و یا به شکل ساده تر با L(M0)68 نشان می دهند.
به کمک پارامترهای زیر می توان جنبه های رفتاری سیستم توصیف نمود ]23[ و ]24[:

Reachability
طبق تعریف، وضعیت سیستم در M_n ، از وضعیت M_0 ، reachable خواهد بود اگر دنباله ای از اجرای گزارها69 وجود داشته باشد که M_0 را به M_n ببرد.
مجموعه وضعیت های قابل دسترسی از طریق M_0 را با مجموعه R (M_0 ) نشان میدهیم.

Boundedness
شبکه پتری (N, M_0)، k-bounded یا به اختصار bounded خواهد بود اگر تعداد توکن های موجود در هر place، برای همه وضعیت های قابل دستیابی از وضعیت شروع، از تعداد محدود k تجاوز نکند. به عبارت دیگر M (p)≤k.
همچنین یک شبکه پتری 1-bounded، شبکه پتری ایمن70 نامیده می شود.

Liveness
این مفهوم در ارتباط نزدیک با مفهوم عدم وجود بن بست در سیستم عامل ها می باشد. شبکه پتری (N, M_0)، live خوانده می شود (به عبارت دیگر وضعیت M_0 یک وضعیت live برای N شمرده می شود) اگر، بدون توجه به اینکه چه وضعیتی از M_0 پیش می آید، در نهایت اجرای تمام گزارهای شبکه با دنبال کردن دنباله ای از گزارها ممکن باشد.
این بدان معنی است که یک شبکه پتری live عملیات بدون بن بست را تضمین می کند بدون اینکه ترتیب اجرای گزارها مهم باشد. به عنوان نمونه، شبکه شکل 2.6 دارای خصوصیت Liveness نمی باشد زیرا در صورتی که گزار t1 در ابتدا اجرا شود، دیگر هیچ یک از گزارها امکان اجرا شدن نخواهند داشت.

شکل 2.6. نمونه ای از شبکه پتری non-Live ]23[

Liveness خصوصیتی ایده آل برای بسیاری از سیستم ها است. با این حال اثبات و فراهم کردن کامل این خصوصیت دشوار برای بسیاری از سیستم های پیچیده غیر ممکن و هزینه بر است. سیستم عامل کامپیوترهای بزرگ نمونه ای از چنین سیستم هایی است. بنابراین در عمل این خصوصیت نادیده گرفته شده و چندین سطح از Liveness برای شبکه ها در نظر گرفته می شود. بر این اساس سطح Liveness گزار t در شبکه پتری (N, M_0) یکی از موارد زیر خواهد بود:
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, M_0)، 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, M_0)، reversible است اگر برای هر وضعیت M، M_0 از طریق M قابل دستیابی (reachable) باشد.

Coverability
در شبکه (N, M_0) گفته می شود وضعیت M قابل پوشش است اگر وضعیت M^’ در R(M_0 ) وجود داشته باشد به طوری که M^’ (p)≥M(p).

Home state
وضعیت M^’ در شبکه (N, M_0)، Home state نامیده می شود اگر برای هر وضعیت M در R(M_0 )، 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•| = 1 for all t T.

Marked Graph (MG)
یک شبکه پتری اولیه با این شرط که هر موقعیت p دقیقا یک گزار ورودی و یک گزار خروجی داشته باشد. یعنی:
|•p| = |p•| = 1 for all p P.

Free-choice net (FC)
یک شبکه پتری اولیه است که در آن هر لبه متصل به یک موقعیت، یا یک لبه خروجی یکتا از یک گزار و یا یک لبه ورودی یکتا به یک گزار است. یعنی:
For all p∈P, |p•| ≤1 or •(p•) = {p}
که معادل است با:
For all p_1, p_2 ϵP, p_1•∩p_2•≠∅=|p_1•|=|p_2•|=1

Extended Free-choice net (EFC)
یک شبکه پتری اولیه است که:
p_1•∩p_2•≠∅= p_1•=p_2• for all p_1, p_2∈P

Asymmetric choice net (AC)
این کلاس که به عنوان شبکه ساده72 هم شناخته می شود، یک شبکه پتری اولیه است که :
p_1•∩p_2•≠∅= p_1•⊆p_2•or p_2•⊆p_1• for all p_1, p_2∈P.

مثال هایی از کلاس های تشریح شده که تفاوت های کلیدی این زیر مجموعه های شبکه پتری را نشان می دهد در شکل 2.8 آمده است.

شکل 2.8. مثال هایی از زیر مجموعه های شبکه های پتری ]23[

قضایا و فرضیات ]23[
با یادآوری این نکته که شبکه اولیه به شبکه ای گفته می شود که وزن همه لبه های آن 1 باشد، قضیه های زیر را داریم:
قضیه 1: اگر شبکه پتری عادی (N, M_0)، Live و Safe باشد، نباید در آن موقعیت source یا sink و نیز گزار source یا sink وجود داشته باشد یعنی: x∈P∪T, •x≠Ø≠x•.

با بسط دادن این قضیه می توان گفت اگر شبکه پتری متصل (N, M_0)، live و safe باشد، آنگاه شبکه N یک شبکه متصل قوی73 است.
قضیه 2: اگر درخت پوشای شبکه پتری (N, M_0) را به عنوان T در نظر بگیریم، شبکه (N,M_0)، Safe خواهد بود اگر و تنها اگر فقط مقادیر 0 و 1 در برچسب لبه های T وجود داشته باشد.

قضیه 3: اگر درخت پوشای شبکه پتری (N, M_0) را به عنوان T در نظر بگیریم، گزار t یک بن بست74 است اگر و تنها اگر t به عنوان برچسب یک لبه در T ظاهر نشود.

قضیه 4: یک state machine، (N, M_0)، live است اگر و تنها اگر این شبکه متصل قوی بوده
و M0 حداقل یک توکن داشته باشد.

Author: mitra4--javid

دیدگاهتان را بنویسید

نشانی ایمیل شما منتشر نخواهد شد. بخش‌های موردنیاز علامت‌گذاری شده‌اند *