首页    期刊浏览 2024年11月08日 星期五
登录注册

文章基本信息

  • 标题:Improved Efficiency of Object Code Verification Using Statically Abstracted Object Code
  • 本地全文:下载
  • 作者:N. Shaukat ; S. Shuja ; S. K. Srinivasan
  • 期刊名称:Scientific Programming
  • 印刷版ISSN:1058-9244
  • 出版年度:2020
  • 卷号:2020
  • 页码:1-19
  • DOI:10.1155/2020/6791891
  • 出版社:Hindawi Publishing Corporation
  • 摘要:

    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.

国家哲学社会科学文献中心版权所有