مدلسازی و درستیابی سیستم اینتر لاکینگ راه اهن به روش صوری و با استفاده از متد B

  • سال انتشار: 1389
  • محل انتشار: دوازدهمین همایش بین المللی حمل و نقل ریلی
  • کد COI اختصاصی: RTC12_093
  • زبان مقاله: فارسی
  • تعداد مشاهده: 1123
دانلود فایل این مقاله

نویسندگان

احمد میر آبادی

محسن پیکرستان

چکیده

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

کلیدواژه ها

ایمنی محور ، روش صوری ، مشخصات سوری ، درستیابی ، متد B

مقالات مرتبط جدید

اطلاعات بیشتر در مورد COI

COI مخفف عبارت CIVILICA Object Identifier به معنی شناسه سیویلیکا برای اسناد است. COI کدی است که مطابق محل انتشار، به مقالات کنفرانسها و ژورنالهای داخل کشور به هنگام نمایه سازی بر روی پایگاه استنادی سیویلیکا اختصاص می یابد.

کد COI به مفهوم کد ملی اسناد نمایه شده در سیویلیکا است و کدی یکتا و ثابت است و به همین دلیل همواره قابلیت استناد و پیگیری دارد.