مدل سازی اسانسور با promela language در محیط ispin
پنج سال پیش منتشر شده
تعداد بازدید: 665
کد پروژه: 83900
شرح پروژه
پروژه دو قسمت داره که قسمت دوم ادامه قسمت اول هست. تو قسمت اول یک سیستم اسانسور هست که میخوایم مدلش رو با یک سری ویژگی ها که ما براش تعریف میکنیم بسازیم. اسانسور دو طبقه داره که هر طبقه یک request button داره که user دکمه رو میزنه تا اسانسور بیاد به اون طبقه و در رو براش باز کنه. داخل اسانسور هم یک request button وجود داره برای هر دو طبقه که user فشار میده دکمه رو تا اسانسور به اون طبقه مورد نظر بره و در رو باز کنه. اسانسور باید وقتی بین طبقه ها حرکت میکنه ، این کار رو تو one time unit انجام بده. و وقتی در اسانسور باز شد فقط باید برای one time unit باز بمونه. حالا میخواد که behavior سیستم اسانسور رو با زبان Promela input language تو spin model checker که سافت ور هست بنویسیم که مدل رو verify کنه برامون. علاوه بر این باید این properties ها رو هم داشته باشه مدل که با LTL formula باید بنویسیم. ۱.اگه user اسانسور رو call کرد eventually باید انجام شه. ۲.درخواست مقصد( destination request) از داخل اسانسور eventually انجام شه. ۳.اسانسور هرگز حرکت نکنه وقتی درش باز هست. این قسمت اول هست که باید این ۳ تا properties با LTL formula نوشته بشن. و بعد با زبان promela تو spin نوشته شن تا مدل verify و تست بشه. قسمت دوم مثل قسمت اول ولی پیچیده تر هست. این اسانسور openDoor button داره به اضافه ی دکمه های قبلی. که اگر وقتی اسانسور در حال حرکت نیست ، این دکمه فشار داده بشه در رو باز نگه میداره برای one extra time unit. با این حال user نمیتونه در رو باز نگه داره به طور نامحدود اگر اسانسور request دیگه ای داره برای سرویس انجام دادن. توی این قسمت دوم ما ۴ طبقه داریم که هر طبقه مثل دفعه قبل one time unit زمان میبرن برای حرکت بین طبقه ها. تو این قسمت هم باید یه سری properties ها با LTL نوشته بشن. ۱.اسانسور eventually باید سرویس رو انجام بده وقتی call میشه حتی اگر openDoor فشار داده بشه. ۲.دکمه مقصد داخل اسانسور باید سرویس رو انجام بده حتی اگه دکمه openDoor فشار داده شده باشه. ۳.اسانسور هرگز با در باز حرکت نمیکنه. ۴.سانسور در رو باز نگه میداره تا زمانی که یک request دریافت کنه. برای این قسمت هم باید تو spin model checker تست و verify بشه. این توضیحات راجع به کل پروژه بود. در اخر هم یه گزارش کوتاه در مورد فرضیاتی که انجام شده و تصمیم گیری های مدل و propeties هایی که verify کردیم میخواد. و بعد هم راجع به spin بنویسم که چه چیزی کار نکردو چه چیزی رو awkward دیدم ک چه پیشنهاد هایی برای بهترش شدنش داریم . همراه با spin zip file
این پروژه شامل 1 فایل مهم است، لطفا قبل از ارسال پیشنهاد حتما نسبت به بررسی این فایل اقدام فرمایید.
مهارت ها و تخصص های مورد نیاز
بودجه
300,000 تومان تا 750,000 تومان
مهلت برای انجام
4روز
وضعیت مناقصه
بسته
درباره کارفرما
عضویت پنج سال پیش
