مدلسازی و اثبات ویژگی های رفتاری سیستم ها با استفاده از شبکه پتری رنگی سلسله مراتبی

چکیده

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

 

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

1395/06/16 تا 1395/06/16

دکتر سعید پاشازاده(دانشیار دانشکده مهندسی برق و کامپیوتر دانشگاه تبریز)

دانشکده مهندسی، دانشگاه بوعلی سینا

500000 ریال

30

1395/06/05

ثبت نام در این کارگاه

پروتکل های امنیتی شبکه

با گسترش اینترنت و سایر شبکه ها ، تعداد زیادی پروتکل امنیتی برای فراهم کردن ارتباط امن گسترش پیدا کرده اند . تحلیل جنبه های گوناگون این پروتکل ها بصورت دستی و با بکارگیری روش های سنتی برای انسان سخت می باشد. ضمنا ضعفهای امنیتی بسیاری از قراردادها پس از پس از پیاده سازی کشف شده اند. با این وجود هنوز راهی برای ایجاد صحیح و موثر پروتکل ها به طور مستقیم و از همان ابتدای طراحی وجود ندارد. بهترین راهکار موجود تحلیل این پروتکل ها با ابزار ها ی خودکار می باشد. در این کارگاه ابزاری به نام Scyther برای تحلیل و تحقیق پروتکل های امنیتی معرفی می گردد . این ابزار علاوه بر رایگان بودن دارای ویژگی هایی می باشد که در بسیاری از ابزار های تحلیل خودکار پشتیبانی نمی گردد. از عمده این ویژگی ها می توان تحلیل نامحدود با تضمین پایان، امکان آنالیز چندین پروتکل همزمان، و امکان آنالیز تکرار های نامحدود در الگوها، تحلیل پروتکل ها بر اساس یک الگوریتم الگوی پالودگی را نام برد.
تحلیل حملات و رفتار پروتکل در وضعیت تعداد نامحدود جلسه بر خلاف ابزار های مشابه کمک می کند .
 

 

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

1395/06/16 تا 1395/06/16

دکتر یونس سیفی، مهندس محمد پیشدار، مهندس نرگس رضائی( دانشگاه بوعلی سینا)

دانشکده مهندسی، دانشگاه بوعلی سینا

500000 ریال

30

1395/06/05

ثبت نام در این کارگاه

راه اندازی بستر آزمایشی جهت ارزیابی شبکه های بی سیم محلی با تمرکز بر ارتباطات چند رسان ای

با گسترش روزافزون ارتباطات اینترنتی که اغلب نیز توسط تلفن های هوشمند و سایر وسایل ارتباطی همراه با اتصال به شبکه های محلی بی سیم صورت می گیرد، فرآهم سازی کیفیت سرویس در این شبکه ها اهمیت ویژه ای پیدا کرده است.
در اغلب کارهای تحقیقاتی در این حوزه که با هدف بهبود کیفیت سرویس در این شبکه ها ارائه می گردند، از شبیه سازی به عنوان ابزاری جهت تایید عملکرد ادعای مطرح شده استفاده می شود. حال آنکه ویژگی های رسانه ی بی سیم از جمله وجود نویز های متنوع، تداخل امواج، نوسانات شرایط کانال، پدیده ی محوشدگی و ... نمی تواند به طور دقیق و مطابق با دنیای واقعی مدلسازی و شبیه سازی شود. به همین دلیل، در این کارگاه، قصد داریم مولفه های لازم برای راه اندازی یک بستر آزمایشی منطبق با استانداردهای IEEE 802.11 در هسته لینوکس را به همراه ملزومات آن معرفی نماییم.
عناوین و محورهای اصلی این کارگاه به صورت زیر خواهند بود:
- معرفی ساختار ماژول های شبکه محلی بی سیم در هسته لینوکس
- معرفی ساختار درایورهای متن باز در این حوزه، به ویژه درایور معروف ath9k
- انجام چند آزمایش عملی به منظور آشنایی با واسط شبکه بی سیم و قابلیت های آن
- معرفی و نحوه پیکربندی ابزارهای لازم برای راه اندازی بستر آزمایشی شبکه های محلی بی سیم در یک آزمایشگاه تحقیقاتی (iw، backports، hostapd، hwsim و ...)
- معرفی ابزارهای تولید ترافیک و استخراج نتایج ارزیابی (D-ITG، Iperf، EvalVid، TCPReplay و ...)
- معرفی اجمالی اسکریپت های نمونه جهت خودکارسازی فرآیند اجرای سناریوهای ارزیابی
 

 

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

 

1395/06/16 تا 1395/06/16

دکتر محمد نصیری، مهندس محمد حسن داعی( دانشگاه بوعلی سینا)، دکتر سید وحید ازهری( دانشگاه علم و صنعت ایران)

دانشکده مهندسی، دانشگاه بوعلی سینا

500000 ریال

30

1395/06/05

ثبت نام در این کارگاه

گارگاه پردازش زبان طبیعی و متن‌کاوی

