ارائه مدلي براي افزايش قابليت اطمينان نرم‌افزارهاي نهفته و بي‌درنگ مبتني بر روش صوري تفسير انتزاعي

Presenting a model for increasing the reliability of embedded and real-time softwares based on the abstract interpretation of formal method

قابليت اطمينان در يك نرم‌افزار، از جنبه هاي حائز اهميت در حوزه كيفيت نرم‌افزار مي باشد. زمانيكه در مورد نرم‌افزارهاي نهفته و بي‌درنگ صحبت مي‌شود، اهميت قابليت اطمينان بسيار بيشتر خواهد بود. زيرا بيشتر اين نرم‌افزارها در حوزه هاي مرتبط با بحراني-ايمني و بحراني-ماموريت، سر و كار داشته و هر گونه شكست در نرم‌افزار حين ماموريت ممكن است خسارات مالي و جاني غيرقابل جبران به همراه داشته باشد. استفاده از روش تفسير انتزاعي به عنوان يكي از انواع تحليل‌هاي ايستا، به منظور تصديق و صحه گذاري معيارهاي كيفيت نرم‌افزار، به ويژه معيارهاي عملكردي و متناسب با مشخصه هاي مورد انتظار نرم‌افزار، يك راه مناسب براي افزايش قابليت اطمينان نرم‌افزار مي باشد. در اين پژوهش سعي شده است يك مدل براي افزايش قابليت اطمينان نرم‌افزارهاي نهفته و بي‌درنگ در حوزه هوايي (هوانوردي و هوا-فضا) و متمركز بر استانداردهاي ECSS40 و ECSS80 با استفاده از ابزارهاي تحليل ايستا مبتني بر روش تفسير انتزاعي (كه گونه‌اي از روش‌هاي صوري و وارسي مدل مي باشد) ارائه شود. نتايج استفاده از اين مدل در شناسايي برخي اشكالات در قطعات كد نمونه مورد مطالعه، موثر بوده است.

Reliability in a software is one of the important aspects in the field of software quality. When it comes to embedded and real-time software, the importance of reliability will be much higher. Because most of these software deal with criticalsafety and critical-mission fields, and any failure in the software during the mission may cause irreparable financial and life losses. Using the abstract interpretation method as one of the types of static analysis, in order to verification and validation the software quality criteria, especially the functional criteria and according to the expected requirements of the software, is a suitable way to increase the reliability of the software. In this research, a model has been presented to show how we can increase the reliability of embedded and real-time software in the avionics engineering scope (focused on ECSS40 and ECSS80 standards) using static analysis tools based on the abstract interpretation method. The results of using this model have been effective in identifying some errors in the studied sample code parts.