62
M. Hadj Kacem et al.
Fig. 6. Smart home case study
an object of type “SmartThing”. The propagation of events between objects is
done through a DeviceGateway.
5 Patterns Specification
UML, as semi-formal language offers several benefits to the definition of IoT
design patterns, such as visual and standard notation. This graphical aspect is
certainly interesting and useful to an architect, in the sense that graphic design is
easy. However, the fact that UML lack a precise semantics is a serious drawback
because this language did not allow checks which we must carry. So, pattern
models generated at the modeling approach can be ambiguous and imprecise.
In addition, during the modeling phase, the architect can easily fall into the
error. This is due to the absence of a precise formal semantics of UML that do
not provide rigorous tools for verification and proof. However, any error or any
bad modeling of a design pattern can cause serious problems that generate bad
consequences.
Thus, ensuring the reliability and the correctness of IoT design patterns is
a goal that we have fixed. For this, we propose an approach to formally specify
design patterns by using the formal method Event-B that is well suited to our
needs and goals. Thus, each diagram graphically modeled will be accompanied
by a formal semantics. This approach allows the validation of the modeling part
and ensure the verification of the relevant properties of design patterns.
Event-B method is well-suited for specifying IoT design patterns: (i) The
primary concept in doing formal developments in Event-B is that of a model. It
is made of several components of two kinds: machines and contexts. Machines
contain the dynamic parts of a model, whereas contexts contain the static parts
M. Hadj Kacem et al.
Fig. 6. Smart home case study
an object of type “SmartThing”. The propagation of events between objects is
done through a DeviceGateway.
5 Patterns Specification
UML, as semi-formal language offers several benefits to the definition of IoT
design patterns, such as visual and standard notation. This graphical aspect is
certainly interesting and useful to an architect, in the sense that graphic design is
easy. However, the fact that UML lack a precise semantics is a serious drawback
because this language did not allow checks which we must carry. So, pattern
models generated at the modeling approach can be ambiguous and imprecise.
In addition, during the modeling phase, the architect can easily fall into the
error. This is due to the absence of a precise formal semantics of UML that do
not provide rigorous tools for verification and proof. However, any error or any
bad modeling of a design pattern can cause serious problems that generate bad
consequences.
Thus, ensuring the reliability and the correctness of IoT design patterns is
a goal that we have fixed. For this, we propose an approach to formally specify
design patterns by using the formal method Event-B that is well suited to our
needs and goals. Thus, each diagram graphically modeled will be accompanied
by a formal semantics. This approach allows the validation of the modeling part
and ensure the verification of the relevant properties of design patterns.
Event-B method is well-suited for specifying IoT design patterns: (i) The
primary concept in doing formal developments in Event-B is that of a model. It
is made of several components of two kinds: machines and contexts. Machines
contain the dynamic parts of a model, whereas contexts contain the static parts