Model checking the properties of an electronic healthcare system to facilitate the detection of preeclampsia through a smart bracelet

Electronic healthcare systems sustain a lifelong observation and treatment of population health and diseases. Through the collaborative communities of doctors the medical staff, along with their students, improve their knowledge regarding their activity field. The current paper proposes an electronic healthcare system that monitors and treats pregnant women who suffer from preeclampsia. Such a system is valuable, because it allows the prediction of emergency situations through the use of a decision support system. The blood pressure of pregnant women will be continuously monitored through a smart bracelet and the information about them is available for the doctors who can monitor their patients, give a diagnosis and treatment, as well as to update it. Doctors can discuss between them through a collaborative virtual environment. Furthermore, medical students can benefit from this and enrich their knowledge. Alerts are sent when critical situations are noticed by the system. Healthcare systems are complex, because they imply computer science, electronics, telecommunication and medicine. Models are created based on how the devices communicate between them, how health data is measured and from it how information is stored and retrieved. The reason behind the creation and test of such models is to determine the issues which might leads to the occurrence of deadlocks. The formal model for the preeclampsia healthcare system was created with Promela and tested automatically using the Spin tool. According to the test, the normal flow was designed in a proper manner, without leading to exceptional behaviors. The formal model will be implemented and integrated in the preeclampsia electronic healthcare system