Automated UML-based Formal Model of E-Health System

The E-Health is a central part of monitoring and managing patient's health electronically at hospital. The existing patient treatment systems works manually because of ambiguities and limitations of semiformal techniques. Therefore, formal model of Patient Treatment System (PTS) as e-health is presented in this work with automation because it is difficult to provide correctness of a proposed model at modeling phase. In E-health system, the doctor scans the patient RFID tag for viewing and entering information in system, diagnosing, giving medicine and test prescription of patient. Further, doctor can view the current location of the patient through RFID number. Firstly, we have developed a semiformal model of the system using Unified Modeling Language (UML) because UML depicts better system design understandability. We have proposed an automated model using Non-Deterministic Automata (NFA) for describing system working in the form of states and transitions. Further, a formal model is developed in Vienna Development Method (VDM-SL) based on discrete mathematical concepts. Formal methods are used in this work to confirm robustness, accuracy and efficiency of the E-health system. The developed formal model is verified by VDM-SL toolbox. Further the maintenance and testing cost is reduced using automata and RFID based E-health system.