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

امروزه سیستم های نرم افزاری ایمنی ـ بحرانی Safety-Critical بخشی جدایی ناپذیر اززندگی بشرگردیده اند به همان اندازه که نقش این نرم افزارها درکارهای روزمره بیشتر می گردد وجود خطا درآنها نیز هزینه های جانی و مالی سنگین تری دارد استفاده ازتمامی روشهای مرسوم درآزمون نرم افزار اگرچه باعث پیدا کردن خطاهای موجود می گردد اما هیچ گاه تضمینی برعدم وجود خطا نمی دهد درحالیکه نرم افزارهای ایمنی ـ بحرانی نیازمند روشی هستند که این تضمین را ارایه نماید و به همین دلیل استفاده ازروشهای فرمال مانند بررسی مدل برای آنها توصیه میگردد دراین مقاله سعی گردیده است ابتدا خصوصیات نرم افزارهای ایمنی ـ بحرانی بیان گردد تا براین اساس بهترین روش وارسی این گونه سیستم ها معرفی شود درادامه نیز روش بررسی مدل Model Checking به عنوان هیافت منتخب برای این دسته ازنرم افزارها معرفی گردیده و درانتها نرم افزار SPIN و زبان مدلسازی Promela به عنوان یکی ازابزارهای بررسی مدل معرفی میگردند

آزمون نرم افزار ، نرم افزارهای ایمنی ـ بحرانی Safety-Critical ، بررسی مدل Model Checking ، نرم افزار spin ، زبان مدلسازی Promela