هدف نخست این کارگاه آشنایی شرکت کنندگان با مفاهیم پایه‌ای موجود در حوزه پردازش زبان طبیعی و متن‌کاوی و تبیین جایگاه این حوزه از دانش در تحقیقات و مطالعات است. همچنین در نظر گرفته شده است تا شرکت کنندگان در این گارگاه با کاربردهای این حوزه از دانش و پیاده‌سازی‌های انجام شده نیز آشنا شوند. لازم به ذکر است که شرکت در این کارگاه نیازمند دانش بالا در این حوزه نیست. شرکت کنندگان تنها لازم است تا آشنایی سطحی با مفاهیم این حوزه و دانش جزیی در زمینه برنامه‌‌نویسی داشته باشند.
سرفصل‌های این کارگاه عبارتند از:
• آشنایی مقدماتی با مفاهیم موجود در حوزه پردازش زبان طبیعی.
• آشنایی با روش‌های موجود جهت استخراج ویژگی از اسناد متنی.
• آشنایی با مفهوم دانش ساخت یافته در این حوزه.
• آشنایی مقدماتی با سیستم‌های متن‌کاوی و مفاهیم آن‌ها.
• آشنایی با ابزارهای موجود در زمینه پردازش زبان طبیعی و متن‌کاوی.
• آشنایی با نمونه عملیاتی یک سیستم پیاده‌سازی شده در این حوزه.
 

 

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

1395/06/16 تا 1395/06/16

مهندس مرتضی جادریان( دانشجوی دکترا، دانشگاه بوعلی سینا)

دانشکده مهندسی، دانشگاه بوعلی سینا

500000 ریال

30

1395/06/05

ثبت نام در این کارگاه

مفهوم IOT، مزایا، چالش‌ها و تاثیر IOT بر فضای کسب و کار

کارگاه حاضر به بررسی اینترنت اشیاء از دیدگاه کسب‌وکار و با تمرکز بر جنبه‌های نظری و علمی می‌پردازد. با توجه به اهمیت تأثیرات اینترنت اشیاء بر ظهور کسب‌وکارهای جدید و تحول در کسب‌وکارهای موجود شناخت جنبه‌های نظری و علمی مرتبط با این حوزه از اولویت بالایی برخوردار است. ازاین‌رو این کارگاه در چند بخش اصلی برنامه‌ریزی‌شده است. در ابتدا اکوسیستم کسب‌وکارهای اینترنت اشیاء باهدف شناختن نقش‌های این اکوسیستم معرفی می‌شود، سپس به بررسی تأثیر اینترنت اشیاء بر اجزای مدل کسب‌وکار شرکت‌ها و سپس گونه شناسی مدل‌های کسب‌وکار اینترنت اشیاء پرداخته خواهد شد. در ادامه تعدادی از کسب‌وکارهای نوپا(استارتاپ) در حوزه اینترنت اشیاء معرفی می‌گردد. آنگاه مهم‌ترین پلتفرم‌های این حوزه به‌عنوان یک مدل کسب‌وکار غالب تشریح گردیده و نهایت با توجه به رویکرد پروژه در حال انجام، که متمرکز بر کسب‌وکارهای مبتنی بر موبایل در حوزه بهداشت و سلامت و یا صنعت است، مدل‌های کسب‌وکار این حوزه نیز موردمطالعه و بررسی قرار می‌گیرد.

 

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

 

1395/06/16 تا 1395/06/16

مهندس محمد حسین همائی اکبرپور(شرکت فناوران شبکه حسگر بی سیم و آزمایشگاه تخصصی اینترنت اشیا)

دانشکده مهندسی، دانشگاه بوعلی سینا

500000 ریال

30

1395/06/05

ثبت نام در این کارگاه

کارگاه آموزشی مقاله نویسی علمی- پژوهشی (فنی و مهندسی)

با حمایت مرکز اطلاعات علمی جهاد دانشگاهی (SID)

 سرفصل مباحث:
• انتخاب مجله علمی مناسب
• ساختار مقالات کامل پژوهشی
• ویژگی های مقالات خوب
• عنوان، مولفان، چکیده و کلیدواژه ها
• مقدمه و توضیح نوآوری
• آزمایشهای عملی/شبیه سازی
• شکل ها و جدول ها
• بحث و نتیجه گیری
• نحوه ارجاع و مرجع نویسی
• اقدامات لازم پیش از ارسال مقاله و پیگیری آن
• ارتباط و پاسخگویی به سردبیر مجله و داوران مقاله
• رعایت اخلاق پژوهشی در مقاله نویسی

 

این کارگاه با حمایت مرکز اطلاعات علمی جهاد دانشگاهی (SID) برگزار می گردد.

 

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

 

 

1395/06/16 تا 1395/06/16

دکتر حمیدرضا صادق محمدی (سردبیر نشریه مهندسی برق و مهندسی کامپیوتر ایران)

دانشکده مهندسی، دانشگاه بوعلی سینا

500000 ریال

30

1395/06/05

ثبت نام در این کارگاه