مدلسازی و درستیابی سیستم اینتر لاکینگ راه اهن به روش صوری و با استفاده از متد B
Publish place: 12th Railway Transportation Conference
Publish Year: 1389
نوع سند: مقاله کنفرانسی
زبان: Persian
View: 1,028
This Paper With 14 Page And PDF Format Ready To Download
- Certificate
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
RTC12_093
تاریخ نمایه سازی: 4 دی 1390
Abstract:
ابهامات سیستمها منشاء بروز خطا بوده و خطا در سیستمهای کنترلی مانند سیستمهای کنترل ریلی از علل و عوامل حوادثی مانند تصادف ریلی و یا خروج از خط می باشد. یکی از راهکارهای رفع ابهامات ، مدلسازی صریح و استفاده از روشهای صوری بوده بطوریکه در بسیار از قراردادهای توسعه نرم افزارهای ایمنی محور استفاده از روش مذکور در مجموعه الزلمات قراردادی گنجانده می شود. روش صوری با استفاده از اثبات کننده های اتوماتیک و نیز آزمون گرهای مدل در زمینه توسعه نرم افزارهای ایمنی محور که هزینه خطای بالایی دراند بسیار مورد توجه می باشد. در حوزه مهندسی راهآهن بکار گیری روش ذکور در کشورهای پیشرفته بسیار متداول بوده و یک نمونه از چگونگی استفاده آن در این تحقیق بررسی شده است. در بحث اینتر لاکینگ ایستگاهها تعامل بین اجزاء مدلی پیچیده می سازد که برررسی این تعاملات بسیار مشکل خواهد بود. از این دید بیان صوری مشخصات با استفاده از روشی صوری بسیار کارآمد می باشد. در این مقاله مدلی از اینتر لاکینگ متمرکز با حلقه بسته ارائه شده است که اگثر فرآیدها مانند رزرو نمودن مسیر ، قفل مسیر ، مسیر شانت ، مسیر معکوس و مسیر فراخوان را در بردارد.
Keywords:
Authors
مراجع و منابع این Paper:
لیست زیر مراجع و منابع استفاده شده در این Paper را نمایش می دهد. این مراجع به صورت کاملا ماشینی و بر اساس هوش مصنوعی استخراج شده اند و لذا ممکن است دارای اشکالاتی باشند که به مرور زمان دقت استخراج این محتوا افزایش می یابد. مراجعی که مقالات مربوط به آنها در سیویلیکا نمایه شده و پیدا شده اند، به خود Paper لینک شده اند :