Information Technology Reference
In-Depth Information
Note that in this system specification, the functional and performance aspects
of each individual component are separated, as well as the specifications of the
components themselves.
3IMCAn ly s
Assume that the IMC under consideration is complete, i.e., it is not subject any
further to interaction with other components that are modeled as IMCs. This is
important, as this means that actions cannot be further delayed due to a delay
which is imposed by the environment. Formally, this means that we can safely
hide all actions in the IMC at hand, i.e., we consider
I\
A where A contains
all actions occuring in
. Accordingly, all actions are labeled by τ . The typical
specification that is subject to analysis is thus of the form:
I
(
I 1 || A 1 I 2 || A 2
...
|| A N I N )
\
A
i =1
where A is the union of all actions in IMC
Act i . Due to the
maximal progress assumption, the resulting IMC can be simplified: in any state
that has a τ -transition, all Markovian transitions can be removed. Subsequently,
sequences of τ -transitions can be collapsed by applying weak bisimulation. If
nondeterminism is absent in the resulting IMC, in fact a CTMC remains, and
all analysis techniques for CTMCs can be employed [34], such as transient or
steady-state analysis or CSL model checking [2].
I i , i.e., A =
Time-bounded reachability. An alternative analysis technique is to compute time-
bounded reachability probabilities. This does not require the IMC to be reducible
to a CTMC, and can thus be applied to any IMC. Let us explain the kind of
measure we are interested in. First, consider infinite paths in an IMC. An infinite
path π in an IMC is an infinite sequence of the form
σ 0 ,t 0
σ 1 ,t 1
σ 2 ,t 2
π = s 0
−−−−→
s 1
−−−−→
s 2
−−−−→
...
with s i
,and t i R 0 .Theoc-
currence of action α after a delay of t time units in state s i in π is denoted by
s i
S , σ i is either an action in
Act
or equals
α,t
−−−→
s i +1 ; in case of a Markovian transition after t time units delay, this is de-
noted by s i ⊥,t
s i +1 . As internal interactive transitions take place immediately,
their occurrence is denoted s i
−−−→
τ, 0
R 0 ,let π @ t denote
the sequence of states that π occupies at time t .Notethat π @ t is in general not
a single state, but rather a sequence of several states, as an IMC may exhibit
immediate transitions and thus may occupy various states at the same time in-
stant. An example path in the IMC of Fig. 1 is s 0 ⊥, 3 . 0
−−−→
s i +1 .Fortimepoint t
s 1 ⊥, 2 . 0
β, 0
−−−→
−−−−→
−−−−→
s 2
s 4 ...
ω ( s )denotethe
set of infinite paths starting in state s . Using a standard cylinder construction,
a sigma-algebra can be defined over the set of infinite paths of an IMC, and can
be equipped with a probability measure [66], denoted Pr in the sequel.
which occupies the states s 2 and s 4 at time instant 5.0. Let
Paths
 
Search WWH ::




Custom Search