بخشی از پاورپوینت
اسلاید 1 :
درستی یابی سیستم های واکنشی
مقدمه ای بر زبان مدلسازی
اسلاید 2 :
فهرست
مقدمه
تاریخچه
ساختار
ابزار
مثال
تبدیل به TS
اسلاید 3 :
زبانی جهت توصیف ساختار که ابزارهای گوناگونی بر پایه آن بنا شده است
بر پایه منطق مرتبه اول
بر پایه Z notation
بر پایه حساب رابطه ای Tarski
مدلسازی تدریجی و تکاملی
تبدیل منطق مرتبه اول به عبارات منطقی بزرگ
آنالیز توسط حل کننده های SAT
زبانی اعلانی است که می تواند نتایج رفتار را بدون دانستن مکانیزم ساختار شرح دهد.
شبیه به زبان های شی گرا می باشد و منطق های ارث بری را در خود دارد.
اسلاید 4 :
کاربرد های Alloy :
طراحی سوئیچینگ در شبکه های مخابرات
یافتن حفره های امنیتی
بیان محدودیت های رفتاری و ساختاری پیچیده
زمان بندی
رمز نگاری
ارتباطات
اسلاید 5 :
نسخه اولیه محدود به مدل کردن Object ها بود ، که به تدریج به یک زبان مدلسازی ساختاری کامل تبدیل شد.
طراحی زبان Alloy توسط گروه طراحی نرم افزار دانشگاه MIT به رهبری Daniel Jackson در سال 1997 صورت گرفت .
اسلاید 6 :
مولفه های اصلی
Signature
Functions
Predicates
Fact
Relation
Assertions
اسلاید 7 :
Signature
یک مجموعه در این زبان تعریف می کند ، مجموعه در واقع نود اصلی داده در این زبان است . برای تعریف مجوعه از syntax زیر استفاده می کنیم:
Sig نام داده {}
می تواند مجموعه ای از مجموعه دیگر خواص را به ارث ببرد.
ارث بری در مدل کردن کامپوننت های نرم افزاری که با روش Object Oriented طراحی می شود ، کاربرد فراوانی دارد .
می توان به مجموعه ها فیلد های توصیفی از قبیل:
دقیقا یک فیلد ( بدون هیچ کلمه خاصی یا با عبارت lone )
Sig نام داده { نام فیلد : نوع داده } Sig نام داده { نام فیلد : lone نوع داده }
اسلاید 8 :
یک یا صفر فیلد (با استفاده از کلمه کلیدی option)
Sig نام داده { نام فیلد : option نوع داده }
و یا تعداد دلخواهی از فیلدی ( با کلمه کلیدی set )
Sig نام داده { نام فیلد : set نوع داده }
اسلاید 9 :
به طور مثال :
abstract sig Person {
father: lone Man,
mother: lone Woman}
sig Man extends Person {
wife: lone Woman}
sig Woman extends Person {
husband: lone Man}
اسلاید 10 :
همچنین می توان از عملگرهای مجموعه ای بین مجموعه ها و نودهای اصلی استفاده کرد .
اسلاید 11 :
Fact
به بیان حقایق در رابطه با مدلسازی می پردازد ، در واقع حقایق به محدودیت ها و قیودی که می توانیم در مدلسازی به کار ببریم می پردازد. ساختار کلی به شرح زیر بوده :
fact [name]
{
[list of constraints]
[multiple constraints are implicitly conjoined]
}
اسلاید 12 :
به طور مثال این حقیقت این محدودیت را برای مدل مذکور عنوان می دارد که هیچ شخصی نمی تواند اجداد خودش باشد .این قبیل محدودیت ها و قیود و شرط ها را تحت عنوان fact معرفی می کنیم.
fact {
no p: Person |
p in p.^(mother + father)
}
اسلاید 13 :
Relation
رابطه بین دومجموعه را عنوان می کند. برای هر کدام از طرفین رابطه می توان تعداد شرکت در نظر گرفت تا مشخص شود رابطه چند به چند است .
C: person n->m person
رابطه بین person , person که m , n نشان دهنده ی تعداد شرکت کننده های طرفین رابطه هستند. می توان از علامت های زیر به جای m , n استفاده کرد .
“؟ “ صفر یا یک
“ ! “دقیقا یک
“ + “یک یا بیشتر
چنانچه علامتی قرار نگیرد ، محدودیتی روی تعداد قرار نمی گیرد.
اسلاید 14 :
Quantifier
به منظور ارتقای منطق گزاره ای به منطق مرتبه اول به کار می رود ، صورهای رایج عبارتند از :
اسلاید 15 :
ابزار اصلی که برای طراحی این مدل استفاده می گردد alloy نام دارد که هم اکنون نسخه 4.2 آن ، به روز ترین و آخرین نسخه موجود است.
Alloy4.2.jar
اسلاید 16 :
Forge
چارچوبی است برای تجزیه و تحلیل برنامه ها
Squander
چارچوبی برای اجرای یکنواخت و واحدی از برنامه های اعلانی و غیراعلانی
Alloy4Eclipse
پلاگین Eclipse برای Alloy
DynAlloy
یک اجرا از Alloy برای کارهای رویه ای
Equals Checker
ابزاری برای چک کردن صحت متدها در جاوا
Margrave
تجزیه و تحلیل خط مشی امنیتی برای فایروال
Secrecy Modeling Language (SML)
زبانی برای ایجاد و اعتبار سنجی مدل های امنیتی
اسلاید 17 :
sig Name {}
sig Addr {}
sig Book {
names : Name,
addrs : Addr,
entries : names -> lone Addr
}
pred show {
#Book.entries > 1
}
pred add[b, b' : Book, n : Name, a : Addr] {
a not in b.addrs
a in b'.addrs
n not in b.names
n in b'.names
b'.entries = b.entries + (n -> a)
}
pred del[b, b' : Book, n : Name, a : Addr] {
b'.entries = b.entries - (n -> a)
}
assert delUndoesAdd {
all b, b', b'' : Book, n : Name, a : Addr |
(no b.entries and add[b,b',n,a] and del[b',b'',n,a])
implies
(b.entries = b''.entries)
}
pred show() {}
run show {}
اسلاید 18 :
هر مثال متشکل از ساختار اصلی A = (Sigs, Facts, Preds) می باشد.
به طور کلی یک TS را مجموعه ای از (q,a,q’) در نظر می گیریم که از حالت q شروع شده و طبق واکنش a به حالت q’ می رود. و همچنین می بایست عناصر شروع کننده یک TS را مشخص کرد .
در ادامه برای مثال فوق حالات زیر را تعریف می کنیم :
اسلاید 19 :
در ادامه باید حالات شروع را مشخص کنیم :
