Ensuring the Correctness and Well Modeling of Intelligent HMS
369
for
1
have
1..*
1 1
for
1
have
1
*
1
*
*
*
1..*
for
*
have
1
1
1
*
Patient
registration-no:string
name:string
contact-info:string
gender:string
blood-group:char(2)
allergies:string
Holders
id:int
name:string
kinship-tie:string
contact-info:string
Hospital
id:int
hospital-name:string
hospital-adress:string
Room
id:int
room-no:int(2)
floor:int(1)
Medical Record
heart-rate:number
blood-pressure:number
respiration-rate:number
temperature:number
movement:boolean
location:string
Medical History
heart-rate:number
blood-pressure:number
respiration-rate:number
temperature:number
movement:boolean
location:string
patient
user
date
User
id:int
pseudo:string
password:string
registration-date:date
Authority
Staff
name:string
contact-info:string
Mesure Object
id:int
mark:string
patient
Treatment
start-date:date
end-date:date
prescribe:string
Grade
id:int
entitled:string
category;string
Fig. 2. Class diagram for HMS.
For the validation of HMS, we describe its classes and relations in Alloy specification respecting its syntax and logic. Listing 1.1 shows a fragment of the transformation
of HMS into the input language of Alloy where sigs refer to classes, extends to associations, and the multiplicity to the class diagram relations.
Listing 1.1: HMS description in Alloy input language.
module hms / ∗ Model o f h o s p i t a l management s y s t e m . ∗ /
a b s t r a c t s i g User {} / / R e f e r t o u s e r c l a s s
s i g S t a f f e x t e n d s User { / / R e f e r t o s t a f f c l a s s
g : one Grade }
s i g M e s u r e O b j e c t e x t e n d s User {} / / R e f e r t o m e s u r e O b j e c t c l a s s
s i g P a t i e n t { / / R e f e r t o p a t i e n t c l a s s
mr : M e d i c a l R e c o r d }
s i g M e d i c a l H i s t o r y { / / R e f e r t o m e d i c a l H i s t o r y c l a s s
p : one P a t i e n t ,
u : one User }
s i g H o l d e r s { / / R e f e r t o h o l d e r s c l a s s
p : one P a t i e n t }
s i g T r e a t m e n t { / / R e f e r t o t r e a t m e n t c l a s s
p : one P a t i e n t ,
r : one Room ,
s : some S t a f f }
369
for
1
have
1..*
1 1
for
1
have
1
*
1
*
*
*
1..*
for
*
have
1
1
1
*
Patient
registration-no:string
name:string
contact-info:string
gender:string
blood-group:char(2)
allergies:string
Holders
id:int
name:string
kinship-tie:string
contact-info:string
Hospital
id:int
hospital-name:string
hospital-adress:string
Room
id:int
room-no:int(2)
floor:int(1)
Medical Record
heart-rate:number
blood-pressure:number
respiration-rate:number
temperature:number
movement:boolean
location:string
Medical History
heart-rate:number
blood-pressure:number
respiration-rate:number
temperature:number
movement:boolean
location:string
patient
user
date
User
id:int
pseudo:string
password:string
registration-date:date
Authority
Staff
name:string
contact-info:string
Mesure Object
id:int
mark:string
patient
Treatment
start-date:date
end-date:date
prescribe:string
Grade
id:int
entitled:string
category;string
Fig. 2. Class diagram for HMS.
For the validation of HMS, we describe its classes and relations in Alloy specification respecting its syntax and logic. Listing 1.1 shows a fragment of the transformation
of HMS into the input language of Alloy where sigs refer to classes, extends to associations, and the multiplicity to the class diagram relations.
Listing 1.1: HMS description in Alloy input language.
module hms / ∗ Model o f h o s p i t a l management s y s t e m . ∗ /
a b s t r a c t s i g User {} / / R e f e r t o u s e r c l a s s
s i g S t a f f e x t e n d s User { / / R e f e r t o s t a f f c l a s s
g : one Grade }
s i g M e s u r e O b j e c t e x t e n d s User {} / / R e f e r t o m e s u r e O b j e c t c l a s s
s i g P a t i e n t { / / R e f e r t o p a t i e n t c l a s s
mr : M e d i c a l R e c o r d }
s i g M e d i c a l H i s t o r y { / / R e f e r t o m e d i c a l H i s t o r y c l a s s
p : one P a t i e n t ,
u : one User }
s i g H o l d e r s { / / R e f e r t o h o l d e r s c l a s s
p : one P a t i e n t }
s i g T r e a t m e n t { / / R e f e r t o t r e a t m e n t c l a s s
p : one P a t i e n t ,
r : one Room ,
s : some S t a f f }