Home // CYBER 2019, The Fourth International Conference on Cyber-Technologies and Cyber-Systems // View article

Refinement Checker for Embedded Object Code Verification

Authors:
Mohana Asha Latha Dubasi
Sudarshan K. Srinivasan
Sana Shuja
Zeyad A. Al-Odat

Keywords: embedded devices; formal verification; refinementbased verification; verification of object code, WFS refinement

Abstract:
We present a formal verification methodology that automates the process to check for correctness of low-level realtime interrupt-driven object code programs. Automation helps in the verification of large-scale programs. Our methodology is based on the theory of Well-Founded Simulation (WFS) refinement, where both the formal specification and implementation are modeled as transition systems (TSs). WFS refinement is used as the notion of correctness and defines what it means for an implementation TS to satisfy its specification TS. WFS refinement has key features like stuttering and refinement maps. Stuttering aids in the abstraction of the state space of the implementation TS. Refinement maps bridge the abstraction gap between the two systems. The efficiency and scalability of the approaches are demonstrated on several device object code case studies.

Pages: 81 to 87

Copyright: Copyright (c) IARIA, 2019

Publication date: September 22, 2019

Published in: conference

ISSN: 2519-8599

ISBN: 978-1-61208-743-6

Location: Porto, Portugal

Dates: from September 22, 2019 to September 26, 2019