158
Internet of Things (IoT)
Analyzing the AAL system development with dependability as a function of reliability involves the following eight steps to assure qualitative and quantitative dependability
analysis.
a. Specify UML behavior models
b. Annotate the models.
c. Convert to PRISM language.
d. Compile and check PRISM model.
e. Simulate the model.
f. Define the properties for dependability.
g. Run the properties.
h. Analyze the result.
Steps d to step h use PRISM tool to compose the dependability analysis. Every activity
is modeled after the UML activity diagram (AD). It consists of decision and action nodes,
each representing the execution scenarios as a sequence diagram. Once the ADs and SDs
are completed, the next step is to build the annotation with reliability components and
transition probabilities. The assumptions of the reliability of the components are based
on (i) the reliability of the services performed where the execution time of the invocation
is not considered as a factor, (ii) state of transition which depends on the source state, and
the available transition and its transfer of control between the components is estimated
through Markov Chain property, and (iii) failures of the transition.
An example of annotation in PRISM with component reliability is as follows and shown
in Figure 8.16.
[
] 0
:(
1) (1
): (
2);
notify s
R s
R
s
c
c
= →
′ = + −
′ =
To ensure whether the system is working properly, software design is very essential which
is set before it gets developed. Besides the functional requirements defined through activity and sequence diagram, it also requires nonfunctional requirements to assure the quality of the system developed. AAL systems require activities that are time constrained and
critical. To ensure the nonfunctional requirements of the system, Benghazi et al. (2012) has
modeled a design based on UML-RT that uses timed traces semantic and methodology
to check the timeliness and safety of AAL activity. Petri Nets is used as tool for modeling
semantic and interactive graphical language to develop and verify nonfunctional requirements of the system (Hein et al. 2009; Palanque et al. 2007). Benghazi has used formal
language CSP+T for defining the timed traces semantics of the operations. CSP+T is the
subset of CSP developed by Hoare in 1985. Let P and Q be a process that has defined a set
of events Σ with a ∈ ∑ and B ⊆ ∑ in a time interval [t,t+T].
ٗ
P STOP SKIP
P a
P I T t a P
I T t
P P Q P Q P Q P Q P Q
B
::
|
|0.*
|
|( , ).
| ( , )
|
|
| ; |
| | | |
=
→
∞ν →
→
→
The system is modeled in such a way that the process of target system is divided into
subsystems, each designed through an UML-RT context diagram and interconnected
Internet of Things (IoT)
Analyzing the AAL system development with dependability as a function of reliability involves the following eight steps to assure qualitative and quantitative dependability
analysis.
a. Specify UML behavior models
b. Annotate the models.
c. Convert to PRISM language.
d. Compile and check PRISM model.
e. Simulate the model.
f. Define the properties for dependability.
g. Run the properties.
h. Analyze the result.
Steps d to step h use PRISM tool to compose the dependability analysis. Every activity
is modeled after the UML activity diagram (AD). It consists of decision and action nodes,
each representing the execution scenarios as a sequence diagram. Once the ADs and SDs
are completed, the next step is to build the annotation with reliability components and
transition probabilities. The assumptions of the reliability of the components are based
on (i) the reliability of the services performed where the execution time of the invocation
is not considered as a factor, (ii) state of transition which depends on the source state, and
the available transition and its transfer of control between the components is estimated
through Markov Chain property, and (iii) failures of the transition.
An example of annotation in PRISM with component reliability is as follows and shown
in Figure 8.16.
[
] 0
:(
1) (1
): (
2);
notify s
R s
R
s
c
c
= →
′ = + −
′ =
To ensure whether the system is working properly, software design is very essential which
is set before it gets developed. Besides the functional requirements defined through activity and sequence diagram, it also requires nonfunctional requirements to assure the quality of the system developed. AAL systems require activities that are time constrained and
critical. To ensure the nonfunctional requirements of the system, Benghazi et al. (2012) has
modeled a design based on UML-RT that uses timed traces semantic and methodology
to check the timeliness and safety of AAL activity. Petri Nets is used as tool for modeling
semantic and interactive graphical language to develop and verify nonfunctional requirements of the system (Hein et al. 2009; Palanque et al. 2007). Benghazi has used formal
language CSP+T for defining the timed traces semantics of the operations. CSP+T is the
subset of CSP developed by Hoare in 1985. Let P and Q be a process that has defined a set
of events Σ with a ∈ ∑ and B ⊆ ∑ in a time interval [t,t+T].
ٗ
P STOP SKIP
P a
P I T t a P
I T t
P P Q P Q P Q P Q P Q
B
::
|
|0.*
|
|( , ).
| ( , )
|
|
| ; |
| | | |
=
→
∞ν →
→
→
The system is modeled in such a way that the process of target system is divided into
subsystems, each designed through an UML-RT context diagram and interconnected