Internet of Things (IoT) has become a common paradigm for different domains such as health care, transportation infrastructure, smart home, smart shopping, and e-commerce. With its interoperable functionality, it is now possible to connect all domains of IoT together for providing competent services to the users. Because numerous IoT devices can connect and communicate at the same time, there can be events that trigger conflicting actions to an actuator or an environmental feature. However, there have been very few research efforts made to detect conflicting situation in IoT system using formal method. This paper provides a formal method approach, IoT Confict Checker (IoTC2), to ensure safety of controller and actuators' behavior with respect to conflicts. Any policy violation results in detection of the conflicts. We defined the safety policies for controller, actions, and triggering events and implemented the those with Prolog to prove the logical completeness and soundness. In addition to that, we have implemented the detection policies in Matlab Simulink Environment with its built-in Model Verification blocks. We created smart home environment in Simulink and showed how the conflicts affect actions and corresponding features. We have also experimented the scalability, efficiency, and accuracy of our method in the simulated environment.
Some preliminary work in the areas of formal modeling and verification for smart home @cite_16 @cite_14 , intelligent transportation system @cite_12 , and health Internet of Things @cite_2 has been done. The closest to this work in terms of detecting conflicts are Depsys @cite_9 , and HomeOS @cite_10 . Depsys specified and detected conflicts after collecting the functionalities of 35 smart apps used in smart home. It detects the conflicts after they have occurred and in order to solve the situation priorities have been set to the apps so that no two apps can access the same actuator. Our approach, on the other hand, detects conflicts as soon as an event is generated which may immediately cause an action or a set of actions that result in conflicts. We have left the automated resolution of conflicts as future work.
@cite_14 @cite_9 @cite_2 @cite_16 @cite_10 @cite_12
1975812213 2728787983 2586458105 2889810448
As sensor and actuator networks mature, they become a core utility of smart homes like electricity and water and enable the running of many CPS applications. Like other Cyber-Physical Systems (CPSs), when a number of applications share physical world entities, it raises many systems of systems interdependency problems. Such problems arise in the cyber part mainly because each application has assumptions on the physical world entities without knowing how other applications work. In this work, we propose DepSys, a utility sensing and actuation infrastructure for smart homes that provides comprehensive strategies to specify, detect, and resolve conflicts in a home setting. Based on real home data, we demonstrate the severity of conflicts when multiple CPSs are integrated and the significant ability of detecting and resolving such conflicts using DepSys. New healthcare technologies are emerging with the increasing age of the society, where the development of smart homes for monitoring the elders’ activities is in the center of them. Identifying the resident’s activities in an apartment is an important module in such systems. Dense sensing approach aims to embed sensors in the environment to report the detected events continuously. The events are segmented and analyzed via classifiers to identify the corresponding activity. Although several methods were introduced in recent years for detecting simple activities, the recognition of complex ones requires more effort. Due to the different time duration and event density of each activity, finding the best size of the segments is one of the challenges in detecting the activity. Also, using appropriate classifiers that are capable of detecting simple and interleaved activities is the other issue. In this paper, we devised a two-phase approach called CARER (Complex Activity Recognition using Emerging patterns and Random forest). In the first phase, the emerging patterns are mined, and various features of the activities are extracted to build a model using the Random Forest technique. In the second phase, the sequences of events are segmented dynamically by considering their recency and sensor correlation. Then, the segments are analyzed by the generated model from the previous phase to recognize both simple and complex activities. We examined the performance of the devised approach using the CASAS dataset. To do this, first we investigated several classifiers. The outcome showed that the combination of emerging patterns and the random forest provide a higher degree of accuracy. Then, we compared CARER with the static window approach, which used Hidden Markov Model. To have a fair comparison, we replaced the dynamic segmentation module of CARER with the static one. The results showed more than 12 improvement in f-measure. Finally, we compared our work with Dynamic sensor segmentation for real-time activity recognition, which used dynamic segmentation. The f-measure metric demonstrated up to 12.73 improvement. A smart home system can provide better services to assist users if it knows what user activities will occur beforehand. Early research in activity prediction has indicated that the result of prediction is unique, but the accuracy remains unsatisfactory if only one result is considered. To solve this problem, this paper proposes a method of leveraging multiple models. In this work, we use a Bayesian network to build a model to predict which activity will happen, and then the predicted results go through a property filtering to get the final result. Due to the possibility that residents in a smart home may have different activity patterns, we have built a Bayesian network model to learn conditional probability of resident activities from the dataset of CASAS project. At last, we compare the results and show that our method has improved coverage and accuracy in activity prediction. This proposed method belongs to an ongoing project involving learning and control in a smart home system. Robust activity recognition in near real-time is a prerequisite for delivering the smartness intrinsic to the pragmatic realisation of smart homes, environments and so forth. Many of the physical devices necessary for equipping a smart home are already available as consumer electronic devices and certified for use by the public. Yet activity recognition remains the preserve of the research community, despite the array of machine learning and other AI techniques currently available. To-date, research has been dominated by the use of pre-segmented data, resulting in the recognition of an arbitrary activity subsequent to its completion. For assistive paradigms dependent on smart technologies, for example Ambient Assisted Living, such approaches are insufficient. The overall objective must be the identification of an activity within an appropriative confidence level as soon as possible after activity commencement. This paper presents a novel approach, COBRA (Cumulatively Overlapping windowing approach for AmBient Recognition of Activities), for near real-time activity recognition, specifically within 60 seconds of the commencement of an activity. COBRA utilises an innovative combination of sliding windows augmented with a logistic regression model. The approach is evaluated using the well-established, open, CASAS dataset.