Formal Verification and Design of Smart Stick for Blind People
Naveed, Ayesha · Zenodo (CERN European Organization for Nuclear Research) · 2020
Researchers these days widely use formal verification to verify software and embedded systems. This paper is based on a smart stick (embedded system) designed for blind people. This embedded system design has been verified using model checking and formal verification. In this paper, an Arduino based stick has been proposed for blind users to help in their navigation by detecting the obstacles using Ultrasonic sensors and speech warning message. It is able to inform the blind person about the circumstances and present condition of the path where he/she is walking. The system is tested under different scenarios in verification and validation software to confirm its authenticity. This system has been practically implemented and, in this paper, we used formal verification and software validation tools to detect and remove any bugs in the requirement and design phase. We believe this will immune our code from bugs and we can find their possible remedies. We claim that this work is novel as we haven’t found any solution in research for blind people that have been formally verified using model checking at design phase and validated using automated tools at requirement phase.