366
S. Ouchani and M. Krichen
reinforcement mechanism using UML and express the related requirements in Alloy. It
takes as input the system requirements as assertions and the reinforced model including
UML diagrams and RBAC model. The results showed the effective correctness of the
modeled system and its related reinforcement mechanism.
The next Sect. 2 describes the related work. Then, we present the modeling and the
validation of the system. Finally, Sect. 5 concludes the paper and suggests the possible
future research.
2 Related Work
In this section, we study the latest IoT contributions, its application in information services, and especially those targeting health care systems. We survey also the contributions dealing with IoT systems modeling, verification and validation.
– Ouchani [14] develops a formal framework to analyze the functional correctness of
IoT systems. The proposed framework covers the main components of IoT systems
and the approach is automatic. However, the framework suffers from the limitations
inherited from PRISM and the security properties are not specified.
– Drira [2] discusses the challenges of modeling IoT in large scale systems called
system-of-systems by focusing on interactions and real-time reconfigurations. This
contribution presents an overview of architectural concepts without dealing with
practical experiments.
– Rahman et al. [18] discuss the complexity of distributing services in many IoT
devices as well as the challenges facing the system requirements for each level:
devices, services, and applications. The proposed model assures a quality attributes
such as update, interoperability, security, functional appropriateness, availability and
adaptability. However, the verification process suffers from many limitations at the
evaluation step.
– Gupta et al. [6] design an IoT-based health monitoring framework to reduce the
neglect of healthcare. Their solution uses the second generation Intel Galileo board,
an Arduino IDE that is explored to program the brain, and Xampp database. This
solution provides support emergency medical services by collecting, integrating, and
inter-operating of IoT data flexibly. However, they are limited in controlling the
access and ensuring privacy.
– Madakam et al. [12] review IoT concepts that aim to unify everything into a common
infrastructure using smart sensors. First, they focus on basic requirements, geneses, definitions, aliases and characteristics of IoT. Further, they present a various
technologies and their usages in innumerable IoT applications into all the domains
including medical, manufacturing, transportation, etc. Finally, they acknowledge the
need to a standard definition and protocols as well as a universal architecture of IoT
that allows for various technologies the ability to inter-operate.
– Gigli et al. [5] attempt services categorization provided by IoT systems, which aims
to help building a service provider. They consider ubiquitous services which are
collaborative aware. However, they require to overcome protocol distinctions among
technologies and unify every aspect of the network.
S. Ouchani and M. Krichen
reinforcement mechanism using UML and express the related requirements in Alloy. It
takes as input the system requirements as assertions and the reinforced model including
UML diagrams and RBAC model. The results showed the effective correctness of the
modeled system and its related reinforcement mechanism.
The next Sect. 2 describes the related work. Then, we present the modeling and the
validation of the system. Finally, Sect. 5 concludes the paper and suggests the possible
future research.
2 Related Work
In this section, we study the latest IoT contributions, its application in information services, and especially those targeting health care systems. We survey also the contributions dealing with IoT systems modeling, verification and validation.
– Ouchani [14] develops a formal framework to analyze the functional correctness of
IoT systems. The proposed framework covers the main components of IoT systems
and the approach is automatic. However, the framework suffers from the limitations
inherited from PRISM and the security properties are not specified.
– Drira [2] discusses the challenges of modeling IoT in large scale systems called
system-of-systems by focusing on interactions and real-time reconfigurations. This
contribution presents an overview of architectural concepts without dealing with
practical experiments.
– Rahman et al. [18] discuss the complexity of distributing services in many IoT
devices as well as the challenges facing the system requirements for each level:
devices, services, and applications. The proposed model assures a quality attributes
such as update, interoperability, security, functional appropriateness, availability and
adaptability. However, the verification process suffers from many limitations at the
evaluation step.
– Gupta et al. [6] design an IoT-based health monitoring framework to reduce the
neglect of healthcare. Their solution uses the second generation Intel Galileo board,
an Arduino IDE that is explored to program the brain, and Xampp database. This
solution provides support emergency medical services by collecting, integrating, and
inter-operating of IoT data flexibly. However, they are limited in controlling the
access and ensuring privacy.
– Madakam et al. [12] review IoT concepts that aim to unify everything into a common
infrastructure using smart sensors. First, they focus on basic requirements, geneses, definitions, aliases and characteristics of IoT. Further, they present a various
technologies and their usages in innumerable IoT applications into all the domains
including medical, manufacturing, transportation, etc. Finally, they acknowledge the
need to a standard definition and protocols as well as a universal architecture of IoT
that allows for various technologies the ability to inter-operate.
– Gigli et al. [5] attempt services categorization provided by IoT systems, which aims
to help building a service provider. They consider ubiquitous services which are
collaborative aware. However, they require to overcome protocol distinctions among
technologies and unify every aspect of the network.