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