368
S. Ouchani and M. Krichen
and the possible use cases for HMS. The doctor can prescribe the status of a patient
already registered by the IT Staff, and also can consult his medical reports. Each patient
have a medical record, that can be filled or updated by a nurse, a doctor, or a smart
object. These cases are only allowed for signed-in and authorized actors. A nurse and
smart objects can fill or update the medical record whereas the doctor can consult, fill,
update, and prescribe medicines to a patient.
Hospital Management System
Hospital Management System
include
include
include
include
include
Fill-update
Consult
Prescribe
Register
Authorize
Authentify
Nurse
Mesure Object
Doctor
IT Staff
Fig. 1. Use case diagram for HMS.
Figure 2 shows the main classes that represent the structure of principle users and
resources. Only the staff with the IoT can fill or update the patient’s medical record if
they have the authority to do that, also each update of the medical record will be saved
automatically in the medical history. We consider also to a patient to have a holder
regarding his treatments.
4 HMS Validation
In terms of system specification, Alloy is a modeling language including a formal syntax and semantics. A specified model in Alloy can be in ASCII format as well with
a visual representation. Generally, Alloy targets the formal specification of object oriented data models that can be used generally in data modeling, that also can be displayed
graphically. Also for systems analysis, Alloy is a verification tool that automatically
analyze the properties (requirements) of alloy models. After checking the properties,
Alloy might generate counterexamples in case of the property violation. Alloy consists
of predicates, facts, relations and signatures. Signatures represent the different entities
of the system. Relations specify the relations between them. Predicates and facts define
constraints, which apply on relations and signatures.
Each Alloy model begins with the module declaration. The first step is to declare the
signatures using the keyword sig. Then, we define the relations (fields) which associate
atoms. To define a subset, we should use the keywords extends or in, also the multiplicity keywords such as one, lone, set, some, etc. Facts correspond to the constraints which
must always hold. Finally, we define the predicate using the keyword pred and run it.
S. Ouchani and M. Krichen
and the possible use cases for HMS. The doctor can prescribe the status of a patient
already registered by the IT Staff, and also can consult his medical reports. Each patient
have a medical record, that can be filled or updated by a nurse, a doctor, or a smart
object. These cases are only allowed for signed-in and authorized actors. A nurse and
smart objects can fill or update the medical record whereas the doctor can consult, fill,
update, and prescribe medicines to a patient.
Hospital Management System
Hospital Management System
include
include
include
include
include
Fill-update
Consult
Prescribe
Register
Authorize
Authentify
Nurse
Mesure Object
Doctor
IT Staff
Fig. 1. Use case diagram for HMS.
Figure 2 shows the main classes that represent the structure of principle users and
resources. Only the staff with the IoT can fill or update the patient’s medical record if
they have the authority to do that, also each update of the medical record will be saved
automatically in the medical history. We consider also to a patient to have a holder
regarding his treatments.
4 HMS Validation
In terms of system specification, Alloy is a modeling language including a formal syntax and semantics. A specified model in Alloy can be in ASCII format as well with
a visual representation. Generally, Alloy targets the formal specification of object oriented data models that can be used generally in data modeling, that also can be displayed
graphically. Also for systems analysis, Alloy is a verification tool that automatically
analyze the properties (requirements) of alloy models. After checking the properties,
Alloy might generate counterexamples in case of the property violation. Alloy consists
of predicates, facts, relations and signatures. Signatures represent the different entities
of the system. Relations specify the relations between them. Predicates and facts define
constraints, which apply on relations and signatures.
Each Alloy model begins with the module declaration. The first step is to declare the
signatures using the keyword sig. Then, we define the relations (fields) which associate
atoms. To define a subset, we should use the keywords extends or in, also the multiplicity keywords such as one, lone, set, some, etc. Facts correspond to the constraints which
must always hold. Finally, we define the predicate using the keyword pred and run it.