Model driven flexible design of a wireless body sensor network for health monitoring

The Wireless Body Sensor Network (WBSN) is a wireless network that is designed to allow communication among sensor nodes that are attached to a human body to monitor the body's vital parameters and environment. The design and development of such WBSN systems for health monitoring have received a large amount of attention recently, in research studies and in industry. This attention is mainly motivated by costly health care and by recent advances in the development of miniature health monitoring devices as well as emerging technologies, such as the Internet of Things (IoT), which contribute to the main challenges of 5G. The existence of an explicit approach to address the required software design and verification should be very beneficial for the construction and maintenance of such systems. This paper presents a preventive health care system that has a flexible design. The proposed system is based on an architecture that has heterogeneous nodes and provides both daily continuous monitoring as well as specific controls. We defined a model to describe the WBSN's global behavior. An important aspect of this work is that we propose a model-driven engineering (MDE) approach to address the derivation of each node's behavior in the WBSN from the WBSN global behavior. This approach allows developers to obtain a system design from the global specification of its requirement. To ensure the conformance of this design to its specification, the derived behaviors should be validated and verified before their deployment. In fact, formal methods are powerful tools for software engineers to verify the logical correctness of concurrent software at different levels of its life cycle. Model checking is one of the most powerful formal methods for verifying the logical correctness of such concurrent systems. In this work, we make use of a model checking approach that is based on a model transformation to validate the automatically derived behavior of a WBSN for health monitoring. This model-driven approach will check whether the derived system behaves correctly according to its global specification, while the objective is to increase the system's performance and QoS. This approach allows the developer to reason about a model of the global system rather than about the system itself.