Information Technology Reference
In-Depth Information
Assumption Truth Maintenance System (ATMS [10]). Precisely, a node label is
a set of environments and an environment is a set of hypotheses. The previous
example will thus involve only one node represented by 1
{
(1
,
2)
,
(3
,
3)
}
where 1
isthenodecore,(1
,
2) and (3
,
3) are both environments, and
{
(1
,
2)
,
(3
,
3)
}
is the
node label. In the following, given a state
t
,weuse
t
n
to denote its corresponding
node core,
t
c
to describe its resulting environment, and
Label
(
G, t
) to refer to
its label in graph
G
.
5.2
Inferring Scenarios with S-TLC
The S-TLC Model Checker is described by Algorithm 1. It employs three data
structures
U
B
. The first refers to the reachability directed graph under
construction generated during forward chaining and backward chaining phase.
The last two are FIFO queues, containing states whose successors have not
being yet computed respectively during forward and backward chaining phases.
The algorithm assumes that a configuration file is done as input, it includes
statements denoting that
Init
is the initial state predicate,
Next
is the next state
relation,
Invariant
is a state-predicate to be satisfied by each reachable state,
and
Inc
is the predicate to be equal false for all states of the system behavior,
it represents the the set of S-TLA inconsistencies. Moreover, the specification is
supposed to be made finite-state. To that effect the configuration file is presumed
to include statements stating that
Constraint
is a predicate that asserts bounds
on the set of reachable states, and
EvidenceState
is a predicate characteristic of
a terminal state representing forensic evidences.
To append a node to the graph under construction, the algorithm uses func-
tion
Append
(
G
,
U
F
and
with a pointer to its
predecessor state
s
. Besides, a state
s
is attached to a FIFO queue
G
, t, t
s
)toaddanode
t
to graph
G
U
using the
function
Append
(
U
, s
) and detached using the function
Tail
(
U
). Moreover, a
node
t
is joined to an existing node
s
inside the graph
G
using the function
Join
(
G
, t
s
). S-TLC works in three phases:
Initialization Phase:
G
,aswellas
U
F
and
U
B
are created and initialized
respectively to empty set
. During this step, each state
satisfying the initial system predicate is computed and then checked whether
it satisfies predicate
Invariant
. In that case, it will be appended to
∅
and empty sequence
after
computing its label, and pointing it to the
null
state. If the state does not
satisfy
EvidenceState
, it will be attached to the unseen queue
G
U
F
,otherwise,
it will be considered as a terminal state and appended to
U
B
in order to be
retrieved in backward chaining phase.
Forward Chaining Phase:
During this phase, the algorithm starts with
U
F
equal to the set of initial system states. Afterwards and until the queue becomes
empty, state
s
(representing the tail of
U
F
) is retrieved and its successor states are
computed. From the latter, for every state (denoted by
t
) satisfying
Constraint
,
if
Invariant
is not satisfied, an error is generated and the algorithm terminates,
otherwise
t
is appended to
G
as follows:
