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

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

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

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.