Modeling of Bootstrapping and Registration IoT Design Patterns
63
of a model [1]. Thanks to this classification, Event-B allows the specification of
structural and behavioral features of design patterns. (ii) Refinement techniques
proposed by this method allow us to build patterns gradually and at different
abstraction levels. (iii) Mathematical proofs allow verifying model consistency
and consistency between refinement levels. (iv) The most important reason to use
Event-B method is the availability of a supporting tool called the Rodin platform
[2]. It is an Eclipse-based tool set that provides effective support for modeling
and automated proof. The platform is open source and is further extendable
with plug-ins. A range of plug-ins have already been developed including ones
that support animation and model checking like the Prob plug-in [5] that we
used.
Extended Component diagram that model structural features of design patterns are transformed to a context in the Event-B method in which we specify
entities of the architecture and their relations. The Sequence diagram is transformed into a machine in Event-B in which we specify events made between
entities of the patterns. This transformation is proposed in order to attribute
formal notations to IoT design patterns for the purpose of checking their design
correctness in a second step. We explicitly defined a refinement strategy to follow.
This strategy is interesting because it defines the pattern development process
and improves the quality of the obtained models, and therefore the success of the
formal development process. We defined specification levels by using a step-wise
development approach.
6 Tool Support
We developed a graphical modeling tool that implements our approach; it ensures
an easy and efficient modeling way for users. With our tool, we aim to make
concrete the aforementioned concepts. The architect can model the solution of
the IoT design patterns using an Eclipse plug-in that we propose. The tool, in
its development, is based on EMF
1 (Eclipse M odeling F ramework) [10]. This
was chosen since we use models, which are basic building units, to develop our
approach (Fig. 7).
7 Related Work
Research connected to design patterns in the field of software architecture, are
mainly classified into four branches of work according to their architectural style.
The first is about design patterns for Object-Oriented Architectures, the second
is about design patterns for Enterprise Application Integration (EAI), the third
is for Service Oriented Architectures (SOA) and the fourth one is for connected
object architectures.
Most of the proposed design patterns are described with a combination
of a text description and a graphical representation sometimes using a proprietary notation in the aim of making them easy to understand. However,
1 https://wiki.eclipse.org/Eclipse Modeling Framework.
63
of a model [1]. Thanks to this classification, Event-B allows the specification of
structural and behavioral features of design patterns. (ii) Refinement techniques
proposed by this method allow us to build patterns gradually and at different
abstraction levels. (iii) Mathematical proofs allow verifying model consistency
and consistency between refinement levels. (iv) The most important reason to use
Event-B method is the availability of a supporting tool called the Rodin platform
[2]. It is an Eclipse-based tool set that provides effective support for modeling
and automated proof. The platform is open source and is further extendable
with plug-ins. A range of plug-ins have already been developed including ones
that support animation and model checking like the Prob plug-in [5] that we
used.
Extended Component diagram that model structural features of design patterns are transformed to a context in the Event-B method in which we specify
entities of the architecture and their relations. The Sequence diagram is transformed into a machine in Event-B in which we specify events made between
entities of the patterns. This transformation is proposed in order to attribute
formal notations to IoT design patterns for the purpose of checking their design
correctness in a second step. We explicitly defined a refinement strategy to follow.
This strategy is interesting because it defines the pattern development process
and improves the quality of the obtained models, and therefore the success of the
formal development process. We defined specification levels by using a step-wise
development approach.
6 Tool Support
We developed a graphical modeling tool that implements our approach; it ensures
an easy and efficient modeling way for users. With our tool, we aim to make
concrete the aforementioned concepts. The architect can model the solution of
the IoT design patterns using an Eclipse plug-in that we propose. The tool, in
its development, is based on EMF
1 (Eclipse M odeling F ramework) [10]. This
was chosen since we use models, which are basic building units, to develop our
approach (Fig. 7).
7 Related Work
Research connected to design patterns in the field of software architecture, are
mainly classified into four branches of work according to their architectural style.
The first is about design patterns for Object-Oriented Architectures, the second
is about design patterns for Enterprise Application Integration (EAI), the third
is for Service Oriented Architectures (SOA) and the fourth one is for connected
object architectures.
Most of the proposed design patterns are described with a combination
of a text description and a graphical representation sometimes using a proprietary notation in the aim of making them easy to understand. However,
1 https://wiki.eclipse.org/Eclipse Modeling Framework.