Verification Framework for Functionality of ECG BioSensors

Abstract

Wireless Body Sensor Networks (WBSNs) enable the integration of various physiological sensors that facilitate continuous monitoring of a patient condition as well as support independent living of persons with chronic conditions in their homes. WBSNs may contain different types of sensors that are used to monitor several medical parameters such as ElectroCardioGram (ECG), which is one of the most commonly used and studied biomedical sensors. ECG Biosensors are used to detect and transmit the electrical activity of the heart over a period of time. The ECGs are treated by a signal processing unit inside the biosensor to detect and identify heart patterns. Testing and verification of these biosensor systems is a challenging and important process since faults in these critical systems may lead to loss of lives as well as loss of money and reputation. However, due to the complexity of these systems, and the increasing demand for new products and new technologies in this domain, traditional testing methods might not be adequate to provide a high level of assurance about the correctness of their operation. In this work, we propose a verification framework for functionality and security of ECG biosensors. The framework is composed of three parts, wherein the first; we use theorem proving to verify the biosensor functionality. Then, we develop a test case gene ration ii algorithm based on formal specifications to validate the functionality of the ECG biosensor. The last part addresses security in the biosensor by providing a protocol with low overhead on the biosensor resources. The protocol is formally verified using the model checking technique. Our framework has been used for the verification of ECG biosensors at several levels of abstractions with respect to functionality and security.

Date of Award	Feb 2017
Original language	American English
Supervisor	Amjad Gawanmeh (Supervisor)