![](/images/graphics-bg.png)
Improved Efficiency of Object Code Verification Using Statically Abstracted Object Code
المؤلفون المشاركون
Shaukat, N.
Shuja, S.
Srinivasan, S. K.
Jabeen, S.
المصدر
العدد
المجلد 2020، العدد 2020 (31 ديسمبر/كانون الأول 2020)، ص ص. 1-19، 19ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2020-07-14
دولة النشر
مصر
عدد الصفحات
19
التخصصات الرئيسية
الملخص EN
One of the major challenges in the formal verification of embedded system software is the complexity and substantially large size of the implementation.
The problem becomes crucial when the embedded system is a complex medical device that is executing convoluted algorithms.
In refinement-based verification, both specification and implementation are expressed as transition systems.
Each behavior of the implementation transition system is matched to the specification transition system with the help of a refinement map.
The refinement map can only project those values from the implementation which are responsible for labeling the current state of the system.
When the refinement map is applied at the object code level, numerous instructions map to a single state in the specification transition system called stuttering instructions.
We use the concept of Static Stuttering Abstraction (SSA) that filters the common multiple segments of stuttering instructions and replaces each segment with a merger.
SSA algorithm reduces the implementation state space in embedded software, subsequently decreasing the efforts involved in manual verification with WEB refinement.
The algorithm is formally proven for correctness.
SSA is implemented on the pacemaker object code to evaluate the effectiveness of abstracted code in verification process.
The results helped to establish the fact that, despite code size reduction, the bugs and errors can still be found.
We implemented the SSA technique on two different platforms and it has been proven to be consistent in decreasing the code size significantly and hence the complexity of the implementation transition system.
The results illustrate that there is considerable reduction in time and effort required for the verification of a complex software control, i.e., pacemaker when statically stuttering abstracted code is employed.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Shaukat, N.& Shuja, S.& Srinivasan, S. K.& Jabeen, S.. 2020. Improved Efficiency of Object Code Verification Using Statically Abstracted Object Code. Scientific Programming،Vol. 2020, no. 2020, pp.1-19.
https://search.emarefa.net/detail/BIM-1209090
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Shaukat, N.…[et al.]. Improved Efficiency of Object Code Verification Using Statically Abstracted Object Code. Scientific Programming No. 2020 (2020), pp.1-19.
https://search.emarefa.net/detail/BIM-1209090
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Shaukat, N.& Shuja, S.& Srinivasan, S. K.& Jabeen, S.. Improved Efficiency of Object Code Verification Using Statically Abstracted Object Code. Scientific Programming. 2020. Vol. 2020, no. 2020, pp.1-19.
https://search.emarefa.net/detail/BIM-1209090
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-1209090
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
![](/images/ebook-kashef.png)
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر
![](/images/kashef-image.png)