Information Technology Reference
In-Depth Information
m is defined on the structure of the sHML formula:
Definition 6 (Synthesis).
m
def
= λ
ff
x env .
fail !
y pid1 =spw ϕ
m (x env ) , y pid2 =spw ψ
m (x env ) ,
λ
x env .
m
def
=
ϕ∧ψ
fork (y pid1 ,
y pid2 )
rcv tr(
stop end
m
m (x env );
def
= λ
[
α
]
ϕ
x env .
α
)
→ ϕ
m
m , y mon (
{ X ,
def
= λ
max ( X
)
x env .
y mon =
ϕ
y mon }
: x env )
m
y mon =lookUp ( X ,
def
= λ
X
x env .
x env ) , y mon (x env )
Auxiliary Function definitions and meta-operators:
x pid1 !z , x pid2 !z end, y rec (x pid1 ,
def
= μ
fork
y rec
(x pid1 ,
x pid2 )
.
rcv z
x pid2 )
μ
y rec
(x var ,
x map )
.
case x map of (
{
x var ,
z mon }
: )
z mon
: z tl
y rec (x var ,
z tl )
def
=
lookUp
nil exit
end
In Def. 6, the monitor for the formula ff immediately reports a violation to some
supervisor actor identified as fail , handling the violation. Conjunction,
ϕ 1 ∧ϕ 2 ,trans-
ϕ 2 and subsequently forwarding
any trace messages to these spawned monitors through the auxiliary function fork .The
translated monitor for [
ϕ 1 and
lates into spawning the respective monitors for
α
ϕ
ϕ
]
behaves as the monitor translation for
once it receives a
trace message encoding the occurrence of action
α
, using the function:
tr( i ? v ) def
tr( i ! v ) def
= {
rv
,
i
,
v
}
= {
sd
,
i
,
v
}
Importantly, the monitor for [
α
]
ϕ
terminates if the trace message does not correspond
to
α
. The translations of max ( X
)and X are best understood together. The monitor for
max ( X
) behaves like that for
ϕ
, under the extended map where X is mapped to the
max ( X
monitor for
from Def. 2.
The monitor for X retrieves the respective monitor translation bound to X in the map
using function lookUp , and behaves like this monitor. Closed formulas guarantee that
map entries are always found by lookUp , whereas guarded formulas guarantee that
formula variables, X , are guarded by necessity conditions, [
ϕ
,e
ff
ectively modelling the formula unrolling
ϕ{
)
/ X }
— this implements the
lazy recursive unrolling of formulas and prevents infinite bound-variable expansions.
α
]
ϕ
z pid =spw
m ( nil ) , mLoop (z pid )
def
= λ
x frm .
x frm
Mon
rcv z msg x pid !z msg end, y rec (x pid )
def
= μ
mLoop
y rec
x pid .
Monitor instrumentation, performed through the function Mon (defined above), spawns
the synthesised function initialised to the empty map, nil , and then acts as a message
forwarder to the spawned process, through the function mLoop (defined above), for any
trace messages it receives through the tracing semantics discussed in Sec. 2.
 
Search WWH ::




Custom Search