![](/images/graphics-bg.png)
Improved Efficiency of Object Code Verification Using Statically Abstracted Object Code
Joint Authors
Shaukat, N.
Shuja, S.
Srinivasan, S. K.
Jabeen, S.
Source
Issue
Vol. 2020, Issue 2020 (31 Dec. 2020), pp.1-19, 19 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2020-07-14
Country of Publication
Egypt
No. of Pages
19
Main Subjects
Abstract 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.
American Psychological Association (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
Modern Language Association (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
American Medical Association (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
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-1209090