Home // International Journal On Advances in Security, volume 12, numbers 1 and 2, 2019 // View article
Authors:
Eman Al-Qtiemat
Sudarshan Srinivasan
Zeyad Al-Odat
Mohana Asha Latha Dubasi
Sana Shuja
Keywords: requirements analysis; safety-critical IoT embedded devices; timing specifications; timing transition systems; formal model; formal verification.
Abstract:
Abstract —Formal verification methods have been shown to be very effective in finding corner case bugs and ensuring safety of embedded software systems. The use of formal verification requires a specification, which is typically a high-level mathemat- ical model that defines the correct behavior of the system to be verified. However, embedded software requirements are typically described in natural language. Transforming these requirements to formal specifications is currently a big gap. While there is some work in this area, this paper proposes solutions to address this gap in the context of refinement-based verification, a class of formal methods that have shown to be effective for embedded object code verification. The proposed approach also addresses both functional and timing requirements and has been demonstrated in the context of safety requirements for software control of infusion pumps.
Pages: 95 to 107
Copyright: Copyright (c) to authors, 2019. Used with permission.
Publication date: June 30, 2019
Published in: journal
ISSN: 1942-2636