A Formal Approach for Scalable Applications in Dynamic and Constrained IoT Systems
A Formal Approach for Scalable Applications in Dynamic and Constrained IoT Systems
Embedded Files
This page is dedicated to our Scalable IoT Applications model.
To use our model, you follow these steps
To use our model, you follow these steps
To download the model click here
1. Installation :
1.1 In the Rodin platform : Go to Help > Install New Software. Then select the appropriate update site from the list of download sites.
1.2 Install the Atelier B Provers plugin from the Atelier B Provers Update site to take full advantage of Rodin proof capabilities.
1.3 Install the ProB plugin from the ProB Update site for powerful model checking and animation.
1.4 Import the downloaded project ScalableIoTApplications model.
2. Animation of our model using ProB :
2.1 Select the Event-B explorer pointing to the ScalableIoTApplications model.
2.2 Select the animation context to place the model into its initial state. Our model is generic enough to be used for any application deployed on constrained and dynamic IoT system. To animate the desired application, you need to give values to constants and carrier sets related to the application in the animation context.
2.3 For instance, to animate the Health Monitoring Application of our motivating example, the initialization settings have been established in the manner described below.
2.4 You can proceed with the animation to validate the model. To do so, you need to right clicking on the machine or context you wish to animate and select "Start Animation/Model Checking".
2.5 Double-click on the SETUP_CONTEXT to place the model into its initial state.
2.6 As you can see, the "CheckInteroperability" event is activated (the green one), and there are many distinct ways to choose the parameters of the event. From there, you can play different scenarios and you can see at each step the variable's values. Double-click on an EVENT to execute it. If you want to control which parameters are used, right click on the EVENT and choose the desired parameter values.
2.7 For example, you can animate the communication (sensor2 -> analyzer) during the execution of HMA application, while verifying the states in which it may move. This scenario to be verified consists of the following steps.
2.7.1 You first trigger the event "BuildIoTSystem" to buid the IoT system on which the Health-Montioring Application is executed. As you can see, the values of the variables of the Structural_Machine (cnnDv, net, unDv) have been updated. Values that have changed are marked with a star. The history pane has also been updated. You can click on an event in the history to return back to the corresponding state. You can click on the left arrow in the Events pane to go back one step at a time (one you stepped back you can also step forward again; this works just like in a web browser).
2.7.2 You activate the event "MobilityManagement" to deal with the mobility of sensor3 (mobileDev (sensor3↦CNN1)). In this case, the variable related to the Mobility_Machine will be updated.
2.7.3 The event "DynamicReconfiguration" is then enabled to reconfigure the network (LLN1) on which the HMA is executed. When you trigger this event, the LLN1 will turn into a challenged network CHN.
2.7.4 Before launching the sensor2 -> analyzer communication, you can fire the event "CheckInteroperability", to verify that the client (sensor2) and the server (analyzer) are interoperable. In this case, the variable Interoperability of the Behavioral_Machine will be evaluated to TRUE (Interoperability=TRUE). As a result, the event "IntermediaryInterference" will be automatically activated.
2.7.5 Then you trigger the event "IntermediaryInterference" to check whether a proxy should assist the client (Proxying = TRUE) or perform any protocols translation.
2.7.6 You can activate the event "HandleProxyConflicts" to interfere the proxy2 as the client does not have the capability to interact with the server (PrxTasks(proxy2)=PrxTasks(proxy2)+1=2).
2.7.7 If proxy2 is not saturated, you can trigger the event "HandleProxyTasks" to route the request of sensor2 to proxy2 where it is proceed and forwarded to the analyzer. The number of proxy2 tasks is then decreased.
2.7.8 If PrxTasks(proxy2 (2) + its copies (0)) + threshold (1) exceed the maximum capacity of proxy2, you can trigger the event "DeployNewProxy" to deploy a new proxy3 (copy) that has same functionalities of proxy2 (deployedPrx(proxy3↦proxy2)).
2.7.9 If not, you can trigger the event "ConsolidateProxy" to remove the useless copies (e.g proxy3).
Finally, the message is forwarded to the analyzer.
2.8 You can identify the model’s behaviour as correct after observing it in many scenarios, which you monitor.
For example, you can launch the next communications, such that the HMA application releases its full execution.
3. Verifiying our model using Proof Obligations (Atelier B): To verify the consistency of the model, Proof Obligations (POs) are generated by the Rodin platform to verify the model properties (e.g Scalability) and to ensure that the events related to four sub-models preserve and do not falsify the invariants.
3.1 You select the machine or context that you want to discharge its proof obligations. Then you click Proof Obligations.
Other Case Studies
Other Case Studies
Our ScalableIoTApplications model is generic enough to be used for any application deployed on constrained and dynamic IoT system. To animate other applications (e.g Fire Alarm Application, Flight Control Application), you need to initialize the animation context by initialization settings related to the desired application.
Example 1 : Fire Alarm Application
Let us consider the safety-critical Fire Alarm application that improves the degree of protection in a smart city. The application is executed on a constrained IoT system (system1) that consists of a constrained-node network (CNN1) and a low-power, lossy network (LLN1). The characteristics of the CNN1 are influenced by being composed of a considerable portion of constrained devices (e.g sensor3, building1, QN1, ...), that exhibit severe limits in terms of resources. However, the LLN1 involves a portion of constrained devices (e.g sensor1) with additional aspects stemming from the network namely a high degree of packet loss. The IoT devices are responsible for the following resources that expose their services:
Gas Sensing Service: hosted on the sensor3.
Window/Door Control Service: offered by the sensor3.
Emergency Notification Service: hosted on the sensor3.
Smoke Sensing Service: offered by the sensor2.
Temperature Record Service: hosted on the sensor2.
Water Sprinkling Service: hosted on the UnN1.
During the execution of Fire Alarm Application, IoT devices communicate in a collaborative manner to ascertain whether or not there is a risk of fire. The following communications may occur:
QN1 -> sensor3: QN1 queries the sensor3 about its hosted resource ‘Gas Sensing Service’. The request is satisfied without the interference of intermediaries (e.g proxy1) since QN1 employs CoAP protocol especially designed to transmit and retrieve the data of constrained nodes. Hence, the sensor3 responds with a payload containing the resource value.
sensor3 to UnN1: sensor3 exhibits severe limits and cannot talk directly to unconstrained UnN1 that employs full protocol stack (e.g HTTP). So as the interference of proxy1 is required to make protocols translations and send JSON state of the captured ‘Emergency Notification’.
The application is in charge of analysing the resources' contents retrieved in real-time from the sensor1 and sensor3 that detect smoke and gases and so on. These readings are evaluated against a predetermined threshold to determinate whether there is a risk of fire. In the event that a risk is identified, the Water Sprinkling Service will be enforced to rapidly extinguish the fire and avoid tragic aftermath.
To animate the application, you need to give values to constants and carrier sets related to Structural_Context, Behavioral_Context, Mobility_Context and Scalability_Context in the animation context. The initialization settings of the animation context have been established in the following manner. The animation context is established to place the model into its initial state. From there, you can play different scenarios to verify the application properties (structure, behavior, mobility and scalability) and validate the model.
Example 2 : Flight Control Application
Flight Control is one instance of constrained and unconstrained IoT devices that bind in a real-world application. The devices (directionSensor, attitudeSensor, ...) communicate to assess the direction and attitude of aircrafts that are reported to hubs via Internet, where they are examined and tracked over time. The application analysis the plane flight indicators retrieved in real-time from the directionSensor and attitudeSensor that detect direction and attitude and so on. These readings are evaluated against a threshold to determinate whether there is a plane deviation or crash danger. In the event that a life-threatening risk is identified, the flight control surface will be automatically adjusted to enahnce flight safety and avoid human looses. From there, the surface control actuator will be put into action to change the position/angle of the surface controls (Rudder, Elevators, Slats, ...). It is directly responsible to change the aircraft principal axis of rotation (Roll and Pitch).
To animate the application and verify/validate our model, the initialization settings of the animation context can be established in the manner described below.
Page updated
Google Sites
Report abuse