توصيفگر ها :
وارسي , وارسي رسمي , كانتيكي , ماژول حافظه , Frama-C , زبان ACSL
چكيده فارسي :
اهميت مسئله وارسي و تاييد رسمي با در نظر گرفتن احتمال بروز خسارات جبران ناپذير در سيستم‌هاي مهم، مخصوصا سيستم‌هايي كه در بخش‌هاي بحراني مورد استفاده قرار مي‌گيرند، به عنوان مثال سيستم‌هاي هواپيما، كشتي، اتومبيل، پزشكي و غيره كاملا مشخص است. با توجه به اينكه بين سخت‌افزار و نرم‌افزار تعامل زيادي برقرار مي‌شود و هر لحظه امكان اين هست كه خطايي تحت عنوان خطاهاي گذرا رخ دهد و باعث ايجاد مشكل بشود، پس وارسي رسمي اين نرم‌افزارها امري لازم و حياتي است. هدف وارسي رسمي سيستم با قابليت اطمينان بالا است. با توجه به اينكه وارسي رسمي هنوز به ندرت در نرم‌افزارها مورد استفاده قرار مي‌گيرد و در حالي‌كه سيستم‌هاي اينترنت اشياء امروزه بسيار رايج و حياتي شده‌اند و به‌طور فيزيكي در دنياي واقعي عمل مي‌كنند. با توجه به حساس بودن و اهميت اين موضوع كه ممكن است هر رفتاري از سيستم‌هاي اينترنت اشياء سر بزند، وارسي رسمي در اين حيطه الزامي مي‌باشد. در اين پايان نامه از تأييد رسمي براي اطمينان از ايمني، امنيت نرم‌افزار و صحت عملكرد در سيستم‌عامل كانتيكي كه بسيار مورد استفاده قرار مي‌گيرد استفاده كرده‌ايم. سيستم‌عامل كانتيكي به زبان C نوشته شده است. اين سيستم عامل سبك وزن و متن باز است. ما تمامي توابع ماژول حافظه سيستم‌عامل كانتيكي كه يكي از تاثيرگذار‌ترين ماژول‌هاي اين سيستم عامل است را مورد تحليل و سپس وارسي رسمي قرار داده‌ايم. ما توابع و ماژول‌هاي هدف را مورد تحليل قرار داده، نحوه تعيين، مشخص كردن و مشخصه‌هاي مورد انتظار براي عملكرد صحيح سيستم‌عامل در ماژول حافظه و ارتباط ساير ماژول‌ها با ماژول حافظه را مشخص كرده‌ايم. سپس با استفاده از ابزارFrama-C ، يك پلتفرم تجزيه و تحليل نرم‌افزار براي كد C نوشته و با استفاده از زبان مشخصات ACSL، تمام مشخصه‌ها را بررسي نموده و ثابت كرده‌ايم كه در كدهاي اين بخش هيچ انحرافي نسبت به مشخصه‌هاي تعيين شده وجود ندارد.
چكيده انگليسي :
The importance of the formal verification issue is quite clear, considering the possibility of irreparable damage to important systems, especially systems used in critical areas, such as aircraft, ship, car, medical, etc, systems. Given that there is a lot of interaction between the hardware and the software, and at any moment it is possible for an error called transient errors to occur and cause a problem, so formal verification of this software is necessary and vital. The goal of formal verification is to develop a reliable system. Given that formal verification is still rarely used in softwares, while IoT systems have become very common and vital today, they operate physically in the real world and Due to the sensitivity and importance of this issue that any behavior of IoT systems may occur, a formal verification in this area is required. In this dissertation, we have used formal verification to ensure the safety, software security, and performance of the widely used Contiki operating system. The Contiki operating system is written in C language. This is a lightweight and open-source operating system. We have analyzed all the functions in memory module of Contiki operating system, which is one of the most effective modules of operating system, and then formally it. We have analyzed the all functions of memory module of contiki, then specified the expected characteristics for the operating system to function properly in the memory module and how other modules relate to the memory module. Then, using the Frama-c tool, a software analysis platform for C code, and ACSL specification language, we checked all the properties and proved that there was no error in the code in this section.
