Article Preview
TopIntroduction
Pervasive computing is considered as a promising scheme which enables users to enjoy services anytime and anywhere in transparent manner (Weiser, 1991; Xu, Shi, & Xie, 2003). A pervasive computing system aims to serve the users without distracting their attention from the tasks (Dey et al., 2001; Abowd et al., 1999). Therefore, the system needs to be aware of the context and adjust its action accordingly.
Context awareness refers to an ability to adapt to changing circumstances based on contextual information. By unobtrusive sensing, collecting, reasoning, and acting on context information, context-aware systems react automatically, which makes the environment truly smart (Preuveneers & Joosen, 2016). A smart environment can be regarded as a complex system made up of every kind of services, especially context-aware services.
Context-aware service gathers context information by sensors deployed in the environment, interpreting information, determining necessary action and commanding the actuator to take appropriate action (Carreira, Resendes, & Santos, 2014; Hoareau & Satoh, 2009). The actuators in turn affect its surrounding physical environment, i.e., influence the context (Carreira et al., 2014). The context change may trigger service elsewhere in the environment, and thus produce cascading reactions. Conflict adaptations or unexpected side effects may exist in the process.
Therefore, understanding the impact of services and side effects are important tasks for the service developer. Ensuring reliability of the smart environment is a complex task due to its dynamic and distributed nature, as well as the number of services (Guilly et al., 2016). Moreover, services may come from different developers or be deployed at different times. The potential consequence of unexpected side effects from subsequent reactions may not always be clear. There is need for better design support to analyze adaptions and discover potential conflict.
The definition of conflict in a pervasive computing environment varies from application to application (Carreira et al., 2014). From the resolution perspective, some conflicts cannot be avoided (e.g. users with different intentions in multiuser environments, two services exclusively applying for the same resource at the same time). The only thing that the system can do is to detect and resolve these conflicts. However, apart from that, there are conflicts that can be avoidable by increasing the flexibility and adaptability of service through improving service logic. In this case, it is important to detect these conflicts at design time.
From the detection perspective, some conflicts can be determined in semantic level, such as services with the same triggering conditions and contradictory actions. Semantic analysis is useful at design time as well as at run time. However, some conflicts cannot be easily determined in semantic level. These services are conflict not only due to their contradictory actions, but also that they are wrongly triggered in certain situations. Simulation and formal verification are effective methods to detect these conflicts and determine their occurring situation.
Applications of formal methods is essential to analyze and verify such systems. There are a lot of research trying to increase the reliability of different aspects of intelligent environments, particularly in using formal verification techniques (Corno & Sanaullah, 2013; Coronato & De Pietro, 2010; Guilly et al., 2016). Such approaches and tools would aid software developers at design time, and would be useful in configuration and reconfiguration processes.
The main concerns of this paper are two types of conflict: (1) one service frustrating the execution of another; and (2) one service violating another service’s objective. The former may occur when services are simultaneously executed. The latter is asynchronous and generally does not directly cause another service to be unable to work, thus more hidden than other types of conflict.
Smart environment is complex due to the number of contexts, services and the user’s activity. The approach presented in this paper aims to show what will occur by simulating complex environment change and service execution, particularly to detect the potential conflicts and determine their occurring situation.