Dependability analysis of DES based on MARTE and UML state machines models

Abstract

UML (Unified Modeling Language) is a standard design notation which offers the state machines diagram to specify reactive software systems. The “Modeling and Analysis of Real-Time and Embedded systems” profile (MARTE) enables UML with capabilities for performance analysis. MARTE has been specialized in a “Dependability Analysis and Modeling” profile (DAM), then providing UML with dependability assets. In this work, we propose an approach for the automatic transformation of UML-DAM models into Deterministic and Stochastic Petri nets and the subsequent dependability analysis.

Appendix: LDSPN composition operator

In general, more than one label can be associated to a transition (place). However, in the composition of two nets, we actually consider at most one label per transition (place): with this restriction we can use a simplified version of the composition operator (Donatelli and Franceschinis 1996). Given two LDSPN ${\cal LN}_{1} = ({\cal N}_{1},\lambda_{1},\psi_{1})$ and ${\cal LN}_{2} = ({\cal N}_{2},\lambda_{2},\psi_{2})$, the LDSPN ${\cal LN} = ({\cal N},\lambda,\psi)$:

$$ {\cal LN} = {\cal LN}_1 \mathop{|~|}_{L_P,L_T} {\cal LN}_{2} $$

resulting from the composition over the sets of labels L _P and L _T is defined as follows.

Let E _P  = L _P  ∩ ψ ₁(P ₁) ∩ ψ ₂(P ₂) and E _T  = L _T  ∩ λ ₁(T ₁) ∩ λ ₂(T ₂) be the subsets of L _P and of L _T , respectively, comprising place and transition labels that are common to the two LDSPNs, $P_1^l$ ($T_1^l$) be the set of places (transitions) of ${\cal LN}_1$ that are labeled l and $P_1^{E_P}$ ($T_1^{E_T}$) be the set of all places (transitions) in ${\cal LN}_1$ that are labeled with a label in E _P (E _T ). Same definitions apply to ${\cal LN}_2$.

Then: $P = P_1 \backslash P_1^{E_P} \cup P_2 \backslash P_2^{E_P} \cup \bigcup_{l \in E_P} \{P_1^l \times P_2^l \}$, $T = T_1 \backslash T_1^{E_T} \cup T_2 \backslash T_2^{E_T} \cup \bigcup_{l \in E_T} \{ T_1^l \times T_2^l \}$, the functions F ∈ { I(), O(), H() } are equal to:

$$ F(p,t) = \begin{cases} F_1(p,t) & \mathrm{if}\ \ p\in P_1\backslash P_1^{E_P}, t \in T_1\backslash T_1^{E_T}\\ F_1(p,t_1) & \mathrm{if}\ \ p\in P_1\backslash P_1^{E_P}, t \equiv (t_1,t_2) \in \bigcup_{l \in E_T} \{ T_1^l \times T_2^l \}\\ F_1(p_1,t) & \mathrm{if}\ \ p\equiv (p_1,p_2) \in \bigcup_{l \in E_P} \{ P_1^l \times P_2^l \}, t \in T_1\backslash T_1^{E_T}\\ F_2(p,t) & \mathrm{if}\ \ p\in P_2\backslash P_2^{E_P}, t \in T_2\backslash T_2^{E_T}\\ F_2(p,t_2) & \mathrm{if}\ \ p\in P_2\backslash P_2^{E_P}, t \equiv (t_1,t_2) \in \bigcup_{l \in E_T} \{ T_1^l \times T_2^l \}\\ F_2(p_2,t) & \mathrm{if}\ \ p\equiv (p_1,p_2) \in \bigcup_{l \in E_P} \{ P_1^l \times P_2^l \}, t \in T_2\backslash T_2^{E_T}\\ \min \{F_1(p_1,t_1), F_2(p_2,t_2)\} & \mathrm{if}\ \ p\equiv (p_1,p_2) \in \bigcup_{l \in E_P} \{ P_1^l \times P_2^l \},\\ & \ \ \ t \equiv (t_1,t_2) \in \bigcup_{l \in E_T} \{ T_1^l \times T_2^l \}\\ \end{cases} $$

Functions F ∈ {Φ(), Λ() } are equal to:

$$ F(t) = \begin{cases} F_1(t) & \mathrm{if}\ \ t \in T_1\backslash T_1^{E_T}\\ F_2(t) & \mathrm{if}\ \ t \in T_2\backslash T_2^{E_T}\\ F_2(t_2) & \mathrm{if}\ \ t \equiv (t_1,t_2) \in \bigcup_{l \in E_T} \{ T_1^l \times T_2^l \}\\ \end{cases} $$

The initial marking function is equal to:

$$ M^0(p) = \begin{cases} M^0_1(p) & \mathrm{if}\ \ p \in P_1\backslash P_1^{E_P}\\ M^0_2(p) & \mathrm{if}\ \ p \in P_2\backslash P_2^{E_P}\\ M^0_1(p_1) + M^0_2(p_2) & \mathrm{if}\ \ p \equiv (p_1,p_2) \in \bigcup_{l \in E_P} \{P_1^l \times P_2^l \}\\ \end{cases} $$

Finally, the labeling functions for places and transitions are respectively equal to:

$$ \psi(x) = \begin{cases}\psi_1(x) & \mathrm{if}\ \ x \in P_1\backslash P_1^{E_P}\\ \psi_2(x) & \mathrm{if}\ \ x \in P_2\backslash P_2^{E_P}\\ \psi_1(p_1)\cup \psi_2(p_2) & \mathrm{if}\ \ x \equiv (p_1,p_2) \in \bigcup_{l \in E_P} \{P_1^l \times P_2^l \}\\ \end{cases} $$

$$ \lambda(x) = \begin{cases}\lambda_1(x) & \mathrm{if}\ \ x \in T_1\backslash T_1^{E_T}\\ \lambda_2(x) & \mathrm{if}\ \ x \in T_2\backslash T_2^{E_T}\\ \lambda_1(t_1)\cup \lambda_2(t_2) & \mathrm{if}\ \ x \equiv (t_1,t_2) \in \bigcup_{l \in E_T} \{ T_1^l \times T_2^l \}\\ \end{cases} $$

The relation being associative with respect to place superposition, we use also as an n-operand by writing ${\cal LN} = |~|_{\emptyset,L_P}^{k=1,..,K} {\cal LN}_{k}$.