Home // International Journal On Advances in Life Sciences, volume 12, numbers 1 and 2, 2020 // View article

Synthesis of Refinement Maps for Real-Time Object Code Verification

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

Keywords: Formal verification; Synthesising of refinement maps; Formal specifications; Refinement-based verification.

Abstract:
Refinement-based verification is a formal verification method, it is considered as a very scalable approach for dealing with low-level artifacts such as real-time object code verification. Two main obstacles prevent implementing the refinement-based verification; firstly, it requires formal specification in transition system form while most specifications are of informal or semi-formal form. To solve this issue, we already proposed synthesising procedures to transform both functional and timing requirements from natural language form into formal specifications, our approach was successfully applied on insulin pump safety requirements. Secondly, the verification process requires a construction of refinement map, which is a function maps implementation states (the artifact to be verified) onto specification states. Actually, constructing refinement maps often requires deep understanding and intuitions about the specification and implementation, it is shown very difficult to construct refinement maps manually. To go over this obstacle, the construction of refinement maps should be automated. As a first step toward the automation process, we manually developed refinement maps for various safety properties concerning the software control operation of insulin pumps. In addition, we identified possible generic templates for construction of refinement maps. To complement our previous work, this paper is built on refinement maps and refinement maps templates proposed previously to automate the construction of refinement maps. Synthesising procedures of refinement maps for functional and timing specifications are proposed. In addition, this paper shows more results of formal specifications and their suggested refinement map functions for timing requirements. Our work uses safety requirements of generic infusion pump model as heuristic data.

Pages: 47 to 56

Copyright: Copyright (c) to authors, 2020. Used with permission.

Publication date: June 30, 2020

Published in: journal

ISSN: 1942-2660