وارسي رسمي به منظور آشكار سازي خطا در ماژول حافظه سيستم عامل كانتيكي

اصفهان : دانشگاه صنعتي اصفهان

كامپيوتر

كارشناسي ارشد

اهميت مسئله وارسي و تاييد رسمي با در نظر گرفتن احتمال بروز خسارات جبران ناپذير در سيستم‌هاي مهم، مخصوصا سيستم‌هايي كه در بخش‌هاي بحراني مورد استفاده قرار مي‌گيرند، به عنوان مثال سيستم‌هاي هواپيما، كشتي، اتومبيل، پزشكي و غيره كاملا مشخص است. با توجه به اينكه بين سخت‌افزار و نرم‌افزار تعامل زيادي برقرار مي‌شود و هر لحظه امكان اين هست كه خطايي تحت عنوان خطاهاي گذرا رخ دهد و باعث ايجاد مشكل بشود، پس وارسي رسمي اين نرم‌افزارها امري لازم و حياتي است. هدف وارسي رسمي سيستم با قابليت اطمينان بالا است. با توجه به اينكه وارسي رسمي هنوز به ندرت در نرم‌افزارها مورد استفاده قرار مي‌گيرد و در حالي‌كه سيستم‌هاي اينترنت اشياء امروزه بسيار رايج و حياتي شده‌اند و به‌طور فيزيكي در دنياي واقعي عمل مي‌كنند. با توجه به حساس بودن و اهميت اين موضوع كه ممكن است هر رفتاري از سيستم‌هاي اينترنت اشياء سر بزند، وارسي رسمي در اين حيطه الزامي مي‌باشد. در اين پايان نامه از تأييد رسمي براي اطمينان از ايمني، امنيت نرم‌افزار و صحت عملكرد در سيستم‌عامل كانتيكي كه بسيار مورد استفاده قرار مي‌گيرد استفاده كرده‌ايم. سيستم‌عامل كانتيكي به زبان C نوشته شده است. اين سيستم عامل سبك وزن و متن باز است. ما تمامي توابع ماژول حافظه سيستم‌عامل كانتيكي كه يكي از تاثيرگذار‌ترين ماژول‌هاي اين سيستم عامل است را مورد تحليل و سپس وارسي رسمي قرار داده‌ايم. ما توابع و ماژول‌هاي هدف را مورد تحليل قرار داده، نحوه تعيين، مشخص كردن و مشخصه‌هاي مورد انتظار براي عملكرد صحيح سيستم‌عامل در ماژول حافظه و ارتباط ساير ماژول‌ها با ماژول حافظه را مشخص كرده‌ايم. سپس با استفاده از ابزارFrama-C ، يك پلتفرم تجزيه و تحليل نرم‌افزار براي كد C نوشته و با استفاده از زبان مشخصات ACSL، تمام مشخصه‌ها را بررسي نموده و ثابت كرده‌ايم كه در كدهاي اين بخش هيچ انحرافي نسبت به مشخصه‌هاي تعيين شده وجود ندارد.

210877

نرم افزار

مهندسي برق و كامپيوتر

دانشگاه صنعتي اصفهان

محمدرضا حيدرپور، زينب زالي

الهام محمودزاده، علي ابن نصير