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.
 
Search WWH ::




Custom Search