Home // CYBER 2018, The Third International Conference on Cyber-Technologies and Cyber-Systems // View article
Authors:
Eman Al-Qtiemat
Sudarshan K. Srinivasan
Mohana Asha Latha Dubasi
Sana Shuja
Keywords: requirements analysis; safety-critical IoT embedded devices; formal model; formal verification.
Abstract:
Formal verification has become the bedrock for ensuring software correctness when dealing with safety-critical systems. One of the biggest obstacles in applying formal techniques to commercial systems is the lack of formal specifications. Software requirements are expressed only in natural language. We present a structured approach for synthesizing formal models from natural language requirements. Synthesizing formal specification models from natural language requirements is a hard problem. Our approach is structured in that, while our procedures do most of the work in the synthesis process, it allows for structured input from the domain expert. The uniqueness of this paper is the novel approach that can synthesize natural language requirements to formal specifications that are useful for refinement-based verification, a formal verification technique that is very effective for the safety-critical Internet of Things (IoT) embedded systems. A number of safety requirements for insulin pumps have been used to demonstrate the effectiveness of the approach.
Pages: 94 to 101
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