Home // VALID 2019, The Eleventh International Conference on Advances in System Testing and Validation Lifecycle // View article

Refinement Maps for Insulin Pump Control Software Safety Verification

Authors:
Eman Al-Qtiemat
Sudarshan Srinivasan
Zeyad Al-Odat
Sana Shuja

Keywords: Keywords–Formal verification; safety-critical devices; Refinement maps; Refinement-based verification.

Abstract:
Abstract—Refinement-based verification is a formal verification technique that has shown promise to be applicable for verification of low-level real-time embedded object code. In refinement-based verification, both the implementation (the artifact to be verified) and the specification are modeled as transition systems, which essentially capture the states of the system and transitions between the states. A key step in the verification process is the construction of a refinement map, which is a function that maps implementation states onto specification states. Construction of refinement maps is most often done manually and requires key insights about how the implementation and specification behave. In this paper, we develop refinement maps for various safety properties concerning the software control operation of insulin pumps. We then identify possible generic templates for construction of refinement maps as a first step towards developing a process to construct refinement maps in an automated fashion.

Pages: 56 to 61

Copyright: Copyright (c) IARIA, 2019

Publication date: November 24, 2019

Published in: conference

ISSN: 2308-4316

ISBN: 978-1-61208-755-9

Location: Valencia, Spain

Dates: from November 24, 2019 to November 28, 2019