Int
ern
at
i
onal
Journ
al of Ele
ctrical
an
d
Co
mput
er
En
gin
eeri
ng
(IJ
E
C
E)
Vo
l.
15
,
No.
1
,
Febr
uary
20
25
, pp.
870
~
882
IS
S
N:
20
88
-
8708
, DO
I: 10
.11
591/ij
ece.v
15
i
1
.
pp
870
-
882
870
Journ
al h
om
e
page
:
http:
//
ij
ece.i
aesc
or
e.c
om
Timed c
oncurr
ent sys
tem
model
ing an
d verifi
cation of
home
care
plan
Acep
T
arya
na
1,2
, D
ie
ky
Ad
z
kiy
a
1
, Muh
am
mad
Syi
fa’ul
Mufi
d
1
, I
m
am
M
u
khlas
h
1
1
Dep
artm
en
t of
M
ath
em
atics,
Facult
y
of Science and
D
ata Analy
tics,
Ins
titu
t T
ek
n
o
lo
g
i Sepuluh
Nop
em
b
er,
Sur
ab
ay
a,
Ind
o
n
esia
2
Dep
artm
en
t of
E
l
ectrica
l
E
n
g
in
eerin
g
,
Eng
in
eering
Fac
u
lty
,
Un
iv
ersitas J
en
d
eral
So
ed
irman
,
Pu
rwok
erto,
Ind
o
n
esia
Art
ic
le
In
f
o
ABSTR
A
CT
Art
ic
le
history:
Re
cei
ved
Dec
9,
2023
Re
vised
Sep 2
0,
2024
Accepte
d
Oct
1,
2024
A
home
c
are
p
la
n
(HCP
)
ca
n
be
integra
te
d
w
it
h
an
elec
tronic
me
d
ical
rec
ords
(EMR)
sys
te
m,
serv
ing
as
an
exa
mp
le
of
a
r
ea
l
-
ti
m
e
s
ystem
with
conc
urre
n
t
proc
esses.
To
ensure
eff
ectiv
e
oper
ation,
HCP
s
must
be
fre
e
of
software
bugs.
I
n
thi
s
pap
er,
we
exp
lore
the
mo
del
ing
and
ver
if
ic
a
ti
on
of
HCP
s
from
the
per
spe
ct
iv
e
of
sche
du
li
n
g
data
oper
at
i
onal
i
za
t
ion.
Speci
fi
ca
l
ly,
we
inv
esti
ga
te
ho
w
patient
s
c
an
obta
in
h
om
e
ser
vic
es
while
pre
venting
sche
duli
ng
con
flicts
in
the
con
te
xt
of
li
m
it
ed
resourc
e
s.
Our
goal
is
to
develop
and
ve
rify
rob
ust
models
for
thi
s
purpose.
We
em
p
loy
forma
l
ism
to
c
onstruct
and
v
al
id
at
e
the
mo
del
,
fo
ll
owing
the
se
steps:
i)
develop
req
uire
m
ent
s
and
spec
ifica
t
ions;
ii
)
cr
ea
t
e
a
mode
l
with
conc
urre
n
t
pro
c
esses
using
t
im
e
d
aut
o
ma
t
a;
and
iii)
v
eri
fy
th
e
mode
l
using
UP
PAAL
tool
s.
Our
study
foc
u
ses
on
HCP
implementation
a
t
a
r
egi
on
al
gene
ra
l
hospital
in
B
anyum
as
D
istri
ct,
Cen
tra
l
J
ava
,
Indon
esia.
The
resul
ts
inc
lud
e
models
and
spec
if
ications
base
d
on
t
im
ed
aut
om
at
a
and
ti
m
ed
com
put
at
ion
tr
ee
logic
(TCTL).
We
succ
essfully
ver
ified
a
conc
ur
ren
t
model
tha
t
ut
il
i
ze
s
synchronized
counter
v
ariabl
es
and
a
send
er
-
re
ceiv
er
appr
oa
ch
to
an
al
y
ze
co
ll
is
ion
c
onstra
in
ts
a
rising
fro
m
the
synchroniz
a
ti
on
of
pa
ti
en
t
and
resour
ce
p
lans
.
Ke
yw
or
ds:
Dead
l
ock
Fo
r
mali
sm
Home ca
re
plan
Synchr
on
iz
at
io
n
Ver
ific
at
io
n
This
is an
open
acc
ess arti
cl
e
un
der
the
CC
BY
-
SA
l
ic
ense
.
Corres
pond
in
g
Aut
h
or
:
Diek
y Ad
z
kiy
a
Dep
a
rtme
nt of
M
at
he
mati
cs,
Faculty
of Scie
nce a
nd D
at
a
An
al
ytics, I
ns
ti
tut Tek
nolo
gi
Sepulu
h Nope
mb
e
r
Keputi
h, S
ukol
il
o,
S
ur
a
ba
ya,
East
Jav
a
60
111,
I
ndonesi
a
Emai
l:
d
ie
ky@
it
s.ac.id
1.
INTROD
U
CTION
E
l
e
c
t
r
o
n
i
c
m
e
d
i
c
a
l
r
e
c
o
r
d
s
(
E
M
R
)
s
y
s
t
e
m
s
a
r
e
s
t
i
l
l
d
e
v
e
l
o
p
i
n
g
,
a
s
i
n
f
o
r
m
a
t
i
o
n
c
o
m
m
u
n
i
c
a
t
i
o
n
t
e
c
h
n
o
l
o
g
i
e
s
a
r
e
p
r
i
o
r
i
t
i
z
e
d
i
n
d
e
v
e
l
o
p
e
d
a
n
d
d
e
v
e
l
o
p
i
n
g
c
o
u
n
t
r
i
e
s
[1]
–
[3]
.
V
a
r
i
o
u
s
p
r
o
b
l
e
m
s
w
i
t
h
E
M
R
s
y
s
t
e
m
i
m
p
l
e
m
e
nt
a
t
i
o
n
h
a
v
e
b
e
e
n
r
e
p
o
r
t
e
d
,
s
u
c
h
a
s
t
h
o
s
e
r
e
p
o
r
t
e
d
b
y
E
b
b
e
r
s
e
t
a
l
.
[4]
r
e
c
o
r
d
i
n
g
m
e
d
i
c
a
l
r
e
c
o
r
ds
c
a
n
i
n
c
r
e
a
s
e
t
h
e
b
u
r
d
e
n
o
n
d
o
c
t
o
r
s
.
M
o
r
e
s
p
e
c
i
f
i
c
a
l
l
y
,
i
n
I
n
d
o
n
e
s
i
a
:
"
t
h
e
g
o
v
e
r
n
m
e
n
t
h
a
s
r
e
g
u
l
a
t
e
d
t
h
e
i
m
p
l
e
m
e
nt
a
t
i
o
n
o
f
E
M
R
s
y
s
t
e
m
s
,
h
o
w
e
v
e
r
,
s
p
e
c
i
f
i
c
r
u
l
e
s
a
r
e
n
e
e
d
e
d
t
o
r
e
g
u
l
a
t
e
t
h
e
i
m
p
l
e
m
e
n
t
a
t
i
o
n
i
t
"
[5]
,
t
he
dev
el
opment
of
it
is
c
urre
ntly
c
on
ce
ntra
te
d
on
a
sin
gl
e
insti
tuti
on
[6]
,
I
ndonesi
a
is
in
the
pro
cess
of
dev
el
op
i
ng
it
to
rep
la
ce
ma
nual
sy
ste
ms
wit
h
el
ect
r
on
ic
al
te
rn
at
ives
or
to
est
ablish
a
ne
w
sy
ste
m
[1]
.
I
n
2
0
1
9
,
2
.
8
%
o
f
h
o
s
p
i
t
a
l
h
e
a
l
t
h
f
a
c
i
l
i
t
i
e
s
h
a
d
a
l
r
e
a
d
y
a
d
o
p
t
e
d
i
t
,
a
n
d
i
t
w
a
s
a
l
s
o
r
e
p
o
r
t
e
d
t
h
a
t
o
f
t
h
o
s
e
7
8
h
o
s
p
i
t
a
l
s
,
m
a
n
y
s
t
i
l
l
n
e
e
d
e
d
t
o
i
m
p
l
e
m
e
nt
i
t
[
7]
.
The
c
halle
ng
e
s
enc
ounte
red
i
n
the
im
pl
ementat
ion
of
it
ste
m
from
issue
s
relat
ed
to
in
f
rastr
uctur
e
,
st
and
a
r
d
oper
at
ing
proce
dure
s
(SOPs
),
in
adequate
c
od
i
ng
qual
it
y,
s
ys
te
m
integrati
on,
ho
sp
it
al
gov
e
rnan
ce, ser
vice e
rro
rs,
a
nd a
pp
li
cat
ion
bugs
[8]
.
A
t
a
t
i
m
e
w
h
e
n
E
M
R
s
y
s
t
e
m
s
i
m
p
l
e
m
e
n
t
a
t
i
o
n
p
r
o
b
l
e
m
s
w
e
r
e
s
t
i
l
l
e
m
e
r
gi
n
g
,
s
e
v
e
r
a
l
r
e
s
e
a
r
c
h
e
r
s
h
a
d
wr
i
t
t
e
n
t
h
e
r
e
s
u
l
t
s
o
f
t
h
e
i
r
s
t
ud
i
e
s
r
e
g
a
r
d
i
n
g
t
h
e
n
e
e
d
f
o
r
p
a
t
i
e
n
t
s
e
r
v
i
c
e
s
f
r
o
m
b
e
i
n
g
p
r
o
v
i
d
e
r
-
c
e
n
t
e
r
e
d
t
o
b
e
i
n
g
e
x
p
a
n
d
e
d
t
o
p
a
t
i
e
n
t
-
c
e
n
t
e
r
e
d
[9]
.
T
h
e
s
e
e
x
t
e
n
s
i
o
n
s
a
r
e
k
n
o
w
n
a
s
i
n
t
e
g
r
a
t
e
d
h
o
m
e
c
a
r
e
(
I
H
C
)
[10]
a
n
d
h
o
m
e
Evaluation Warning : The document was created with Spire.PDF for Python.
In
t J
Elec
&
C
omp E
ng
IS
S
N:
20
88
-
8708
Timed
co
nc
ur
r
ent system
mo
de
li
ng
and
ve
rif
ic
ation of
home
ca
re
p
l
an
(
Ace
p
T
ar
y
ana
)
871
c
a
r
e
p
l
a
n
(
H
C
P
)
a
c
c
o
r
d
i
n
g
t
o
[
11]
.
B
o
t
h
s
y
s
t
e
m
s
c
a
n
b
e
c
o
n
n
e
c
t
e
d
t
o
t
h
e
h
o
s
p
i
t
a
l
m
e
d
i
c
a
l
r
e
c
o
r
d
f
a
c
i
l
i
t
i
e
s
,
t
h
u
s
i
m
p
r
o
v
i
n
g
t
h
e
a
d
o
p
t
i
o
n
o
f
E
M
R
s
y
s
t
e
m
s
[
12]
.
O
n
e
e
x
a
m
p
l
e
o
f
a
p
a
t
i
e
n
t
-
c
e
nt
e
r
e
d
s
e
r
v
i
c
e
i
s
a
H
C
P
.
G
a
n
i
e
t
a
l
.
[1
1]
s
t
a
t
e
t
h
a
t
t
h
e
f
o
r
m
u
l
a
t
i
o
n
f
o
r
t
h
e
sp
eci
ficat
i
on
s
of
home
c
are
pla
ns
is
ch
al
le
ng
in
g
f
or
s
ever
al
reasons:
care
pl
ans
are
in
her
e
ntly
no
ns
tr
uctu
red
processes
t
hat
involve
re
petit
ive
act
ivit
i
es
bu
t
ar
e
irre
gu
la
r
and re
quire c
omplex
tem
pora
l expressi
on
s
.
H
C
P
i
s
a
n
e
x
a
m
p
l
e
o
f
a
r
e
a
l
-
t
i
m
e
s
y
s
t
e
m
o
r
s
o
f
t
w
a
r
e
w
i
t
h
c
o
n
c
u
r
r
e
n
t
p
r
o
c
e
s
s
e
s
.
Q
u
a
l
i
t
y
s
o
f
t
w
a
r
e
m
u
s
t
m
e
e
t
r
e
l
i
a
bi
l
i
t
y
,
p
e
r
f
o
r
m
a
n
c
e
,
a
n
d
e
a
s
e
o
f
u
s
e
[
13]
.
E
r
r
o
r
s
a
n
d
b
u
g
s
a
r
e
m
a
j
o
r
s
o
f
t
w
a
r
e
p
r
o
b
l
e
m
s
t
h
a
t
c
a
n
c
a
u
s
e
p
l
a
n
e
c
r
a
s
h
e
s
,
d
i
s
r
u
p
t
s
p
a
c
e
s
h
u
t
t
l
e
m
i
s
s
i
o
n
s
,
a
n
d
e
v
e
n
s
t
o
p
t
r
a
d
i
n
g
o
n
t
h
e
s
t
o
c
k
m
a
r
k
e
t
.
A
r
i
a
n
e
’
s
r
o
c
k
e
t
l
a
u
n
c
h
c
r
a
s
h
e
d
d
u
e
t
o
a
f
l
o
a
t
i
n
g
-
p
o
i
n
t
o
v
e
r
f
l
o
w
,
a
b
u
g
t
h
a
t
c
a
u
s
e
d
t
h
e
c
r
a
s
h
[14]
.
T
h
e
c
a
u
s
e
o
f
t
h
e
b
u
g
i
s
a
d
e
a
d
l
o
c
k
[15],
[
16]
.
C
o
n
d
i
t
i
o
n
s
s
u
c
h
a
s
d
e
a
d
l
o
c
k
,
s
t
a
r
v
a
t
i
o
n
,
a
n
d
i
n
c
o
n
s
i
s
t
e
n
c
y
m
u
s
t
b
e
p
r
e
v
e
n
t
e
d
a
s
e
a
r
l
y
a
s
p
o
s
s
i
b
l
e
[15],
[17]
.
G
a
n
i
e
t
a
l
.
[1
1]
h
a
v
e
d
i
s
c
u
s
s
e
d
t
h
e
f
o
r
m
a
l
m
o
d
e
l
i
n
g
a
n
d
v
e
r
i
f
i
c
a
t
i
o
n
o
f
H
C
P
p
r
o
b
l
e
m
s
,
b
u
t
i
t
s
t
i
l
l
n
e
e
d
s
t
o
a
d
d
r
e
s
s
t
h
e
i
s
s
u
e
o
f
d
e
a
d
l
o
c
k
c
o
n
d
i
t
i
o
n
s
.
A
s
m
e
n
t
i
o
n
e
d
a
b
o
v
e
,
d
e
a
d
l
o
c
k
s
c
a
us
e
s
o
f
t
w
a
r
e
b
ug
s
t
h
a
t
m
u
s
t
b
e
r
e
s
o
l
v
e
d
.
I
n
H
C
P
s
y
s
t
e
m
s
,
d
e
a
d
l
o
c
k
s
m
a
y
o
c
c
u
r
i
f
h
e
a
l
t
h
s
e
r
v
i
c
e
s
d
o
n
o
t
p
r
o
v
i
d
e
s
u
f
f
i
c
i
e
n
t
m
e
d
i
c
a
l
p
e
r
s
o
n
n
e
l
t
o
p
r
o
v
i
d
e
p
a
t
i
e
nt
c
a
r
e
a
t
h
o
m
e
.
T
h
e
o
p
e
r
a
t
i
o
n
o
f
a
n
H
C
P
s
y
s
t
e
m
r
e
q
u
i
r
e
s
g
u
a
r
a
n
t
e
e
s
a
s
a
q
u
a
l
i
t
y
c
r
i
t
e
r
i
o
n
i
n
t
e
r
m
s
o
f
d
e
ve
l
o
p
m
e
n
t
a
n
d
o
p
e
r
a
t
i
o
n
.
A
n
H
C
P
m
u
s
t
b
e
f
r
e
e
o
f
s
o
f
t
w
a
r
e
b
u
g
s
.
I
n
t
h
i
s
p
a
p
e
r
,
w
e
d
i
s
c
u
s
s
H
C
P
m
o
d
e
l
i
n
g
a
n
d
v
e
r
i
f
i
c
a
t
i
o
n
f
r
o
m
t
h
e
p
e
r
s
p
e
c
t
i
v
e
o
f
s
c
h
e
d
u
l
i
n
g
d
a
t
a
o
p
e
r
a
t
i
o
n
a
l
i
z
a
t
i
o
n
.
H
o
w
c
a
n
p
a
t
i
e
n
t
s
o
b
t
a
i
n
s
e
r
v
i
c
e
s
a
t
h
o
m
e
t
o
a
v
o
i
d
s
c
h
e
d
u
l
i
n
g
c
o
n
f
l
i
c
t
s
w
i
t
h
p
r
o
v
i
d
e
r
s
s
u
c
h
a
s
do
c
t
o
r
s
a
n
d
n
u
r
s
e
s
?
E
a
c
h
p
a
t
i
e
nt
'
s
b
u
s
i
n
e
s
s
p
r
oc
e
s
s
e
s
a
r
e
u
n
i
q
u
e
a
n
d
m
a
y
b
e
c
o
m
p
l
e
x
a
s
t
h
e
y
a
d
a
p
t
t
o
t
h
e
p
a
t
i
e
nt
'
s
c
i
r
c
u
m
s
t
a
n
c
e
s
.
E
a
c
h
p
r
o
p
o
s
e
d
c
a
s
e
r
e
q
u
i
r
e
s
a
b
u
s
i
n
e
s
s
pr
o
c
e
s
s
m
o
d
e
l
t
o
b
e
c
he
c
k
e
d
t
o
d
e
t
e
r
m
i
n
e
w
h
e
t
h
e
r
i
t
c
a
n
s
a
t
i
s
f
y
t
he
r
e
q
u
e
s
t
.
T
h
e
s
y
s
t
e
m
m
u
s
t
p
r
o
v
i
d
e
t
h
e
b
e
s
t
b
u
s
i
n
e
s
s
p
r
o
c
e
s
s
f
l
o
w
t
o
s
e
r
v
e
p
a
t
i
e
n
t
s
.
T
h
e
r
e
i
s
a
l
o
t
o
f
l
i
t
e
r
a
t
u
r
e
t
h
a
t
h
a
s
i
n
v
e
s
t
i
g
a
t
e
d
i
m
p
r
o
v
i
n
g
b
u
s
i
n
e
s
s
p
r
o
c
e
s
s
m
o
d
e
l
i
n
g
,
f
o
r
e
x
a
m
p
l
e
,
u
s
i
n
g
p
e
t
r
i
n
e
t
s
[
1
8]
b
u
s
i
n
e
s
s
p
r
o
c
e
s
s
m
o
d
e
l
i
n
g
a
n
d
n
o
t
a
t
i
o
n
(
B
P
M
N
)
,
a
n
d
u
n
i
f
i
e
d
m
o
d
e
l
i
n
g
l
a
n
gu
a
g
e
(
U
M
L
)
[
19]
,
a
n
d
c
o
n
f
o
r
m
a
n
c
e
c
h
e
c
k
i
n
g
u
s
i
n
g
g
r
a
p
h
d
a
t
a
b
a
s
e
s
[2
0]
.
H
o
w
e
v
e
r
,
r
e
s
e
a
r
c
h
e
r
s
c
h
o
s
e
t
o
u
s
e
t
i
m
e
d
a
u
t
o
m
a
t
a
m
o
d
e
l
i
n
g
f
o
r
t
h
e
H
C
P
p
r
o
b
l
e
m
b
e
c
a
u
s
e
t
i
m
e
d
a
u
t
o
m
a
t
a
c
a
n
b
e
f
o
r
m
e
d
t
h
r
o
u
g
h
U
M
L
s
t
a
t
e
-
m
a
c
h
i
n
e
t
r
a
n
s
l
a
t
i
o
n
[21
]
,
w
h
i
c
h
i
s
h
e
l
p
f
u
l
f
o
r
a
u
t
o
m
a
t
i
o
n
d
e
v
e
l
o
p
m
e
n
t
.
T
h
e
o
t
h
e
r
a
d
v
a
n
t
a
g
e
o
f
t
i
m
e
d
a
u
t
o
m
a
t
a
i
s
t
h
a
t
t
h
e
y
c
a
n
m
o
d
e
l
c
o
m
p
l
e
x
s
y
s
t
e
m
s
,
u
n
l
i
k
e
p
e
t
r
i
n
e
t
s
[2
2]
.
W
e
p
r
o
p
o
s
e
a
m
e
t
h
o
d
t
o
m
o
d
e
l
a
n
d
v
e
r
i
f
y
H
C
P
.
T
h
e
s
t
u
d
y
a
i
m
s
t
o
d
e
v
e
l
o
p
a
n
d
v
e
r
i
f
y
t
h
e
s
e
p
l
a
n
s
s
o
t
h
e
y
a
r
e
f
l
e
xi
b
l
e
f
or
p
a
t
i
e
nt
s
t
o
c
r
e
a
t
e
a
h
o
m
e
c
a
r
e
p
l
a
n
a
n
d
m
o
r
e
a
c
c
e
s
s
i
b
l
e
f
o
r
t
h
e
c
o
o
r
d
i
n
a
t
o
r
t
o
c
o
n
t
r
o
l
t
h
e
c
o
l
l
i
s
i
o
n
a
n
d
m
o
n
i
t
o
r
t
h
e
u
s
e
o
f
l
i
m
i
t
e
d
r
e
s
o
u
r
c
e
s
.
A
p
a
r
t
f
r
o
m
b
e
i
n
g
a
n
e
x
a
m
p
l
e
o
f
r
e
a
l
-
t
i
m
e
s
o
f
t
w
a
r
e
,
H
C
P
c
a
n
a
l
s
o
b
e
c
r
i
t
i
c
a
l
s
o
f
t
w
a
r
e
[23]
i
n
h
e
a
l
t
h
s
e
r
v
i
c
e
s
b
e
c
a
u
s
e
t
h
e
r
e
a
r
e
c
r
u
c
i
a
l
a
s
p
e
c
t
s
o
f
t
h
e
s
e
q
u
e
n
c
e
o
f
e
v
e
n
t
s
a
n
d
t
i
m
i
n
g
(
n
o
t
s
p
e
e
d
o
f
p
e
r
f
o
r
m
a
n
c
e
)
[
2
4
]
a
n
d
e
r
r
o
r
s
o
r
b
u
g
s
t
h
a
t
c
a
n
h
a
v
e
a
c
r
i
t
i
c
a
l
i
m
p
a
c
t
o
n
p
a
t
i
e
n
t
s
.
B
a
s
e
d
o
n
t
h
e
d
e
a
d
l
o
c
k
p
o
t
e
n
t
i
a
l
t
h
a
t
c
a
u
s
e
s
b
u
g
s
a
n
d
c
r
i
t
i
c
a
l
s
y
s
t
e
m
s
,
w
e
c
o
n
d
u
c
t
e
d
a
s
t
u
d
y
t
o
c
o
n
t
r
i
b
u
t
e
t
o
t
h
e
f
o
r
m
a
l
v
e
r
i
f
i
c
a
t
i
o
n
o
f
t
h
e
h
e
a
l
t
h
c
a
r
e
s
e
c
t
o
r
.
T
h
e
p
r
o
p
o
s
e
d
s
o
l
u
t
i
o
n
s
a
r
e
a
s
f
o
l
l
o
w
s
:
i)
for
mu
la
te
requir
ements
an
d
s
pecifica
ti
ons;
ii
)
m
od
el
co
nc
urren
t
processes
us
in
g
ti
med
a
utomat
a;
and
ii
i)
employ
UP
P
AA
L
f
or
ver
if
ic
at
ion
.
N
ote:
UP
P
A
AL
is
a
forma
l
modeli
ng
a
nd
ver
ific
at
io
n
t
ool
f
or
ti
med
a
uto
mata
-
bas
ed
sy
ste
m
s
that
al
lows
us
to
ve
rify
prop
e
rtie
s
us
i
ng
te
mp
oral
lo
gic
[25]
.
T
h
i
s
p
a
p
e
r
e
x
p
l
o
r
e
s
f
o
r
m
a
l
m
e
t
h
o
d
s
f
o
r
m
o
d
e
l
i
n
g
a
n
d
v
e
r
i
f
y
i
n
g
H
C
P
.
F
o
r
t
h
i
s
p
u
r
p
o
s
e
,
w
e
m
o
d
e
l
i
t
u
s
i
n
g
t
i
m
e
d
a
u
t
o
m
a
t
a
.
T
h
e
m
o
d
e
l
e
n
c
o
m
p
a
s
s
e
s
a
h
o
m
e
c
a
r
e
p
l
a
n
,
a
c
o
u
n
t
e
r
v
a
r
i
a
b
l
e
,
a
n
d
a
m
e
d
i
c
a
l
s
t
a
f
f
a
u
t
o
m
a
t
o
n
.
W
e
p
r
e
s
e
n
t
t
w
o
p
r
o
p
o
s
e
d
v
e
r
i
f
i
c
a
t
i
o
n
m
e
t
h
o
d
s
.
T
h
e
f
i
r
s
t
a
p
p
r
o
a
c
h
w
a
s
m
o
d
e
l
e
d
u
s
i
n
g
a
c
o
u
n
t
e
r
v
a
r
i
a
b
l
e
a
u
t
o
m
a
t
o
n
,
w
h
i
l
e
t
h
e
s
e
c
o
n
d
u
s
e
d
a
m
e
d
i
c
a
l
s
t
a
f
f
a
u
t
o
m
a
t
o
n
.
W
e
h
a
n
d
l
e
o
n
l
y
p
o
s
t
o
p
e
r
a
t
i
ve
a
n
d
d
i
a
b
e
t
i
c
w
o
u
n
d
c
a
r
e
c
a
s
e
s
.
I
n
t
h
r
e
e
s
t
a
g
e
s
,
w
e
c
a
r
r
i
e
d
o
u
t
o
u
r
r
e
s
e
a
r
c
h
s
t
u
d
y
.
Id
en
ti
fy
in
g
a
com
patible
healt
hcar
e
sy
st
em
f
or
im
plem
enting
HCPs
is
the
init
ia
l
ste
p.
H
om
e
ca
re
he
al
th
ser
vice
s
ys
te
ms
a
re
ide
ntifie
d
in
the
seco
nd
s
ta
ge.
T
he
HCP
is
fo
r
mall
y
m
od
el
e
d
in
the
t
hir
d
sta
ge.
T
he
final
sta
ge
ve
r
ifie
s
the
reach
a
bili
ty,
sat
isfact
ion
,
in
var
ia
nce,
an
d
certai
nty
of
t
he
pro
pose
d
a
ut
om
at
a
with
U
PPAAL.
T
he
ver
ific
at
io
n
res
ults
are
ei
ther
sat
isf
ying
or unsati
sf
yin
g.
T
he
rest
of
the
pa
per
is
orga
nized
as
fo
ll
ows:
s
ect
io
n
2
def
i
nes
t
he
for
mali
sm
of
the
requireme
nts
and
s
pecifica
ti
on
s
,
model,
a
nd
UP
P
AAL
ver
ific
at
io
n.
S
ect
ion
3
disc
usse
s
the
st
udy
res
ults,
i
nclu
ding
t
he
form
ulati
on
of
re
quireme
nts
and
s
pecifica
ti
on
s
of
HCP
,
c
on
st
ru
ct
io
n
of
home
ca
re
pat
te
rn
s,
m
odel
in
g
f
or
li
mit
ed
res
ourc
e
sync
hron
iz
at
i
on,
a
nd
ve
rif
yin
g
the
a
utomat
a
of
HCP
us
in
g
UP
P
A
AL.
S
ect
ion
4
pr
es
en
ts
the
study’s c
on
cl
usi
on
s
.
2.
METHO
D
In
this
sect
io
n,
we
discuss
t
he
f
ormal
iz
at
ion
of
HCP
syst
ems.
The
case
stu
dy
us
e
d
w
as
relat
ed
t
o
po
st
operati
ve
and
diabeti
c
wou
nd
ca
re.
Additi
on
al
l
y,
we
ha
ve
a
dd
e
d
a
pr
ocess
s
ynch
r
on
iz
at
io
n
aspect,
a
novelty
for
synch
r
on
iz
in
g
s
ome
ti
med
aut
oma
ta
for
home
care
pla
n
sy
s
te
ms,
so
t
hat
processes
ca
n
avo
i
d
dead
l
oc
ks
[
16]
. T
he
re
searc
h desig
n
i
nvolv
e
s forma
li
zi
ng
ti
med system
s a
nd UPP
AA
L
verific
at
ion.
Evaluation Warning : The document was created with Spire.PDF for Python.
IS
S
N
:
2088
-
8708
In
t J
Elec
&
C
omp E
ng,
V
ol.
15
, No
.
1
,
Febr
uary
20
25
:
870
-
8
82
872
2.1. F
orma
li
z
ing
timed sys
t
ems
In
ge
ner
al
,
veri
ficat
ion
is
a
s
te
p
to
fi
nd
a
model
(
)
that
meet
s
the
s
pec
ific
at
ion
(
)
in
a
formal
la
nguag
e
,
⊨
(1)
(r
ea
d
"
sat
isfie
s
").
I
n
this
pa
pe
r,
w
e
pr
opos
e
modeli
ng
a
ho
me
ca
re p
la
n. Home
ca
re
is
a
ne
w
ser
vice
t
ha
t
su
pp
or
ts
E
M
R
s
y
s
t
e
m
s
.
In
te
grat
ing
home
c
are
ser
vices
w
it
h
EMR
s
y
s
t
e
m
s
is
crit
ic
al
because
ma
ny
urge
nt
op
e
rati
ons
or
proces
ses
th
reat
en
sa
fety
[
26]
.
Home
ca
re
is
a
lso
a
s
ys
te
m
th
at
has
ti
me
d
re
qu
i
reme
nts
tha
t
can
b
e
cl
ea
rly
sta
te
d
[
11]
an
d
can
be
seen
as
a
re
al
-
ti
me
s
ys
te
m
in
wh
ic
h
there
are
c
oncu
rr
e
nt
processes
[27],
[
28]
that
re
quire
modeli
ng
us
in
g
ti
me
d
a
ut
oma
ta
[
11]
.
P
r
op
e
r
home
ca
re
i
nvolv
es
m
od
el
in
g
an
d
prepa
rin
g
sp
eci
ficat
io
ns
t
hat
incl
ud
e
the
ti
me
as
pect
in
th
e
discuss
i
on.
Acc
ordin
g
t
o
Gan
i
et
al.
,
ti
med
a
uto
mat
a
can
model an
exa
m
ple home
care
sy
ste
m
(as
a
)
[
11]
.
In
ad
diti
on,
spe
ci
ficat
ion
s
a
re
prepa
re
d
more
preci
sel
y
us
i
ng
ti
me
d
c
omp
ut
at
ion
al
tree
lo
gic
(
TCTL)
[29]
.
T
he
ver
i
ficat
ion
ste
ps
include
i)
de
ve
lop
in
g
re
qu
ir
ements
a
nd
s
pe
ci
ficat
ion
s;
ii
)
de
vel
op
i
ng
t
imed
models;
an
d
ii
i)
ver
if
ying t
he mo
dels. Eac
h s
te
p
is e
xp
la
ine
d
in
s
ub
sect
io
ns 2.1.
1, 2.
1.2,
a
nd 2.1.3
.
2.1.1
Requ
ir
e
ments an
d s
pe
ci
ficat
io
ns
First,
re
gardin
g
t
he
de
velo
pme
nt
of
re
qu
ir
ements
an
d
s
pe
ci
ficat
ion
s,
in
the
case
of
ti
med
s
ys
te
ms,
we
us
e
TCTL
-
base
d
s
peci
fic
at
ion
s.
A
n
exa
mp
le
of
a
ti
med
require
ment
for
a
hom
e
ca
r
e
unit
is
as
f
ol
lows
:
Accor
ding
to
Neal
[
30]
,
pos
top
e
rati
ve
wou
nd
care
ada
pts
to
the
locat
io
n
of
t
he
wou
nd:
i)
th
e
crit
er
ia
for
treat
ing
sur
gical
w
ounds
on
the
face
are
3
t
o
5
da
ys
;
ii
)
sur
gical
w
ounds
on
t
he
scal
p
a
nd
a
rm
s
f
or
7
t
o
10
da
ys
;
ii
i)
sur
gical
wounds
on
the
c
he
st,
st
om
ac
h,
hands
,
a
nd
le
gs
f
or
10
–
14
da
ys
;
a
nd
i
v)
s
urgical
wou
nd
s
on
t
he
palms
of
the
hands
a
nd
feet
for
14
to
21
da
ys
.
Pati
ents'
home
ca
re
requi
reme
nts
di
ff
e
r
from
tho
se o
f
hosp
it
al
serv
ic
es. Ho
me
care
is
re
p
e
ti
ti
ve,
un
str
uct
ur
e
d
(
re
gu
la
r
a
nd
ir
re
gu
la
r)
,
a
nd
s
pecific
to
c
ertai
n
patie
nts.
T
he
s
pecifica
ti
ons
a
re
de
te
rmine
d
base
d
on
ti
me
inf
or
mati
on
e
xpress
ed
as
a
quad
r
up
le
t
(
da
ys,
ti
me
ranges,
per
i
od,
durati
on)
[
11]
.
We
will
c
on
du
ct
a
s
urvey,
c
ollec
t
data,
and
pr
e
pa
re
re
qu
i
reme
nts
for
home
care se
rv
ic
es
at
one
of the
gove
rnment
hosp
it
al
s in
the
B
an
yumas
D
ist
rict
.
2.1.2 Ti
med
m
od
el
s
The
sec
ond
in
vo
l
ves
dev
el
oping
ti
med
sy
st
em
models.
T
he
the
ory
unde
rlying
the
de
velo
pm
e
nt
o
f
ti
med
s
ys
te
m
sp
eci
ficat
io
ns
,
s
pecifica
ll
y,
us
in
g
ti
med
a
uto
mata
,
is
e
xpla
ined
i
n
mor
e
de
ta
il
in
a
previ
ou
s
pap
e
r
[
31]
.
Ga
ni
et
al.
def
i
ne
d
aut
om
at
a
m
odel
s
as
f
ollo
ws
,
especial
ly
for
modeli
ng
a
ho
me
care
plan
i
ns
ide
ti
med
aut
om
at
a
[
11]
. De
finiti
on 1 (
Au
t
om
at
a). A
uto
mata
=
(
,
0
,
,
,
,
,
,
,
,
)
wh
e
re
:
−
S
is
a
finite
set
of
the
locat
io
ns
or
sta
te
s
of
th
e
aut
om
at
on
;
0
i
s
the
init
ia
l
sta
te
;
F
⊆
S
is
t
he
final
sta
te
;
W
⊆
S
is
the set
of
wait
ing
sta
te
s
;
E
⊆
S
is t
he
set
of e
xecu
te
d
sta
t
es
;
St
⊆
S
is st
a
rt stat
es
;
−
is a fi
nite set
of tra
ns
it
ion l
ab
el
s inclu
ding
{
};
−
is a fi
nite set
of cloc
ks
;
−
:
⟶
(
)
,
w
hich
a
sso
ci
at
es an
i
nv
a
ria
nt in
eac
h st
at
e of the
au
t
om
at
on
;
−
⊆
×
×
(
)
×
2
×
is a tran
sit
ion
s
et
.
Ba
sed
on
def
i
niti
on
1,
we
c
on
st
ru
ct
tw
o
a
uto
mata
t
o
m
odel
patie
nt
ca
r
e
and
nur
se
or
phys
ic
ia
ns
serv
ic
es
.
To
model
these
t
wo
i
ns
ta
nces
,
sever
al
c
onditi
on
s
nee
d
to
be
obser
ved,
s
uc
h
as
sc
heduling
a
nd
arr
a
ng
e
ments
with
li
mit
ed
re
so
urces
e.
g.
,
nurses
a
nd
ph
ysi
ci
ans.
T
her
e
f
ore,
we
disc
us
s
the
s
yn
c
hro
niz
at
ion
set
ti
ng
s
for
the
r
es
ources,
whi
ch
a
re e
xp
la
in
e
d
as
foll
ows.
The
sync
hron
i
zat
ion
a
ppr
oac
h
betwee
n
pro
cesses
in
the
model
is
im
ple
mented
us
in
g
t
wo
met
hods
:
i)
one
a
utomat
on
use
s
s
ha
red
global
var
ia
bl
es
[
32]
–
[
34]
;
a
nd
ii
)
tw
o
aut
oma
tons
a
re
s
ynch
r
on
iz
e
d
(
∥
)
us
in
g
process
s
yn
c
hron
i
zat
io
n:
"se
nder
!"
a
nd
"
rec
ei
ver
?"
[
25]
.
T
he
f
irst
meth
od
us
es
a
globa
l
var
ia
ble
t
o
m
anag
e
li
mit
ed
res
our
ces.
Dinsdal
e
-
You
ng
et
al.
[
33]
us
e
th
e
sema
phore
and
c
ounter
var
ia
ble
to
m
anag
e
con
c
urre
ncy.
F
ur
t
her
m
ore,
Ci
ci
rell
i
and
Nigr
o
[
32]
sta
te
the
sema
phor
e
usi
ng
a
c
ounter
va
riable
in
the M
orris
al
gorithm.
The
seco
nd
meth
od
e
xp
la
ins
ho
w
the
t
wo
aut
oma
tons
co
mm
un
ic
at
e
s
yn
c
hr
onously
.
F
or
e
xam
ple,
a
la
mp
a
uto
ma
ton
c
ommu
nic
at
es
with
the
use
r
aut
om
at
on.
Accor
ding
to
def
i
niti
on
1,
t
he
la
mp
a
uto
ma
ton
has
the
at
trib
ute
S
=
{
off
,
low
,
bri
g
ht
}
,
y
cl
ock
is
wr
i
tt
en
as
X
=
{
y
}
,
w
herea
s
the
use
r
a
uto
mat
on
has
the
at
tribu
te
S
=
{
idle
}
.
The
b
eha
viors of
th
e
auto
mata
are
as
f
ollow
s: If
the u
ser
presses
a
butt
on
in
Fig
ur
e 1
t
hat
is
identifie
d
wi
th
"p
ress!
"
as
a
sen
der
(i.e.
,
it
sy
nc
hro
nizes
with
"p
ress?"
a
s
a
receive
r,
t
he
la
mp
is
tu
r
ne
d
on,
as
s
how
n
i
n
Figure
2
).
I
n
ad
diti
on
,
t
he
us
e
r
pr
e
sses
the
butt
on
rand
om
l
y
at
a
ny
ti
me
or
do
es
no
t
press
th
e
bu
tt
on
at
al
l.
T
he
cl
oc
k
y
o
f
t
he
la
mp
is
us
e
d
to
detect
w
hether
the
us
e
r
is
movin
g
(
y
<
5
)
qu
i
ckly
or
slo
w
(
≥
5
).
We
us
e
t
his
co
nce
pt
to
ma
nag
e
li
mit
ed
re
so
urces
f
or
the
home
care
s
yst
em,
wh
ic
h
will
be
disc
us
se
d
in the ne
xt sect
ion
.
T
he
fi
rst a
nd sec
ond
s
ync
hro
nizat
ion
me
thods a
re c
o
m
bi
ned
.
Evaluation Warning : The document was created with Spire.PDF for Python.
In
t J
Elec
&
C
omp E
ng
IS
S
N:
20
88
-
8708
Timed
co
nc
ur
r
ent system
mo
de
li
ng
and
ve
rif
ic
ation of
home
ca
re
p
l
an
(
Ace
p
T
ar
y
ana
)
873
Fu
rt
hermo
re,
we
al
so
dev
el
oped
a
reacti
ve
home
care
al
gorith
m
w
hile
c
reati
ng
a
home
care
model
us
in
g
a
uto
mat
a.
The
pur
pos
e
of
ps
e
udoc
ode
is
to
e
nhan
ce
read
e
rs
’
co
mprehe
ns
io
n
of
aut
om
at
on
be
hav
i
or
thr
ough
co
de.
This
c
od
e
incl
ud
e
s
se
qu
e
ntial
instru
ct
io
ns
t
hat
can
be
i
nte
rpreted
c
oncu
r
ren
tl
y
[
35]
.
Th
eref
or
e
,
this al
gorith
m
can s
olv
e
a
sim
il
ar p
r
oble
m.
2.1.3. M
od
el
ve
ri
ficat
i
on
A
f
ormal
ve
rifi
cat
ion
a
ppro
ac
h
is
a
s
ys
te
mat
ic
method
for
ens
ur
in
g
t
hat
a
sy
ste
m
or
m
odel
meet
s
it
s
sp
eci
ficat
io
ns
and
prop
e
rtie
s.
This
ap
proac
h
us
es
mat
hema
ti
cal
log
ic
,
for
mali
sms,
a
nd
f
ormal
anal
ys
is
to
ols
[25],
[
29]
,
[
36]
,
[
37]
.
I
n
gen
e
r
al
,
the
ob
je
ct
iv
e
of
f
ormal
veri
ficat
ion
is
to
pro
ve
or
care
fu
l
ly
chec
k
w
heth
er
a
sy
ste
m
or m
odel
co
nfo
rms t
o specifie
d re
quireme
nts.
I
n (
1)
,
rep
re
sents t
he
model,
w
hile
is t
he pr
op
e
rtie
s
or sp
eci
ficat
ion
s.
Figure
1. Use
r a
uto
mat
on
Figure
2. Lam
p
a
uto
mat
on
2.2. U
PPA
AL
v
eri
fic
at
i
on
Pr
e
vious
resea
rch
that
util
iz
ed
UP
P
A
AL
i
nc
lud
e
d
modeli
ng
a
nd
ve
rifica
ti
on
us
in
g
U
PP
AA
L
[
32]
to
formall
y
ver
i
fy
dea
dlo
c
k
-
fr
ee
as
well
as
safe
ty
an
d
r
esp
ons
e
pro
per
ti
es
e
xpress
ed
i
n
TC
TL
us
i
ng
an
e
xisti
ng
model
chec
ke
r,
e.
g.,
U
PP
A
AL
[
38]
,
facil
it
at
es
automatic
conver
si
on
of
ver
i
fied
ti
med
a
utomat
a
-
base
d
models
(in
UPPA
AL)
[39]
.
UP
P
A
AL
is
a
world
wide
-
fa
mous
m
od
el
c
heck
i
ng
t
oo
l
f
or
ti
med
a
utomat
a
[
40]
.
UP
P
A
AL
ti
me
d
a
uto
mata
ta
ke
advanta
ge of vali
datio
n
an
d verificat
io
n
s
uppo
rt in
th
e UP
PAAL to
ol
[41
]
. We
us
e t
he
f
ollo
wing formula t
o
c
heck the
model
[
25],
[
42]
:
−
<
>
∅
(
Possi
bl
y
∅
, i.e.,
a stat
e exists
wh
e
re
∅
holds
)
−
[]
∅
(
Invar
ia
ntly
∅
,
eq
uiv
al
e
nt to
no
t
<
>
not
∅
)
−
[]
∅
(
P
otentia
ll
y al
way
s
∅
, i.e.,
a
sta
te
p
at
h
e
xist
s over w
hich
∅
alw
ays
hol
ds
)
−
<
>
∅
(
Alw
ays
ev
e
nt
ually
∅
,
eq
ui
valent to
not
[]
∅
not
∅
)
−
∅
⟶
(
∅
al
way
s lea
ds
to
,
eq
uiv
al
e
nt
to
[
](
∅
im
plies
<
>
)
)
3.
RESU
LT
S
AND
DI
SCUS
S
ION
3.1.
Requ
ir
eme
nt
s
a
n
d sp
eci
fica
t
ions of
h
ome c
are p
l
an
s
Su
r
ve
y
res
ults:
a
hos
pital
in
Ba
nyum
as
D
is
tric
t
has
dev
el
op
e
d
home
ca
r
e
par
ti
cularl
y
f
or
treat
in
g
diabeti
c
a
nd
posto
per
at
ive
w
ounds.
T
he
se
rv
ic
e
is
sim
ple:
patie
nts
re
gi
ste
r
f
or
treat
ment
v
ia
a
s
pe
ci
fic
Wh
at
s
A
pp,
an
d
the
n
the
nur
s
ing
te
am
ap
pro
ves
the
patie
nt
for
the
visit
.
O
ne
e
xam
ple
of
the
re
qu
i
reme
nt
s
for
patie
nts
par
ti
ci
pating i
n
t
he H
CP is as
fo
ll
ow
s:
a.
Diabeti
c
wou
nds
we
re
treat
e
d
daily
f
or
a
pproximat
el
y
7
t
o
10
da
ys
.
W
ound
treat
me
nt
ti
me
s
can
dep
e
nd
on
patie
nt
a
va
il
abili
ty.
F
or
e
xam
ple,
Pati
en
t_1
:
e
ve
ry
day
f
rom
1
to
10
Oct
ob
e
r
20
23,
Pati
ent
_2:
li
ke
Pati
ent_1,
but
there
are
othe
r
restrict
io
ns
;
namely
,
visit
s
are
hel
d
ev
ery
08.
00
a
m.
Pati
ent_3
:
Li
ke
Pati
ent_2, t
here are e
xce
ptions, name
ly
,
e
xc
ept on
4 Octo
be
r 202
3
at
12.30 noo
n.
b.
Po
sto
pe
rati
ve
wou
nd
ca
re
a
da
pts
t
o
t
he
l
oc
at
ion
of
t
he
w
ound:
T
he
crit
eria
f
or
t
reati
ng
surgical
w
ound
s
on
t
he
face
ar
e
approximat
el
y
3
t
o
5
days,
su
r
gical
w
ounds
on
the
scal
p
an
d
ar
ms
ap
pro
ximate
ly
7
–
1
0
days,
s
urgical
w
ounds
on
t
he
c
hest,
st
oma
ch,
ha
nds,
a
nd
le
gs
f
or
a
pproximat
el
y
10
to
14
da
ys,
a
nd
su
r
gical
wo
unds o
n
t
he palms
of the
ha
nd
s
and
feet f
or ap
prox
imat
el
y 14
–
21 d
a
ys
[
30]
.
Sp
eci
fical
ly,
r
egardin
g
the
s
pecifica
ti
ons
f
or
diabetes
an
d
posto
per
at
i
ve
w
ound
se
rv
i
ces,
patie
nt
sp
eci
f
ic
at
io
ns
wer
e
pr
e
pa
red
base
d
on
the
requireme
nts
sta
te
ments
exp
la
ine
d
in
t
he
introd
uction.
The
sentences
ar
ra
nged
in
a
set
of r
eq
uireme
nts have w
or
ds
t
hat ex
press
te
mpo
r
al
it
y,
su
c
h
as
"
every d
a
y,
"
"
f
or
te
n
days,"
an
d
"
from
08.00
to
20.00".
Re
qu
i
r
ements
al
s
o
ha
ve
di
ff
e
ren
t
t
imes
than
regular
on
es
(e
xc
ept).
Exam
ple:
Pati
ent_
3
plan
ne
d
to
treat
diabet
es
w
ounds
f
rom
10/
01
/
23
to
10/1
0/23
e
ve
r
y
m
orni
ng
ex
c
ept
on
10
/
04
/
23 at 1
2.30. E
xam
ples
of Pati
ent
_
1
a
nd Pati
ent
_2 are
in
Ta
ble
1.
Evaluation Warning : The document was created with Spire.PDF for Python.
IS
S
N
:
2088
-
8708
In
t J
Elec
&
C
omp E
ng,
V
ol.
15
, No
.
1
,
Febr
uary
20
25
:
870
-
8
82
874
The
c
on
st
ru
ct
i
on
of
the
requirem
e
nts
se
ntence
f
or
post
op
e
rati
ve
wou
nd
ca
re
is
presented
i
n
qu
a
dru
plet
f
orm
in
Table
2.
Exam
ple:
Pati
ent_
3
plan
ne
d
treat
ment
by
r
ecei
vin
g
rei
nfo
rceme
nt
dressi
ng
an
d
daily
i
nject
ion
act
ivit
ie
s
exc
ept
for
10/0
4/2
3.
E
ach
act
ivit
y
re
qu
ire
s
a
treat
me
nt
ti
me
of
a
pp
roxi
mate
l
y
30 min
.
Table
1.
Sp
eci
f
ic
at
ion
of acti
vi
ti
es "d
ia
betic
w
ou
nd
s"
for an
y pati
ents
Patien
ts
Activ
ity
Day
s
Tim
e
r
an
g
es
Period
Du
ration
Patien
t_
1
Ch
an
g
es in
diab
eti
c wou
n
d
ban
d
ag
es
Every d
ay
Morn
in
g
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
Patien
t_
2
Ch
an
g
es in
d
iab
eti
c wou
n
d
ban
d
ag
es
Every d
ay
Morn
in
g
,
0
8
.00
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
Patien
t_
3
Ch
an
g
es in
diab
eti
c wou
n
d
ban
d
ag
es
Every d
ay
excep
t
(10
/0
4
/2
3
)
Morn
in
g
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
1
0
/0
4
/
2
3
1
2
.30
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
Table
2.
Sp
eci
f
ic
at
ion
of
act
iv
it
ie
s "p
os
to
pe
r
at
ive woun
ds
"
for
a
ny p
at
ie
nt
s
Patien
ts
Activ
ity
Day
s
Tim
e
r
an
g
es
Period
Du
ration
Patien
t_
1
Rein
force
d
ressin
g
Every d
ay
Morn
in
g
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
Patien
t_
2
Rein
force
d
ressin
g
Every d
ay
Morn
in
g
,
0
8
.00
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
Patien
t_
3
Rein
force
d
ressin
g
Every d
ay
excep
t (
1
0
/0
4
/
2
3
)
Morn
in
g
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
Injectio
n
1
0
/0
4
/
2
3
1
2
.30
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
3.2. H
CP pa
tter
n
HCP
patte
r
ns
can
be
cat
eg
ori
zed
int
o
t
hr
ee
disti
nct
ty
pes
:
daily
care
pa
tt
ern
s,
relat
ive
daily
ca
re
patte
rn
s
on
s
pecific
dates,
and
a
bs
ol
ute
patte
rn
s
on
c
ertai
n
dates.
The
f
ocu
s
of
this
st
udy
is
on
t
he
sp
eci
ficat
io
ns
and
de
velo
pme
nt
of
a
uto
ma
ta
that
util
iz
e
the
first
t
wo
c
at
egories
of
H
CP
patte
r
ns
.
These
patte
rn
s
w
il
l
be
ela
borated
up
on in
t
he
s
ubse
qu
e
nt s
ubsect
ion
.
3.2.1 E
very d
ay
pa
t
tern
This
pa
tt
ern
r
epr
ese
nts
a
pa
ti
ent's
need
to
visit
the
hos
pi
ta
l
daily
in
th
e
morni
ng,
e
ve
ning,
or
at
certai
n
ti
mes,
s
uch
as
09
:
00.
Table
3
s
pecifi
es
visit
s
f
or
pa
ti
ents
with
dia
betes
to
rec
ei
ve
medical
proc
edures
su
c
h
as
"
diabe
ti
c
wound
ca
re
"
an
d
"i
nject
io
n".
Fig
ur
e
3
s
hows
a
n
eve
ryday
patte
r
n
a
ut
om
at
on
for
tr
eat
in
g
patie
nts
with
di
abetes,
wh
ic
h refe
rs
to
the
spe
ci
ficat
ion
s i
n Table
1
.
Table
3.
E
xa
m
ples
of
"
diabeti
c woun
ds
”
Activ
ity
Day
s
T
im
e
r
an
g
es
Period
Du
ration
Tr
eatin
g
wou
n
d
s
Every d
ay
Morn
in
g
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
Injectio
n
Every d
ay
0
9
:0
0
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
20
Wou
nd
treat
m
ent
was
pla
nn
e
d
e
ve
ry
m
orni
ng
f
r
om
10/0
1/
2023
t
o
10/1
0/2
02
3,
an
d
inje
ct
ion
act
i
vity
was
car
ried
out
eve
r
y
da
y
sta
r
ti
ng
at
09
:
00.
Transi
ti
on
1
e
xpla
ins
that
i
nje
ct
ion
act
ivit
y
c
an
be
gin
at
9:00,
an
d
transiti
on
2
e
xpla
ins
t
hat
w
ound
t
reatment
act
ivit
y
be
gin
s
after
injec
ti
on.
I
nject
ion
can
be
pe
rformed
aft
e
r
wou
nd
treat
me
nt,
a
s
s
how
n
in
tra
ns
it
ion
s
5
a
nd
7.
T
he
a
utomat
a
res
et
s
the
da
y
cl
oc
k
val
ue
(
)
e
very
u
p
to
1
,
440
min
ut
es
(one d
a
y)
.
A
ll
po
ssible
sc
he
du
le
s o
f
injec
ti
on
a
nd
treat
in
g
wou
nd
act
ivit
ie
s
acce
ptable
t
o
the
automata
incl
ud
e
"(treat
i
ng
w
ound,
480)
,
(i
nject
ion
,
540),
(inject
io
n,
19
80),
(trea
ti
ng
wou
nd,
2001)
,
(Inject
ion
,
40
6620
)
" i
n
a ce
rtai
n
pe
rio
d.
Figure
3. Dia
be
ti
c auto
mata
f
or
“
eve
ry d
a
y patt
ern
”
Evaluation Warning : The document was created with Spire.PDF for Python.
In
t J
Elec
&
C
omp E
ng
IS
S
N:
20
88
-
8708
Timed
co
nc
ur
r
ent system
mo
de
li
ng
and
ve
rif
ic
ation of
home
ca
re
p
l
an
(
Ace
p
T
ar
y
ana
)
875
3.2.2. Rel
ati
ve
da
ys
patte
rn
with
ex
ceptio
n
Durin
g
maki
ng
a
home
care
plan,
the
patie
nt
de
te
rmine
s
t
he
da
y
of
the
visit
.
H
oweve
r
,
s
om
e
visit
s
are
for
bidden
on
s
pecific
dat
es.
For
i
ns
ta
nc
e,
posto
per
at
iv
e
patie
nts
ma
y
sel
ect
a
T
hurs
day
visit
ser
vi
ce
f
or
te
n
da
ys
(
10
/
01/2
3
to
10/1
0/23)
e
xce
pt for 1
0/04/2
3.
Table
4
e
xp
la
in
s the
sp
eci
ficat
io
ns
of
t
he home ca
re p
la
n
for
posto
per
at
i
ve
act
ivit
ie
s,
inclu
ding
rein
f
or
ci
ng
dr
essi
ng
a
nd
i
nject
ion
.
Both
act
ivit
ie
s
we
re
c
onduct
ed
within
60
min
utes
on
T
hurs
da
ys
e
xcep
t
f
or
10
/
04
/
23.
Fig
ure
4
s
hows
t
he
automata
act
i
vity
pla
n.
T
ransi
ti
on
s
1,
2,
3,
an
d
4
sta
te
Saturd
a
y,
S
unda
y,
Monda
y,
a
nd
T
ue
sd
a
y,
res
pecti
vely.
T
ra
ns
it
io
ns
5
a
nd
8
e
xe
cute
injec
ti
on
a
nd
r
ei
nfor
ce
dressi
ng
act
ivit
ie
s,
wh
ic
h
la
st
f
or
a
ma
ximum
of
60
min
utes
i
n
lo
cat
io
ns
1
a
nd
2
.
Transi
ti
on
7
is
a
transiti
on
to
accom
moda
te
the
date
ex
cepti
on
"
10/0
4/
23
".
T
ra
ns
it
io
ns
10
a
nd
11
sta
te
act
ivit
ie
s
for
Wednes
da
y
a
nd
F
rida
y,
re
sp
e
ct
ively.
Here,
t
ran
sit
io
n
12
re
pr
ese
nts
a
n
act
ivit
y
to
reset
the
da
y
and
we
ek
cl
oc
ks
,
an
d
t
ran
sit
i
on
13
resets
th
e
da
y
cl
ock.
T
he
final
tra
ns
it
ion
is
tra
ns
it
io
n
14,
w
hich
re
presents
the tra
ns
it
ion a
t t
he
en
d o
f
loc
at
ion
4
.
Table
4.
E
xa
m
ples
of
“
posto
pe
rati
ve wou
nd
care
”
Activ
ity
Day
s
Tim
e
r
an
g
es
Period
Du
ration
Rein
force
d
ressin
g
Thu
rsd
ay
excep
t(10
/0
4
/2
3
)
Morn
in
g
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
Injectio
n
1
0
/0
4
/
2
3
—
1
0
/0
1
/
2
3
-
1
0
/1
0
/2
3
30
3.3. Li
mi
ted
r
esou
rce
synch
roniza
tio
n
Home
ca
re
pr
a
ct
ic
es
le
ad
to
t
he
joi
nt
use
of
li
mit
ed
res
our
ces.
Home
car
e
may
res
ult
in
strug
gle
o
r
com
petit
ion
f
or
res
ources.
Limi
te
d
res
ource
s
for
home
ca
r
e
include
hom
e
care
medical
equ
i
pm
e
nt
an
d
healt
h
workers
li
ke
nurses
a
nd
doct
or
s
.
T
o
a
ddress
this
i
ssu
e
,
we
first
model
t
he
li
mit
at
ion
of
nurses
’
res
ource
s.
Due
to
the
fact
t
ha
t
healt
hca
re
w
orkers’
res
our
ces
are
li
mit
ed
,
s
ynch
ronizat
ion
is
nece
ssar
y
w
hen
patie
nt
s
us
e
home
ca
re
s
er
vi
ces.
F
or
exa
m
ple,
five
patie
nt
s
are
plan
ni
ng
home
care
with
only
t
wo
nur
ses
a
vaila
ble
on
t
he
same
da
y,
at
t
he
same
ti
me
,
or
at
differe
nt
ti
mes.
Desig
ning
an
aut
oma
ton
t
o
ha
ndle
resou
rce
co
nt
ention
pro
blems
is
an
excit
ing
c
halle
ng
e
.
Tables
1
and
2
s
how
the
plans
of
ma
ny
patie
nts
for
home
care
ser
vic
es
for
diabeti
c a
nd po
stop
e
ra
ti
ve wound t
reatment.
Pati
ents
w
ho
a
re
plan
ning
tre
at
ment
m
us
t
i
mmediate
ly
re
cei
ve
c
onfirma
ti
on
of
the
av
ai
la
bili
ty
of
serv
ic
es
acc
ordin
g
to
thei
r
sc
heduled
a
ppoi
ntment.
The
ti
med
a
uto
mat
on
in
Fi
gure
4
r
egu
la
te
s
po
st
operati
ve
wou
nd
care
.
A
uto
mata
sti
ll
n
eeds
t
o
discuss
mana
gi
ng
the
li
mit
ed
avail
ab
il
it
y
of
medica
l
per
s
onnel
to
serv
e
the
ma
ny
a
nd
var
ie
d
patie
nt
care
pla
ns
.
W
he
n
a
patie
nt
pl
ans
home
care
,
the
aut
om
at
a
mu
st
be
a
ble
to
ch
eck
the possi
bili
ty
of a r
el
ia
ble
sc
hedule to
avoi
d
sc
he
du
li
ng c
olli
sion
s
.
To
overc
om
e
the
c
onflic
t
in
t
he
us
e
of
me
di
cal
sta
ff
res
our
ces,
we
propos
e
two
a
ppro
ac
hes.
I
n
th
e
first a
ppro
ac
h,
we desi
gn t
he a
uto
mata
as
fo
l
lows
.
a.
In
c
rease
t
he
ne
ed
for
me
dical
pe
rs
onnel
t
o
e
ns
ure
a
s
ynch
r
on
iz
at
io
n
betw
een
home
care
ser
vices
a
nd
t
he
avail
abili
ty of
medical
per
s
on
nel.
b.
A
gl
ob
al
var
ia
ble
that
detect
s
medical
us
e
,
f
or
e
xam
ple,
is
the
va
riable.
It
init
ia
ll
y
has
th
e
valu
e
of
the
numb
e
r
of
me
dical
sta
f
f,
dec
reases
by
one
if
a
patie
nt
has
us
e
d
it
,
and
inc
reases
by
on
e
a
gain
i
f
a
patie
nt has fi
ni
sh
e
d usin
g
it
.
Figure
4. P
os
to
per
at
ive
wo
und
ca
re fo
r
"rela
ti
ve
patte
r
n"
Evaluation Warning : The document was created with Spire.PDF for Python.
IS
S
N
:
2088
-
8708
In
t J
Elec
&
C
omp E
ng,
V
ol.
15
, No
.
1
,
Febr
uary
20
25
:
870
-
8
82
876
The
first
a
utomat
on
desig
n
base
d
on
t
he
li
te
ratur
e
[
34]
guara
ntees
co
rrec
t
seq
ue
ntial
and
te
m
poral
log
ic
.
T
his
is
a
relat
ively
sim
ple
strat
eg
y
f
or
mana
ging
the u
se o
f
li
mit
ed
r
eso
ur
ces
.
I
n
thi
s
pro
po
sal
,
onl
y
one
automat
on
is
a
rr
a
ng
e
d,
an
d
t
he
a
vaila
bili
ty
of
home
care
s
erv
ic
es
is
ex
pressed
a
s
a
global
co
unte
r
va
riable.
Figure
5
e
xp
l
ai
ns
the
sync
hro
nizat
ion
of
care
a
nd
ava
il
abili
ty
of
m
edical
pe
r
son
ne
l
serv
ic
es
us
i
ng
the
var
ia
ble
with
a
ma
ximum
nu
mb
e
r
of
me
dic
al
perso
nnel
of
2
pe
ople
(
=
2
).
H
om
e
care
ser
vi
ces
sta
rt
f
rom
08.
00
t
o
11.00
eve
r
y
wee
k.
The
va
riable
re
pr
e
se
nts
the
cl
oc
k
f
or
the
da
y,
a
nd
represe
nts
the
week
l
y
cl
oc
k.
Figure
5. S
yn
c
hro
nizat
ion
of
act
ivit
y
us
i
ng a
va
riable
The
sec
ond
a
ppr
oach
us
es
a
sy
nc
hro
nizat
ion
met
hod
be
tween
the
ho
me
care
a
utomat
on
a
nd
a
medical
sta
ff
a
uto
mat
on.
I
n
t
his
case,
we
discuss
t
he
main
te
nan
ce
act
ivit
ie
s
for
po
st
op
e
r
at
ive
wou
nd
ca
re,
as
in
Fi
gure
4
,
by
a
ddin
g
sen
di
ng
"ser
ve
!"
s
yn
c
hro
nizat
ion
at
t
ran
sit
io
ns
5
a
nd
8.
T
he
n,
we
c
reate
a
ne
w
automat
on
t
o
s
yn
c
hro
nize
t
he
a
vaila
bili
ty
of
me
dical
se
r
vices
in
Fig
ur
es
6
an
d
7,
res
pe
ct
ively.
T
he
a
ddit
ion
of
s
ynch
r
on
iz
a
ti
on
met
hods
for
s
ource
a
uto
mata
re
fers
to
the
UPPA
A
L
instr
uctions
[
26]
an
d
the
us
e
of
sen
der
a
nd
rec
ei
ver
se
map
hor
es in
UP
P
A
AL
[
33]
.
Figure
6. M
e
di
cal
staff
a
utom
at
on
f
or
posto
pe
rati
ve wou
nd
s
The
t
wo
a
pproaches
e
nsure
t
hat
the
te
m
por
al
log
ic
is
gua
r
anteed,
that
re
al
iz
abili
ty
is
achieve
d,
an
d
that
it
can
dete
ct
dead
l
oc
ks
.
To
desc
ribe
t
he
pro
gr
e
ss
of
the
process
,
we
de
velo
ped
a
n
al
gorithm
t
o
e
xp
la
in
the
a
uto
mat
on
sync
hro
nizat
ion
process.
A
lgorit
h
m
1
co
ntains
a
n
al
go
rithm
t
hat
de
monstrate
s
us
i
ng
the
va
riable f
or c
oncu
rr
e
nc
y
in
th
e home ca
re a
ut
om
at
on.
Figure
7
.
Auto
mate
d home ca
re
plan
a
utoma
ton
f
or
posto
pe
rati
ve wou
nd
s
Evaluation Warning : The document was created with Spire.PDF for Python.
In
t J
Elec
&
C
omp E
ng
IS
S
N:
20
88
-
8708
Timed
co
nc
ur
r
ent system
mo
de
li
ng
and
ve
rif
ic
ation of
home
ca
re
p
l
an
(
Ace
p
T
ar
y
ana
)
877
Algorith
m
2
presents
t
he
co
nc
urren
c
y
of
the
process
f
orme
d
from
t
he
t
wo
aut
om
at
a
in
F
igure
6
a
nd
Figure
7.
T
he
t
wo
a
utomat
a
c
om
m
unic
at
e
usi
ng
a
se
r
ving
c
hannel
to
obta
in
pe
rmissi
on
t
o
use
"I
nject
io
n"
an
d
"R
ei
nf
orce
_dre
ssing
"
ser
vices
f
rom
me
dical
per
s
onnel's
li
mit
ed
res
ources
.
The
va
riable
represe
nt
s
the av
ai
la
ble c
apacit
y of me
di
cal
p
ers
onnel.
Algorith
m
1
. C
on
c
urre
ncy in
a home ca
re al
gorithm
u
si
ng
"counter"
v
a
riable
Program
Homecare_1
{
=
{
1
,
2
,
3
}
with
1
th
e
in
it
ia
l
st
at
e
an
d
=
{
4
}
is
fi
na
l
st
at
e.
=
{
,
,
}
wi
th
,
,
represents
a
duration
clock,
day
clock,
week
clock,
and
a
period
clock
in
minutes,
respectively.}
{ Global Declaration For Variables, Constants, and Primitives }
: Integer,
: Integer {Max = 2}
Proced
ure
Homecare_post_everyday()
{Local Variable Declaration}
,
,
: Clock
{ Algorithm :}
Repeat
=
0
1
:
While (
< 480)
+
+
Endwhile
While
(
<
660
)
AND
≥
)
+
+
or break {Optional because it is a non deterministic
\
}
Endwhile
=
0
+
+
2
:
=
0
While
(
<
60
)
+
+
Endwhile
−
−
3
:
Until (
> 1440) AND
(
>
10080
)
4
:
{Main Program}
=
0
{ Resources of nurses or doctors}
Patient1=Homecare_post_everyday() { Patient1 instantiation }
Patient2=Homecare_post_everyday() { Patient2 instantiation }
Patient3=Homecare_post_everyday(
) { Patient3 instantiation }
Patient4=Homecare_post_everyday() { Patient4 instantiation }
Patient5=Homecare_post_everyday() { Patient5 instantiation }
Patient6=Homecare_post_everyday() { Patient6 instantiation }
Patient7=Homecare_post_everyday() { Patient7 instantiation }
Patient8=Homecare_post_everyday() { Patient8 instantiation }
End of the template
Algorith
m
2.
C
on
c
urre
ncy in
a home ca
re al
gorithm
u
si
ng
sy
nc
hro
nizat
io
n
Program
Homecare_2
=
{
0
,
1
,
2
,
3
}
with
0
the
in
itial
state
a
nd
=
{
4
}
is
final
state.
=
{
,
,
,
}
with
,
,
,
represents
a
duration
clock,
day
clock,
week
clock,
and
a
period
clock,
in
minutes,
respectively.
{ Global Declaration For Variables, Constants, and Primitives }
: Chan {Channel for synchronization}
Procedure
Post_services()
{Local Variable Declaration}
: Clock
{ Algorithm :}
Repeat
Idle
:
While
(
?
)
OR
(
>
1
)
=
0
,
+
+
Endwhile
Injection :
=
0
Evaluation Warning : The document was created with Spire.PDF for Python.
IS
S
N
:
2088
-
8708
In
t J
Elec
&
C
omp E
ng,
V
ol.
15
, No
.
1
,
Febr
uary
20
25
:
870
-
8
82
878
While
(
≤
30
)
+
+
Endwhile
Reinforce_dressing :
=
0
While
≤
30
)
+
+
Endwhile
−
−
Until TRUE
Procedure
Care_plan_post_except_syn()
{Local Variable Declaration}
,
,
,
: Clock
{ Algorithm :}
=
0
Repeat
=
0
Repeat
=
0
Repeat
0
:
if
(
1
in
Figure
) then transition_1
if (
2
in
Figure
) then transition_2
if
(
3
in
Figure
) then transition_3
if (
4
in
Figure
) then transition_4
if (
7
in
Figure
) then transition_7
if (
10
in
Figure
) then transition_10
if (
11
in
Figure
) then tran
sition_11
if (
5
in
Figure
) then
While (NOT
)
Injection(), Re
inforce_dressing()
Endwhile
1
:
=
0
While (
<
60
)
+
+
if (
8
in
Figure
) then
While (NOT
)
Injection(), Reinforce_dressing()
Endwhile
2
:
=
0
While
(
<
60
)
+
+
3
:
Until
(
>
1440
)
Until
(
>
1440
>
10080
)
Until
(
>
1440
>
407520
)
4
:
{Main Program}
S1=Post_Services() {S1 instantiation }
Patient5=Care_plan_post_except_syn(
) { Patient5 instantiation }
Patient6=Care_plan_post_except_syn() { Patient6 instantiation }
Patient7=Care_plan_post_except_syn(). { Patient7 instantiation }
Patient8=Care_plan_post_except_syn()
{ Patient8 instantiation }
End of Template
3.4. F
orma
l
analy
sis o
f
c
are
plan
s
usin
g time
d
au
t
om
ata
Figure
8
de
pi
ct
s
the
i
ns
ta
nt
ia
ti
on
of
the
ei
gh
t
patie
nts
us
in
g
t
he
te
m
plate
aut
om
at
a
sho
wn
in
Figure
5.
Eig
ht
patie
nts
wer
e
plan
ned
t
o
rec
ei
ve
home
care
with
a
li
mit
ed
num
be
r
of
me
dical
per
s
onnel
(t
wo
people)
.
T
he
a
ver
a
ge
me
dical
ser
vice
ta
kes
a
maxim
um
o
f
60
min
utes.
Simi
la
r
to
Fi
gure
8,
we
al
s
o
si
mu
la
te
the
insta
ntiat
ion
of
4
Ca
re_p
la
n_post_e
xce
p_
s
yn
a
utomat
a
co
ns
ist
ing
of
Pati
ent
5,
Pati
ent
6,
Pati
ent
7,
an
d
Pati
ent
8
a
nd a
Po
st_
ser
vices a
uto
mat
on, nam
el
y
1
.
Af
te
r
descr
i
bin
g
a
nd
sim
ulati
ng
t
he
a
utomat
a,
the
next
ste
p
is
to
ve
rify
the
properti
es
of
t
he
pro
po
se
d
a
utomat
a
model.
A
ll
mo
delin
g
a
nd
ve
rificat
io
n
s
te
ps
us
e
the
U
PPAAL
t
oo
l
[4
3]
.
We
t
ried
to
check
the
m
od
el
s
ho
wn
in
Fi
gures
6
a
nd
7.
Re
a
chab
il
it
y
c
hec
ks
a
re
ex
press
ed
as
fo
ll
ows:
<
>
(
5
.
4
)
&&
(
6
.
4
)
&&
(
7
.
4
)
&&
(
8
.
4
).
All
pr
op
e
rtie
s
in
Fig
ur
e
9
a
re
sat
isfie
d.
T
he
refor
e
,
sta
te
4
(f
inal
sta
te
)
can
be reache
d t
h
r
ough tra
ns
it
ion
s
that
pass
t
hro
ugh
se
ve
ral stat
es, and
no
dead
l
ock o
c
cu
r
s.
Evaluation Warning : The document was created with Spire.PDF for Python.
In
t J
Elec
&
C
omp E
ng
IS
S
N:
20
88
-
8708
Timed
co
nc
ur
r
ent system
mo
de
li
ng
and
ve
rif
ic
ation of
home
ca
re
p
l
an
(
Ace
p
T
ar
y
ana
)
879
Figure
8. A
utomat
a instanti
at
ion f
or eig
ht p
at
ie
nts u
si
ng s
ynchro
nizat
ion
c
ounter
v
a
riable
Figure
9. Re
achab
il
it
y
c
hec
kin
g f
or the
sync
hro
nizat
ion
a
ppr
oac
h of
t
wo
automata
4.
CONCL
US
I
O
N
The
crit
ic
al
it
y
of
t
he
home
care
syst
em
w
as
ad
dr
esse
d
by
pro
posin
g
two
a
ppr
oach
e
s.
The
firs
t
appr
oach
use
s
a
c
ounter
vari
able,
a
nd
the
seco
nd
a
ppr
oa
ch
us
es
s
yn
c
hro
nizat
ion
wi
th
a
sen
de
r
-
re
cei
ver
channel.
T
he
main
f
oc
us
of
HCP
disc
us
se
d
in
thi
s
pa
per
i
s
diabeti
c
an
d
po
st
operati
ve
wou
nd
ca
re.
Mod
el
in
g
of
patie
nts
w
ho
reg
ist
ere
d
f
or
home
ca
re
is
m
od
el
e
d
us
in
g
ti
me
d
a
utom
at
a.
Th
e
ti
me
a
uto
mata
are
de
sign
e
d
Evaluation Warning : The document was created with Spire.PDF for Python.