Information Technology Reference
In-Depth Information
a) Module-Level constructs:
The expression cvariables
v
1
,...,v
n
adds
the declaration of constrained variables, distinguishing them from non-constrained
ones, which remain declarable using variables statement.
b) Non constant S-TLA
+
operators:
Given a constrained variable
h
,we
denote by
h
the value of
h
in the next state. Moreover,
untouched
h
replaces
the expression
h
=
h
c) Constant S-TLA
+
a fictive value to rep-
resent the constrained variable value, before a hypothesis is enunciated.
operators:
we denote by
Standard Form of a S-TLA
+
Specification
4.1
The first part of Figure 3, [5], illustrates a typical S-TLA
+
specification, de-
scribed by module
SpecExpl
. The specified system is described by formula
spec
,
while the initial system state is described by predicate
Init
(no hypotheses are
enunciated as constrained variables
g
and
h
are both equal to
). Action
A
,for
instance, is true for a pair of states
if (1) the value that
t
assigns to
x
is
1 higher than the value that
s
affects to
x
, (2) under the hypothesis
g
=1,
and (3) without
t
being reached under the hypothesis
h
= 2 (by the definition
of inconsistency predicate
Inc
). Finally, the predicate
Evd
describes a relevant
S-TLA
+
system state (a valuation of some system variables) which is of capital
importance especially in fulfilling forensic investigation objectives. Its use will
be demonstrated afterwards in section 4.2.
s, t
⎡
⎣
⎤
⎦
module
SpecExpl
extends
Naturals
variables
x
cvariables
h, g
x
=2
g
=1
h
=
A
⎡
⎣
⎤
⎦
x
=1
g
=1
h
=
B
(
|
=
⊥
φ
)
⎡
⎣
⎤
⎦
A
Init
(
x
=0)
∧
(
g
=
)
∧
(
h
=
)
A
(
g
=1)
∧
(
x
=
x
+1)
∧
untouched
h
B
(
h
=2)
∧
(
x
=
x −
1)
∧
untouched
g
C
(
x
=
x ×
3)
Next
A∨B∨C
Evd
x
=2
Inc
(
g
=1)
∧
(
h
=2)
Spec
x
=3
g
=1
h
=
C
⎡
⎣
⎤
⎦
x
=0
g
=
h
=
(
|
=
⊥
φ
)
A
⎡
⎣
⎤
⎦
⎡
⎣
⎤
⎦
B
x
=
−
1
g
=
x
=
−
2
g
=
B
h
=2
h
=2
Init
∧
[
Next
]
x,g,h
∧
ni
x,g,h
(
Next, Inc
)
⎡
⎣
⎤
⎦
x
=
3
g
=
h
=2
−
C
theorem
Spec
⇒
(
x
∈
Nat
)
Fig. 3.
Standard form of a S-TLA
+
specification and a relative behavior fragment
The second part of Figure 3 describes a fragment from the set of possible
system behaviors relative to formula
Spec
. For a successive execution of
A
fol-
lowed by
B
, two successive hypotheses are generated:
g
” = 1 followed by
h
”=2.