Context-aware systems are an emerging class of mobile computing systems aiming to provide ubiquitous access to information, communication and computation. These systems are able to sense and adapt their behavior automatically to the current environmental context. In this paper, we present a formal approach based on bigraphical reactive systems for specifying and verifying the main features of context-aware systems. The proposed formalism provides a clear separation between the part of the system which is affected by the context and the remaining part. In order to illustrate its potential, we apply our approach through a motivating case study of a smart home system, and by using the Bigraphical Model Checker (BigMC) for verification purposes.
Recently, context-aware systems are becoming
one of the most promising fields in the wide range of
ubiquitous computing
In the literature, there are many definitions of the term “context”, but until now there is no universal one. In (Abowd et al., 2000), a generic definition has been proposed in which context is referred as “any information that can be used to characterize the situation of an entity. An entity is a person, place or object that is considered relevant to the interaction between a user and an application, including location, time, activities and the preferences of each entity”.
Nevertheless, the lack of a solid formal foundation
in the most existing definitions, combined with the
increasing complexity and diversity of context-aware
systems, represent a clear challenge to model and
verify such systems. Therefore, the formal modeling
represents a crucial and delicate step to reduce
complexity and enhance the verification of
contextaware systems. As a result, many formal approaches
have been introduced to deal with this issue; Pascal
Zimmer
Furthermore, according to
Among the recent BRS-based studies in the
domain of context-aware systems, we can highlight
the following: Plato-graphical models
Our proposed approach
Moreover, to illustrate the interest of our
approach, we apply it, in this paper, to a simple smart
home system focusing on the function of the lightning
control service. Besides, in order to assess the
feasibility and effectiveness of our proposed
approach, we use the Bigraphical Model Checker
(BigMC)
The rest of this paper is organized as follows. Section 2 presents a motivating case study of a context-aware home system. Section 3 gives an overview of bigraphical reactive systems. Section 4 briefly introduces our BRS-based approach for modeling the different aspects of context-aware systems. Section 5 describes how we use the BigMC to implement the smart home case study in order to validate the correctness of our proposed approach. Finally, conclusion and future work are given in Section 6.
Along with the rapid proliferation of high technologies, particularly in the fields of electronic, communication and control, homes and the way we live in them have changed dramatically in the last decade. Today, the smart home research becomes one of the major sub-domains of ubiquitous computing. Many research institutes and well-known enterprises such as Apple, Microsoft, Cisco, Xerox, MIT, Siemens and IBM, are developing smart housing products and services in order to improve the comfort, convenience and security of inhabitants.
According to the definition given by the UK
Department of Trade and Industry (DTI), a smart home
is “A dwelling incorporating a communications network
that connects the key electrical appliances and
services, and allows them to be remotely controlled,
monitored or accessed”
Technically, a smart home incorporates three
main elements: internal network, intelligent control
and home automation
One of the most well-known smart home services is the lightning control system which is a standalone system serving to deliver the right amount of light only where and when it is needed. For example, setting outdoor lights to go on at sunset and off at daybreak.
According to
Structurally, a bigraph is a graphical model emphasizing both locality and connectivity of ubiquitous systems. The figure below depicts the anatomy of bigraphs.
The dashed line rectangles with rounded corners represent roots (also known as regions) that are used to distinguish significantly different spaces in which nodes can be nested. Nodes can be nested inside one another. Nodes and edges are denoted by and respectively. The small bold points linking nodes to edges are called ports. Each node is characterized by a control, represented by an upper-case letter. The shaded rectangles represent sites, which allow nodes to host any content inside. The outer names and inner names represent end points where connections with the outside world can be established.
Moreover, a bigraph consists of two independent sub-graphs (as shown in Figure 2), a place graph (topograph) expressing usually the physical location of nodes and a link graph (monograph) representing the mobile connectivity among them.
Formally, a bigraph over a signature takes the form = (, , ,
P, L) ∶ → To illustrate the bigraph notations, Figure 1 represents a bigraph : 〈2, { 0, 1}〉 → 〈2, { 0, 1, 2}〉 where the sets of nodes and edges are given by = { 0, 1, 2} {: 2, : 4} and = { 0, 1} respectively.
= represents the signature of the bigraph .
The interface = 〈2, { 0, 1}〉 is the inner face of in which 2 is a finite ordinal representing the number of sites and = { Similarly, the
0, 1} is the set of inner names. outer face of is given by = 〈2, { 0, 1, 2}〉 where regions and = { Finally, : 2 → 2 is the : { 0, 1} → { 0, 1, 2} is its link graph.
2 represents the
number of 0, 1, 2} is the set of outer names.
Bigraphs
can
be
also
expressed in terms
language
) to represent the entire
Moreover, each part of the system (i.e. contextaware and context-unaware parts) has its own reaction rules, namely context reaction rules and internal reaction rules, respectively. However, these reaction rules are performed independently of each other. That is, a context-aware reaction rule is a sequence of reaction rules occurred in each part of the context-aware system to shift it from one state to
To illustrate the effectiveness of our approach to model the different aspects of context-aware systems, in the following, we apply it through a simple lightning control system. ° | ∥ . ⊗ →( ) 1 /
Composition of nodes Merge product (Juxtaposition of nodes) Parallel product (Juxtaposition of roots) Nesting. contains Tensor product Node with control of arity ⃗ The barren (empty) root Site numbered Connection from inner name y to outer name are connected to the central control unit. The site 1 predicted to introduce other context information; such as interior lights, motion sensors, security cameras and so on. Finally, the open link x is used to capture context information.
The algebraic expression of the lightning control system running in DAY MODE is as follows: ⁄ ℎ.
(. )| . (.
)| 1
As mentioned previously, at sunset, the lightning control system switches automatically to
reaction represents a context reaction rule. The figure below models the bigraph host : → of the new context bigraph.
We denote the captured sunset information and light-on event by NIGHT and ON respectively. These nodes are called
context-nodes, resulting of the context transition introduced in our case study.
Formally, the aforementioned nodes are the result of a sequence of context reaction rules (see Table 2) triggered by the captured sunset information.
The figure below depicts a portion of the context bigraph : →
resulting after the occurrence of the previous reaction rules sequence.
The idea behind the separation of the contextaware aspects (Figure 5) of the system from the other aspects (Figure 4) is not only to cope with the complex nature of context-aware systems, but also to make predictive modeling, simple and efficient, by providing a generic way for capturing, structuring and representing the system-context relationships.
That is, the bigraphical model of the lightning control system running in NIGHT
(see host and context bigraph presented in Figure 4 and of ; it proceeds by plugging each region of into its matching site of , and merging the outer names of with the inner names of .
To clarify a bit more, = 〈, 〉 is the inner face of the bigraph in which represents the number of sites where each region of containing context-nodes can be planted into the ℎ
site of . is the set of inner names where each inner name is linked to its related outer name of to form a context-edge. )| . (.
. (. . (. )| 1 )| 1 )| 1
Formal methods are one of the
highlyrecommended techniques in software design of
complex systems in both academia and industry. They
offer a powerful potential to achieve an early
integration of verification in the design process, to
provide more effective verification techniques and to
reduce the verification time
Recently, research in formal methods has led to the appearance of some very promising verification techniques accompanied by powerful software tools that automate various verification steps, in order to facilitate the early detection of defects. Model checking is one of the most successful strategies for analyzing the correctness of safety-critical systems. It is a formal technique for automatically verifying whether a finite-state system satisfies a given logical property.
In the following, we introduce the Bigraphical model checker BigMC and its grammar, then, we describe how to use it in order to implement and perform some verifications on the lightning control system model.
BigMC (Bigraphical Model Checker) is a model
checker specifically designed to operate on any model
encoded as a bigraphical reactive systems
The full BigMC grammar is given in the following table. ∷= ; | ∷= % ∶ ∷= % ∶ ∷= % → ∷= % ∷= → | ∷= . | | | || | $ | | ∷= [ ] | : : = , | ∷= [ – – ][ – – 0 – 9] ∗ | − ∷= ℎ ( ) | () | !
BigMC grammar is relatively simple since it is based on a term language. In the table above, refers to a bigraphical model that may be composed from other models or/and expressions . An expression can be a control () , reaction rules ( → ) , or a property () . A control must be pre-defined by the declaration of the bigraph signature % and % commands, which define the arity (number of ports) of a given control as well as whether it is active or passive. Any term of the form → is considered to be a reaction rule, where the first term represents the redex, while the second represents the reactum. Finally, the property is expressed as a logical formula and it is checked whether a given bigraphical model satisfies or violates this formula.
In order to verify the feasibility of our approach, we use the BigMC model checker to encode the lightning control system.
The table below represents the bigraphical specification of the context-unaware part in BigMC terms language.
The bigraphical specification of the context-aware part represented in Figure 5 is as follows: #Reaction Rules CCUnit[e1,x].(mode.$2) -> CCUnit[e1,x].(mode.NIGHT); OLight[e1].(mode.$3) -> OLight[e1].(mode.ON);
Once the lightning control system model and the set of reaction rules are defined, the next step consists to specify some properties that must be checked. Here, we focus on proving that the final state corresponding to the bigraph reconfiguration displayed in Figure 6 is eventually reachable by the application of the above reaction rules.
BigMC implements explicit-state checking of
properties expressed as matching. Each property is
expressed as combinations of two predefined
predicates: matches () and terminal (). The
matches() predicate describes some redex that must
be found (or assert that not be found) in every possible
agent of a given system as it behaves. The terminal ()
predicate is true if an only if there are no possible
further states reachable by a step of reaction from the
current one. Furthermore, predicates can be
combined together with the common boolean
operators and, or and not (i.e. &&, || and !) to form
more complex expressions
Now, let final_state be a reachability property defined as the negation of the buit-in predicate terminal (). We note that the final state is a terminal state which does not lead to any further states and there are no reaction rules that can be applied to it.
The specification of the final_state property in BigMC is as follows:
The following are the default command-line options for BigMC: -m 1000: maximum number of steps. -r 50: reporting frequency.
-p: a command to print new states.
Running BigMC with these options, we prove that the intended state is successfully reached as shown in step 4 of Table 8. > C:\Progra~1\BigMC/bin/bigmc -m 1000 -r 50 -p 1: (OLight[e1].mode.OFF.nil|CCUnit[e1,x].mode.DAY.nil) 2: (OLight[e1].mode.ON.nil|CCUnit[e1,x].mode.DAY.nil) 3: (OLight[e1].mode.OFF.nil|CCUnit[e1,x].mode.NIGHT.nil) 4: (CCUnit[e1,x].mode.NIGHT.nil|OLight[e1].mode.ON.nil) [mc::step] Complete!
In this paper, we have presented a formal approach based on bigraphical reactive systems to specify and verify context-aware systems. Firstly, we have shown, through a case study of a smart home system, the potential of our approach for a generic and high level modeling of the different aspects of contextaware systems. The proposed approach provides a clear separation between the context-aware part of the system and the remaining one; each part is modeled by a distinct bigraph, and their composition yields a new bigraph describing the whole structure of the context-aware system.
Besides, the behavior of context-aware systems has been characterized by bigraphical reaction rules with respect to both context changes and internal system changes. Then, we have implemented the case study using the BigMC model checker and effectively proven the applicability of our approach.
As a future extension, we intend to evaluate the effectiveness of our approach by checking whether some critical non-functional properties (i.e. security) of a particular bigraphical model are true.
Additionally, we are developing a tool
Baier, C., Katoen, J. P. (2008) Principles of Model Checking (Representation and Mind Series). The MIT Press. Cambridge. England.