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

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