چکیده

روش های رسمی مبتنی بر ریاضیات هستند و با هدف قابلیت اثبات ویژگی های رفتاری سیستم های مختلف ایجاد شده اند. زبان های رسمی مختلفی وجود دارند که هر کدام از آ ن ها برای اثبات برخی ویژگی های محدود و یا سیستم های خاصی ایجاد شده اند. اغلب روش های رسمی قابلیت تعمیم پایینی برای استفاده در حوزه های متنوع دارند. شبکه پتری رنگی سلسله مراتبی توسعه ای از شبکه پتری سنتی است که قابلیت مدل سازی آن به طرز چشمگیری توسعه یافته است. این روش رسمی برای مدل سازی و بررسی ویژگی های رفتاری سیستم های همروند در مرحله طراحی ابداع شده است. شبکه پتری رنگی دارای واسط گرافیکی ساده بوده و از زبان هوش مصنوعی ML استفاده می کند و مبتنی بر تئوری کیسه است و یکی از روش های رسمی پرکاربرد محسوب می شود که قابلیت بسیار زیادی در مدل سازی انواع سیستم های توزیعی و همروند دارد. در شبکه پتری رنگی، مدل ایجاد شده برای اثبات ویژگی های رفتاری سیستم با انجام تغییرات جزئی، قابلیت استفاده برای شبیه سازی و استخراج معیارهای کارآیی سیستم را هم دارد. بدین ترتیب با ایجاد یک مدل، ابتدا صحت ویژگی های رفتاری سیستم اثبات شده و سپس معیارهای کمی کارآیی سیستم با همان مدل قابل استخراج است.
در این کارگاه مد نظر است که ابتدا شبکه پتری کلاسیک و مبنای ریاضی آن بطور اجمالی معرفی شود. سپس شبکه پتری رنگی معرفی خواهد شد و بطور اجمالی زبان هوش مصنوعی ML معرفی خواهد شد. در ادامه یک سیستم نمونه با استفاده از ابزار متن باز CPN Tools با شبکه پتری رنگی سلسله مراتبی مدل سازی و اجرا شده و فضای حالت آن استخراج خواهد شد. سپس ضمن معرفی گرامر زبان های پرس و جو از فضای حالت LTL و CTL چند ویژگی رفتاری مورد نظر با این زبان ها فرموله خواهند شد. سپس این ویژگی ها با جستجو در گراف فضای حالت اثبات خواهند شد. در انتها نحوه شبیه سازی سیستم با استفاده از مدل توسعه یافته و استخراج معیارهای کارآیی سیستم نمایش داده خواهد شد.
اهمیت موضوع
اکثر دانشجویان کارشناسی ارشد فناوری اطلاعات یا نرم افزار، سیستم ها، الگوریتم ها یا پروتکل های توزیعی جدیدی ارائه می دهند یا تغییراتی روی روش های موجود انجام می دهند ولی قابلیت اثبات وجود یا عدم وجود ویژگی های رفتاری سیستم را ندارند. بسیاری از پروتکل های موجود بر روی شبکه های حس گر بی سیم یا شبکه های موردی بدون اثبات صحت ویژگی های رفتاری ارائه شده اند. به عنوان نمونه می توان به ویژگی های رفتاری عدم وجود بن بست، عدم بروز وضعیت ناخواسته خاصی در یک سیستم، صحت و امن بودن اشاره کرد. در صورت نا امن بودن سیستم و وجود حفره امنیتی می توان با تحلیل فضای حالت سیستم بطور خودکار سناریوی حمله به سیستم را استخراج کرد.
دانشجویان معمولاً در سطح کارشناسی و کارشناسی ارشد هیچ درسی در رابطه با افزایش توانایی آن ها در رابطه با اثبات صحت سیستم های طراحی شده سپری نمی کنند. آن ها ناچاراً به شبیه سازی سیستم و استخراج برخی ویژگی های کمی کارآیی بسنده می کنند. هدف این کارگاه آشنا کردن مهندسین با یکی از کارآمدترین روش های رسمی، ابزارهای موجود و زبان های جستجوی فضای حالت است. همچنین نمایش داده خواهد شدکه چگونه با استفاده از این روش امکان شبیه سازی سیستم با استفاده از مدل ایجاد شده برای اثبات صحت سیستم میسر است.

زمان و تاریخ : ساعت 14 الی 18 شانزدهم شهریورماه 1395