370
S. Ouchani and M. Krichen
For the effectiveness of the proposed framework, we show the correctness of the
proposed model through checking and simulation. We check the assertions related to
HMS as described in Fig. 3. The first assertion is to check if only a single user has a
medical record. The second looks for the medical history of users whereas the third
confirms that the medical data are updated by an authorized user.
/ / Ch e c k i n g e a c h MH r e f e r t o o ne pa t i e n t
a s s e r t e a c h M H r e f e r O n e P a t i e n t { a l l mhs : M e d i c a l H i s t o r y
| one p t : P a t i e n t
| mhs . p = p t }
check e a c h M H r e f e r O n e P a t i e n t
/ / Ch e c k i n g e a c h MH u p d a t e d by one u s e r
a s s e r t eachMHupdatedOneUser { a l l mhs : M e d i c a l H i s t o r y
| one u r : User | mhs . u = u r }
check eachMHupdatedOneUser
/ / Ch e c k i n g s i n g l e u s e o f MR
a s s e r t singleUseMR { a l l ps : P a t i e n t | one p : P a t i e n t
| ps . mr = p . mr }
check singleUseMR
Fig. 3. Checking HMS Assertions.
5 Conclusion
This contribution proposes a concrete model for healthcare system, especially for emergency service in order to facilitate the integration and communication of IoT measures,
devices and management systems. First, we proposed UML modeling for the structural
and behavioral description of the specific domain of emergency. Further, we proposed
Alloy for ensuring the correctness of the model by expressing it safely into its input
language. With respect to the obtained results we ensure the correctness of the proposed model. Regarding the obtained results, we target to extend the work in different
directions. First, we generalize a meta model from where we can instantiate the model
of different services rather than medical and health care. In addition, we have to automate the generation of Alloy code and prove its soundness. Also, we intend to provide,
the network architecture including the web services for the different models. Then, we
show the impact between them and how we can express and ensure the privacy when
deployed. Our final target is to generate a mega system using micro-services architecture, with extensible secure services that can be deployed for different environments.
S. Ouchani and M. Krichen
For the effectiveness of the proposed framework, we show the correctness of the
proposed model through checking and simulation. We check the assertions related to
HMS as described in Fig. 3. The first assertion is to check if only a single user has a
medical record. The second looks for the medical history of users whereas the third
confirms that the medical data are updated by an authorized user.
/ / Ch e c k i n g e a c h MH r e f e r t o o ne pa t i e n t
a s s e r t e a c h M H r e f e r O n e P a t i e n t { a l l mhs : M e d i c a l H i s t o r y
| one p t : P a t i e n t
| mhs . p = p t }
check e a c h M H r e f e r O n e P a t i e n t
/ / Ch e c k i n g e a c h MH u p d a t e d by one u s e r
a s s e r t eachMHupdatedOneUser { a l l mhs : M e d i c a l H i s t o r y
| one u r : User | mhs . u = u r }
check eachMHupdatedOneUser
/ / Ch e c k i n g s i n g l e u s e o f MR
a s s e r t singleUseMR { a l l ps : P a t i e n t | one p : P a t i e n t
| ps . mr = p . mr }
check singleUseMR
Fig. 3. Checking HMS Assertions.
5 Conclusion
This contribution proposes a concrete model for healthcare system, especially for emergency service in order to facilitate the integration and communication of IoT measures,
devices and management systems. First, we proposed UML modeling for the structural
and behavioral description of the specific domain of emergency. Further, we proposed
Alloy for ensuring the correctness of the model by expressing it safely into its input
language. With respect to the obtained results we ensure the correctness of the proposed model. Regarding the obtained results, we target to extend the work in different
directions. First, we generalize a meta model from where we can instantiate the model
of different services rather than medical and health care. In addition, we have to automate the generation of Alloy code and prove its soundness. Also, we intend to provide,
the network architecture including the web services for the different models. Then, we
show the impact between them and how we can express and ensure the privacy when
deployed. Our final target is to generate a mega system using micro-services architecture, with extensible secure services that can be deployed for different environments.