Information Technology Reference
In-Depth Information
adopted the DFT work mentioned above to the recent AADL Error Model An-
nex, and provides a map of each of the components on an I/O-IMC, again in a
fully compositional manner. This is in spirit similar to the work performed in the
ESA project COMPASS [13,14,15], where IMC are targetted to model nominal
and probabilistic fault behaviour, fault propagation and recovery, and degraded
modes of operation. The integration of nominal behavior and error models ba-
sically boils down to a parallel composition of a variable-decorated transition
system (which is a semantically an IMC) and an IMC.
Generalised stochastic Petri nets.
Generalised Stochastic Petri Nets (GSPNs) are
a well-established modelling formalism for performance and dependability eval-
uation, supporting stochastic timed behavior and weighted immediate choices
[54,55]. To this end, timed transitions and immediate transitions are supported
in a GSPN. Performance evaluation of a GSPN proceeds at the level of the
reachability (or: marking) graph. That graph is transformed into a CTMC, for
which ecient steady-state and transient solvers are at hand. This evaluation
trajectory was pioneered by the tool GreatSPN [20], nowadays it is implemented
in a plethora of tools.
However, it is notoriously overlooked that the above evaluation trajectory is
incomplete. It is restricted to
confusion-free
GSPNs. Confusion arises if a firing
sequence admits the simultaneous enabling of multiple non-conflicting immediate
transitions. GSPNs equip immediate transitions with global priority levels and
globally assigned weights to diminish the occurrence of such nondeterministic
choices. But priorities and weights do not, and cannot, eliminate confusion in its
full entirety. The presence of nondeterminism, however, makes it impossible to
associate an unambiguous stochastic process to such nets.
Recently we managed to attack this principal problem [40]. We have taken
up earlier thoughts on nondeterministic GSPN semantics [37] to come up with
an IMC semantics for GSPNs. Actually, this semantics is not more than a re-
interpretation of the marking graph as an IMC. With the analysis results re-
ported in this paper, this means that also confused GSPNs can now be analysed.
This was not possible before.
Example 6.
Consider the GSPN depicted in the figure below on the left where
solid bars depict immediate transitions and open bars represent delayed tran-
sitions. This GSPN is confused. In marking (0
,
0
,
1
,
1), for instance, the set of
reachable tangible markings is
{
(1
,
0
,
0
,
0)
,
(0
,
0
,
0
,
1)
}
. If the enabled transition
t
5
is chosen, the tangible marking (0
,
0
,
0
,
1) is reached almost surely. However, if
enabled transition
t
6
is chosen, we enter the tangible marking (1
,
0
,
0
,
0) almost
surely. Hence, the next tangible markings depends on the way the nondetermin-
ism in (0
,
0
,
1
,
1) is resolved and cannot be quantified. The usual way to deal
with this situation is to equip transitions
t
5
and
t
6
with weigths. The marking
graph of the GSN is depicted in the figure on the right. Here, solid arrows depict
Markovian transitions, and dashed arrows correspond to the firing of immediate
transitions in the net, and are interpreted as
τ
-labeled IMC transitions.
