Home // CYBER 2018, The Third International Conference on Cyber-Technologies and Cyber-Systems // View article

Static Stuttering Abstraction for Object Code Verification

Authors:
Naureen Shaukat
Sana Shuja
Sudarshan Srinivasan
Shaista Jabeen
Mohana Asha Latha Dubasi

Keywords: Formal verification; static stuttering abstraction; stuttering instructions; refinement map; infusion pump

Abstract:
The biggest challenge in the formal verification of an embedded system software is the complexity and large size of the implementation. The problem gets even bigger when the embedded system is an Internet of Things (IoT) device that is running intricate algorithms. In Refinement-based verification, both specification and implementation are expressed as transition systems. Each behavior of the implementation transition system is matched with the specification transition system with the help of a refinement map. The refinement map can only project those values that are responsible to label the current state of the system. When the refinement map is applied at object code level, several instructions map to a single state in the specification transition system called stuttering instructions. The concept of Static Stuttering Abstraction (SSA) is a novel idea that focuses on filtering common multiple segments of these stuttering instructions. The patterns are then replaced by mergers that preserve the behavior of the original object code and extensively reduce the size of the object code. The smaller code size also gives the lesser number of stuttering transitions and eventually more discernible matching between the specification and implementation of transition systems. We have implemented SSA technique on two platforms using infusion pump as a case study and the technique has proved consistent in considerably reducing the size and complexity of the implementation transition system.

Pages: 102 to 106

Copyright: Copyright (c) IARIA, 2018

Publication date: November 18, 2018

Published in: conference

ISSN: 2519-8599

ISBN: 978-1-61208-683-5

Location: Athens, Greece

Dates: from November 18, 2018 to November 22, 2018