راست آزمایی قابلیت دسترس پذیری الگوریتم باکری با یک زبان برنامه ریزی با قیود

سال انتشار: 1400
نوع سند: مقاله کنفرانسی
زبان: فارسی
مشاهده: 155

فایل این مقاله در 9 صفحه با فرمت PDF قابل دریافت می باشد

استخراج به نرم افزارهای پژوهشی:

لینک ثابت به این مقاله:

شناسه ملی سند علمی:

ITCT12_037

تاریخ نمایه سازی: 7 شهریور 1400

چکیده مقاله:

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

کلیدواژه ها:

نویسندگان

رضا رافع

استاد راهنما

حامد ویسی

نویسنده