Information Technology Reference
In-Depth Information
distributes μ of s to μ of s such that only related states obtain a positive weight
(3(a)), and the total probability mass of u that is assigned by Δ coincides with
μ ( u ) and symmetrically for u (cf. 3(b), 3(c)).
Theorem 3.
is a precongruence wrt. parallel composition and hiding.
Constraint-oriented specification of performance aspects. Let us conclude this
section by describing how IMCs can be used to meet the challenges as put
forward in the well-known paradigm of separation of concerns. We do so by
showing that IMCs can be naturally used to specify performance aspects in the
so-called constraint-oriented specification style [64]. This style is a format par
excellence to support the separation of concerns principle when specifying the
characteristics of complex distributed systems. It has been originally developed
to support the early phases of the design trajectory. Put in a nutshell, constraints
are viewed as separate processes. Parallel composition is used to combine these
constraints much in the same vein as logical conjunction.
To illustrate how IMCs perfectly match the constraint-oriented specification
style consider a given system model P that does not contain random timing
constraints yet —i.e., P is a labeled transition system— and let α and β be two
successive actions in P . To insert a random delay between these two actions, it
now su ces to construct an IMC D p with an initial state with outgoing transition
α and a final state, i.e. a state without outgoing transitions, that can can only
be reached by a β -transition. The state reached after performing α and the state
from which the β -transition is emanating are connected by a CTMC, i.e., an IMC
with only Markovian transitions. This CTMC models the random delay that we
want to impose on the delay between α and β . The resulting system is now
obtained as P
|| {α,β} D p . The “delay” process D p is thus imposed as additional
constraint to process P . This procedure can now be repeated to impose delays
between other actions in P . As CTMCs can approximate general probability
distributions arbitarily closely, this is a powerful recipe. This is exemplified in
[39] where a complex telephone system specification in LOTOS has been enriched
with performance characteristics using a constraint-oriented specification style.
Now assume that we want to impose random delays on some of the observable
actions from P and Q . Following the procedure just described, this yields
( P
|| A Q )
|| A p ∪A q
( D p || D q )
where A p are the synchronised actions with “delay” process D p and A q the
ones with D q . Note that the timing constraints are added “on top” of the entire
specification. As it su ces to impose a single delay on each action, the processes
D p and D q are independent, and thus need not to synchronise. In case D p
delays some local actions from P ,and D q delays local actions from Q ,theabove
specification can be rewritten into the weak bisimilar specification:
P
|| A p D p
local constraints of P
|| A q D q
local constraints of Q
Q
|| A
 
Search WWH ::




Custom Search