=Paper=
{{Paper
|id=Vol-1256/paper1
|storemode=property
|title=Towards Formal Modeling and Verification of Context-Aware Systems
|pdfUrl=https://ceur-ws.org/Vol-1256/paper1.pdf
|volume=Vol-1256
|dblpUrl=https://dblp.org/rec/conf/vecos/CherfiaBB14
}}
==Towards Formal Modeling and Verification of Context-Aware Systems==
https://ceur-ws.org/Vol-1256/paper1.pdf
18
Towards Formal Modeling and Verification of
Context-Aware Systems
Taha Abdelmoutaleb Cherfia Faïza Belala Kamel Barkaoui
LIRE Laboratory LIRE Laboratory Laboratoire CEDRIC
Software Technologies and Information Software Technologies and Information Conservatoire Nationale des Arts et
Systems Department, Constantine 2 Systems Department, Constantine 2 Métiers
University University CNAM, Paris Cedex 03,
Algeria Algeria France
taha.cherfia@univ-constantine2.dz faiza.belala@univ-constanine2.dz kamel.barkaoui@cnam.fr
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.
Formal Verification. Context-Aware Systems. Bigraphical Reactive Systems. Bigraphical Model Checker.
1. INTRODUCTION complexity and enhance the verification of context-
aware systems. As a result, many formal approaches
Recently, context-aware systems are becoming have been introduced to deal with this issue; Pascal
one of the most promising fields in the wide range of Zimmer (Zimmer, 2005) introduced a new process
ubiquitous computing (Weiser, 2002). These systems calculus, called Context-Aware Calculus (CAC in
are able to dynamically adapt their behavior in short), to formally describe the context-aware
response to changes on context information without systems. Likewise, authors in (Siewe, Cau and Zedan,
an explicit user intervention. 2009) proposed a logical language CCA (Calculus of
In the literature, there are many definitions of the Context-aware Ambients) for the modeling and
term “context”, but until now there is no universal one. verification of context-aware systems.
In (Abowd et al., 2000), a generic definition has been Furthermore, according to (Birkedal, Debois and
proposed in which context is referred as “any Hildebrandt, 2006), one of the principal aims for the
information that can be used to characterize the theory of Bigraphical Reactive Systems (BRS in short)
situation of an entity. An entity is a person, place or is to model ubiquitous systems, capturing mobile
object that is considered relevant to the interaction locality in the place graph and mobile connectivity in
between a user and an application, including location, the link graph.
time, activities and the preferences of each entity”.
Among the recent BRS-based studies in the
Nevertheless, the lack of a solid formal foundation domain of context-aware systems, we can highlight
in the most existing definitions, combined with the the following: Plato-graphical models (Birkedal,
increasing complexity and diversity of context-aware Debois and Hildebrandt, 2006), context and actions
systems, represent a clear challenge to model and (Xu, Xu and Lei, 2011), context and capabilities
verify such systems. Therefore, the formal modeling (Wang, Xu and Lei, 2011) and BiAgents (Pereira,
represents a crucial and delicate step to reduce Kirsch and Sengupta, 2012). Nonetheless, only the
19
graphical representation of bigraphical reactive is “A dwelling incorporating a communications network
systems has been used to model context-aware that connects the key electrical appliances and
systems and their evolution. There has been no services, and allows them to be remotely controlled,
information or formal definition of the relationship monitored or accessed” (King, 2003). Remotely-
between the context changes and the system controlled means that the appliances and services
reactions. Furthermore, no formal verification has may be controlled within or outside the dwelling.
been performed within these approaches to
Technically, a smart home incorporates three
investigate the correctness of the context-aware
main elements: internal network, intelligent control
models.
and home automation (Jiang, Liu and Yang, 2004); to
Our proposed approach (Cherfia and Belala, provide the inhabitant with a full control over the smart
2014) is quite similar to the previous ones since it is home system. In a bit more details, with a single press
based on BRS, but where the context-aware and on a touchpad, a smart homeowner can control
context-unaware parts of the system, are clearly lighting, climate, multimedia, window and door
separated. Each one has its own reaction rules and by operations, security and surveillance, as well as many
using the composition operation defined natively in other functions.
BRS, we can describe, first the whole context-aware
One of the most well-known smart home services
system and then, capture the relationship between the
is the lightning control system which is a standalone
context changes and the system behavior.
system serving to deliver the right amount of light only
Moreover, to illustrate the interest of our where and when it is needed. For example, setting
approach, we apply it, in this paper, to a simple smart outdoor lights to go on at sunset and off at daybreak.
home system focusing on the function of the lightning
control service. Besides, in order to assess the 3. BIGRAPHS OVERVIEW
feasibility and effectiveness of our proposed
According to Milner (2009), a bigraphical reactive
approach, we use the Bigraphical Model Checker
system is a bigraph representing the current topology
(BigMC) (Perrone, Debois and Hildebrandt, 2013) to
of the system and a set of reaction rules that allow
determine whether the composition operation satisfies
describing its behavior by capturing the context
the reachability property.
changes.
The rest of this paper is organized as follows.
Structurally, a bigraph is a graphical model
Section 2 presents a motivating case study of a
emphasizing both locality and connectivity of
context-aware home system. Section 3 gives an
ubiquitous systems. The figure below depicts the
overview of bigraphical reactive systems. Section 4
anatomy of bigraphs.
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.
2. MOTIVATING EXAMPLE
Along with the rapid proliferation of high Figure 1: The anatomy of Bigraphs.
technologies, particularly in the fields of electronic,
communication and control, homes and the way we The dashed line rectangles with rounded corners
live in them have changed dramatically in the last represent roots (also known as regions) that are used
decade. Today, the smart home research becomes to distinguish significantly different spaces in which
one of the major sub-domains of ubiquitous nodes can be nested. Nodes can be nested inside one
computing. Many research institutes and well-known another. Nodes and edges are denoted by 𝑣𝑖 and 𝑒𝑖
enterprises such as Apple, Microsoft, Cisco, Xerox, respectively. The small bold points linking nodes to
MIT, Siemens and IBM, are developing smart housing edges are called ports. Each node is characterized by
products and services in order to improve the comfort, a control, represented by an upper-case letter. The
convenience and security of inhabitants. shaded rectangles represent sites, which allow nodes
According to the definition given by the UK to host any content inside. The outer names and inner
Department of Trade and Industry (DTI), a smart home names represent end points where connections with
the outside world can be established.
20
Moreover, a bigraph consists of two independent For example, the following is the corresponding
sub-graphs (as shown in Figure 2), a place graph algebraic expression of the bigraph given in Figure 1
(topograph) expressing usually the physical location
of nodes and a link graph (monograph) representing 𝑣0𝑦0 . (𝑣1𝑦0,𝑥0 |𝑑0 ) ∥ 𝑣2𝑦1 ,𝑦2 ,𝑥0,𝑥1 . 𝑑1
the mobile connectivity among them.
For more details about the theory of bigraphical
reactive systems the reader is referred to (Milner,
2009).
4. BIGRAPH-BASED MODEL FOR CONTEXT-AWARE
SYSTEMS
Our proposed approach (Cherfia and Belala,
2014) consists in providing a bigraphical reactive
systems based approach to formally model the
different aspects of context-aware systems. Firstly, we
have enriched the bigraph definition to represent the
Figure 2: Place graph and Link graph. structure of the context-aware system by modeling
separately both the context-aware and context-
Formally, a bigraph 𝐺 over a signature 𝒦 takes the unaware parts of the system. To do so, we use two
form distinct bigraphs (𝑆 and 𝐶). 𝑆: 𝐾 → 𝐽 is a bigraph
𝐺 = (𝑉, 𝐸, 𝑐𝑡𝑟𝑙, 𝐺 P , 𝐺 L ) ∶ 𝐼 → 𝐽 modeling the context-unaware part of the system and
𝐶: 𝐼 → 𝐾 is another bigraph modeling the context-
To illustrate the bigraph notations, Figure 1 aware part. Then, we combine them together using the
represents a bigraph 𝐺: 〈2, {𝑥0 , 𝑥1 }〉 → 〈2, {𝑦0 , 𝑦1 , 𝑦2 }〉 composition operation (𝑆 ∘ 𝐶) to represent the entire
where the sets of nodes and edges are given by 𝑉 = system given by 𝑆𝐶 : 𝐼 → 𝐽.
{𝑣0 , 𝑣1 , 𝑣2 } and 𝐸 = {𝑒0 , 𝑒1 } respectively. 𝒦 = Moreover, each part of the system (i.e. context-
{𝐾: 2, 𝑀: 4} represents the signature of the bigraph 𝐺. aware and context-unaware parts) has its own
The interface 𝐼 = 〈2, {𝑥0 , 𝑥1 }〉 is the inner face of 𝐺 in reaction rules, namely context reaction rules and
which 2 is a finite ordinal representing the number of internal reaction rules, respectively. However, these
sites and 𝑋 = {𝑥0 , 𝑥1 } is the set of inner names. reaction rules are performed independently of each
Similarly, the outer face of 𝐺 is given by 𝐽 = other. That is, a context-aware reaction rule is a
〈2, {𝑦0 , 𝑦1 , 𝑦2 }〉 where 2 represents the number of sequence of reaction rules occurred in each part of the
regions and 𝑌 = {𝑦0 , 𝑦1 , 𝑦2 } is the set of outer names. context-aware system to shift it from one state to
Finally, 𝐺 𝑃 : 2 → 2 is the place graph of 𝐺 while another.
𝐺 𝐿 : {𝑥0 , 𝑥1 } → {𝑦0 , 𝑦1 , 𝑦2 } is its link graph.
To illustrate the effectiveness of our approach to
Bigraphs can be also expressed in terms model the different aspects of context-aware systems,
language (Milner, 2008) the primary operations and in the following, we apply it through a simple lightning
elements used by the present paper are summarized control system.
in Table 1.
TABLE 1: Algebraic expressions of bigraphs.
Term Interpretation
𝑈°𝑉 Composition of nodes
𝑈|𝑉 Merge product (Juxtaposition of nodes)
𝑈 ∥𝑉 Parallel product (Juxtaposition of roots)
𝑈. 𝑉 Nesting. 𝑈 contains 𝑉
Figure 3: DAY MODE bigraph.
𝑈⊗𝑉 Tensor product
𝐾→ (𝑈)
𝑥
Node with control 𝐾of arity 𝑥⃗ As shown in Figure 3, the node DAY nested in
CCUnit (Central Control Unit) indicates that the
1 The barren (empty) root
lightning control system is running in DAY MODE (i.e.
𝑑𝑖 Site numbered 𝑖 outdoor lights are OFF). The hyper-edge e1 linking the
𝑥/𝑦 Connection from inner name y to outer name 𝑥 node OLight with CCUnit means that the outdoor lights
are connected to the central control unit. The site 1
21
predicted to introduce other context information; such The figure below depicts a portion of the context
as interior lights, motion sensors, security cameras bigraph 𝐶: 𝐼 → 𝐾 resulting after the occurrence of the
and so on. Finally, the open link x is used to capture previous reaction rules sequence.
context information.
The algebraic expression of the lightning control
system running in DAY MODE is as follows:
⁄𝑥 𝑂𝐿𝑖𝑔ℎ𝑡. (𝑚𝑜𝑑𝑒. 𝑂𝐹𝐹 )|𝐶𝐶𝑈𝑛𝑖𝑡𝑥 . (𝑚𝑜𝑑𝑒. 𝐷𝐴𝑌)|𝑑1 Figure 5: Bigraph C: Context-Aware Bigraph.
4.1. Context-Unaware Bigraph 4.3. Modeling Context-Aware System
As mentioned previously, at sunset, the lightning The idea behind the separation of the context-
control system switches automatically to NIGHT aware aspects (Figure 5) of the system from the other
MODE. Consequently, the occurred reaction aspects (Figure 4) is not only to cope with the complex
represents a context reaction rule. The figure below nature of context-aware systems, but also to make
models the bigraph host 𝑆: 𝐾 → 𝐽 of the new context predictive modeling, simple and efficient, by providing
bigraph. 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 MODE 𝑆𝐶 (see
Figure 6) is given by the composition of the bigraph
host and context bigraph presented in Figure 4 and
Figure 5, respectively.
Formally, the composition operation occurs if and
only if the inner face of 𝑆 corresponds to the outer face
of 𝐶; it proceeds by plugging each region of 𝐶 into its
Figure 4: Bigraph S: Host bigraph. matching site of 𝑆, and merging the outer names of 𝐶
with the inner names of 𝑆.
Note that DAY and OFF nodes that disappeared
and replaced with site 2 and 3 respectively, are To clarify a bit more, 𝐾 = 〈𝑘, 𝑍〉 is the inner face of
context-nodes which only appear in DAY MODE. the bigraph 𝑆 in which 𝑘 represents the number of sites
where each region 𝑖 of 𝐶 containing context-nodes can
The algebraic expression of the above bigraphical
be planted into the 𝑖 𝑡ℎ site of 𝑆. 𝑍 is the set of inner
model is as follows:
names where each inner name is linked to its related
⁄𝑥 𝑂𝐿𝑖𝑔ℎ𝑡. (𝑚𝑜𝑑𝑒. 𝑑3 )|𝐶𝐶𝑈𝑛𝑖𝑡𝑥 . (𝑚𝑜𝑑𝑒. 𝑑2 )|𝑑1 outer name of 𝐶 to form a context-edge.
4.2. Context-Aware 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.
Figure 6: Bigraph SC: NIGHT MODE bigraph.
TABLE 2: Reaction rules sequence.
The algebraic expression of the lightning control
Event Reaction rule system running in NIGHT MODE is as follows:
⁄𝑥 𝑂𝐿𝑖𝑔ℎ𝑡. (𝑚𝑜𝑑𝑒. 𝑑3 )|𝐶𝐶𝑈𝑛𝑖𝑡𝑥 . (𝑚𝑜𝑑𝑒. 𝑑2 )|𝑑1 ⁄𝑥 𝑂𝐿𝑖𝑔ℎ𝑡. (𝑚𝑜𝑑𝑒. 𝑂𝑁)|𝐶𝐶𝑈𝑛𝑖𝑡𝑥 . (𝑚𝑜𝑑𝑒. 𝑁𝐼𝐺𝐻𝑇)|𝑑1
Sunset →
⁄𝑥 𝑂𝐿𝑖𝑔ℎ𝑡. (𝑚𝑜𝑑𝑒. 𝑑3 )|𝐶𝐶𝑈𝑛𝑖𝑡𝑥 . (𝑚𝑜𝑑𝑒. 𝑁𝐼𝐺𝐻𝑇)|𝑑1 Finally, the algebraic expression of the above
context-aware reaction rule is as follows:
⁄𝑥 𝑂𝐿𝑖𝑔ℎ𝑡. (𝑚𝑜𝑑𝑒. 𝑑3 )|𝐶𝐶𝑈𝑛𝑖𝑡𝑥 . (𝑚𝑜𝑑𝑒. 𝑁𝐼𝐺𝐻𝑇)|𝑑1
Light-On → ⁄𝑥 𝑂𝐿𝑖𝑔ℎ𝑡. (𝑚𝑜𝑑𝑒. 𝑂𝐹𝐹 )|𝐶𝐶𝑈𝑛𝑖𝑡𝑥 . (𝑚𝑜𝑑𝑒. 𝐷𝐴𝑌)|𝑑1
⁄𝑥 𝑂𝐿𝑖𝑔ℎ𝑡. (𝑚𝑜𝑑𝑒. 𝑂𝑁)|𝐶𝐶𝑈𝑛𝑖𝑡𝑥 . (𝑚𝑜𝑑𝑒. 𝑁𝐼𝐺𝐻𝑇)|𝑑1 →
⁄𝑥 𝑂𝐿𝑖𝑔ℎ𝑡. (𝑚𝑜𝑑𝑒. 𝑂𝑁)|𝐶𝐶𝑈𝑛𝑖𝑡𝑥 . (𝑚𝑜𝑑𝑒. 𝑁𝐼𝐺𝐻𝑇)|𝑑1
22
5. MODEL-CHECKING ANALYSIS BigMC grammar is relatively simple since it is
based on a term language. In the table above, 𝑴
Formal methods are one of the highly- refers to a bigraphical model that may be composed
recommended techniques in software design of from other models or/and expressions 𝑬. An
complex systems in both academia and industry. They expression 𝑬 can be a control (𝒌), reaction rules (𝑻 →
offer a powerful potential to achieve an early 𝑻), or a property (𝑷). A control 𝒌 must be pre-defined
integration of verification in the design process, to by the declaration of the bigraph signature %𝐚𝐜𝐭𝐢𝐯𝐞
provide more effective verification techniques and to and %𝐩𝐚𝐬𝐬𝐢𝐯𝐞 commands, which define the arity
reduce the verification time (Baier and Katoen, 2008). (number of ports) of a given control as well as whether
it is active or passive. Any term of the form 𝑻 → 𝑻 is
Recently, research in formal methods has led to considered to be a reaction rule, where the first term
the appearance of some very promising verification 𝑻 represents the redex, while the second represents
techniques accompanied by powerful software tools the reactum. Finally, the property 𝑷 is expressed as a
that automate various verification steps, in order to logical formula and it is checked whether a given
facilitate the early detection of defects. Model bigraphical model satisfies or violates this formula.
checking is one of the most successful strategies for
analyzing the correctness of safety-critical systems. It 5.2. Reachability Checking
is a formal technique for automatically verifying
In order to verify the feasibility of our approach,
whether a finite-state system satisfies a given logical
we use the BigMC model checker to encode the
property.
lightning control system.
In the following, we introduce the Bigraphical
model checker BigMC and its grammar, then, we The table below represents the bigraphical
describe how to use it in order to implement and specification of the context-unaware part in BigMC
perform some verifications on the lightning control terms language.
system model.
TABLE 4: BigMC Specification of a Lightning Control
5.1. BigMC: Bigraphical Model Checker System.
BigMC (Bigraphical Model Checker) is a model #Central Control Unit Nodes
checker specifically designed to operate on any model %active CCUnit : 2;
encoded as a bigraphical reactive systems (Perrone, %active mode : 0;
Debois and Hildebrandt, 2013). It permits the %passive DAY : 0;
execution of bigraphical reactive systems and
checking whether some specification or properties of #Outdoor lights Unit Nodes
a particular bigraphical model are true. One of the %active OLight : 1;
main benefits of BigMC is its ability to provide a %active mode : 0;
mechanism of state reachability analysis based on %passive OFF : 0;
properties expressed in terms of matching. In other
words, it can find all possible configurations of a #Hyper-edges
particular model, check the specification against them %name e1;
and provide a counter-example in the event that a
configuration violates the specification. #Lightning Control System Model
The full BigMC grammar is given in the following table. OLight[e1].(mode.OFF)|CCUnit[e1,x].(mode.DAY);
TABLE 3: Terms language for bigraphs. The bigraphical specification of the context-aware
part represented in Figure 5 is as follows:
𝑀 ∷= 𝐸; 𝑀 | 𝐸
𝐸 ∷= %𝑝𝑎𝑠𝑠𝑖𝑣𝑒 𝑘 ∶ 𝑎𝑟𝑖𝑡𝑦 TABLE 5: BigMC Specification of the Context Bigraph.
𝐸 ∷= %𝑎𝑐𝑡𝑖𝑣𝑒 𝑘 ∶ 𝑎𝑟𝑖𝑡𝑦
𝐸 ∷= %𝑟𝑢𝑙𝑒 𝑛 𝑇 → 𝑇 #Context-Aware Nodes
𝐸 ∷= %𝑝𝑟𝑜𝑝𝑒𝑟𝑡𝑦 𝑛 𝑃 %passive NIGHT : 0;
𝐸 ∷= 𝑇 → 𝑇 | 𝑇 %passive ON : 0;
𝑇 ∷= 𝐾. 𝑇 | 𝑇 | 𝑇 | 𝑇 || 𝑇 | $𝑛 | 𝐾 | 𝑛𝑖𝑙
𝐾 ∷= 𝑘[𝑛𝑎𝑚𝑒𝑠] | 𝑘 Table 6 decodes the sunset and light-on reaction
𝑛𝑎𝑚𝑒𝑠 : : = 𝑛, 𝑛𝑎𝑚𝑒𝑠 | 𝑛 rules listed in Table 2 that are applied to switch the
𝑛 ∷= [𝑎 – 𝑧𝐴 – 𝑍][𝑎 – 𝑧𝐴 – 𝑍0 – 9] ∗ | − lightning control system to NIGHT MODE.
𝑃 ∷= 𝑚𝑎𝑡𝑐ℎ𝑒𝑠(𝑇) | 𝑡𝑒𝑟𝑚𝑖𝑛𝑎𝑙() | ! 𝑃
23
TABLE 6: Specification of the reaction rules. TABLE 8: Model-Checking results.
#Reaction Rules > C:\Progra~1\BigMC/bin/bigmc -m 1000 -r 50 -p
CCUnit[e1,x].(mode.$2) -> CCUnit[e1,x].(mode.NIGHT);
1: (OLight[e1].mode.OFF.nil|CCUnit[e1,x].mode.DAY.nil)
OLight[e1].(mode.$3) -> OLight[e1].(mode.ON);
2: (OLight[e1].mode.ON.nil|CCUnit[e1,x].mode.DAY.nil)
Once the lightning control system model and the
set of reaction rules are defined, the next step consists 3: (OLight[e1].mode.OFF.nil|CCUnit[e1,x].mode.NIGHT.nil)
to specify some properties that must be checked.
4: (CCUnit[e1,x].mode.NIGHT.nil|OLight[e1].mode.ON.nil)
Here, we focus on proving that the final state
corresponding to the bigraph reconfiguration [mc::step] Complete!
displayed in Figure 6 is eventually reachable by the
application of the above reaction rules. [mc::report] [q: 0 / g: 4] @ 5
BigMC implements explicit-state checking of
properties expressed as matching. Each property is 6. CONCLUSION
expressed as combinations of two predefined
predicates: matches () and terminal (). The In this paper, we have presented a formal
matches() predicate describes some redex that must approach based on bigraphical reactive systems to
be found (or assert that not be found) in every possible specify and verify context-aware systems. Firstly, we
agent of a given system as it behaves. The terminal () have shown, through a case study of a smart home
predicate is true if an only if there are no possible system, the potential of our approach for a generic and
further states reachable by a step of reaction from the high level modeling of the different aspects of context-
current one. Furthermore, predicates can be aware systems. The proposed approach provides a
combined together with the common boolean clear separation between the context-aware part of the
operators and, or and not (i.e. &&, || and !) to form system and the remaining one; each part is modeled
more complex expressions (Perrone, Debois and by a distinct bigraph, and their composition yields a
Hildebrandt, 2013). new bigraph describing the whole structure of the
context-aware system.
Now, let final_state be a reachability property
defined as the negation of the buit-in predicate Besides, the behavior of context-aware systems
terminal (). We note that the final state is a terminal has been characterized by bigraphical reaction rules
state which does not lead to any further states and with respect to both context changes and internal
there are no reaction rules that can be applied to it. system changes. Then, we have implemented the
case study using the BigMC model checker and
The specification of the final_state property in effectively proven the applicability of our approach.
BigMC is as follows:
As a future extension, we intend to evaluate the
TABLE 7: Reachability property specification. effectiveness of our approach by checking whether
some critical non-functional properties (i.e. security) of
#Properties a particular bigraphical model are true.
%property final_state !terminal(); Additionally, we are developing a tool (Cherfia and
%check Belala. 2014) that supports the modeling and
execution of any context-aware system encoded as a
The following are the default command-line bigraphical reactive system, in order to apply our
approach on large-scale ubiquitous systems.
options for BigMC:
-m 1000: maximum number of steps. 7. REFERENCES
-r 50: reporting frequency. Abowd, G., Dey, A., Brown, P., Davies, N., Smith, M.,
Steggles, P. (1999) Towards a Better Understanding
-p: a command to print new states.
of Context and Context-Awareness. In: Proceedings
of First International Symposium, HUC’99, LNCS
Running BigMC with these options, we prove that
1707. Karlsruhe, Germany, 27-29 September 1999.
the intended state is successfully reached as shown in Springer-Verlag. 304-307.
step 4 of Table 8.
24
Baier, C., Katoen, J. P. (2008) Principles of Model Milner, R. (2009) The Space and Motion of
Checking (Representation and Mind Series). The MIT Communicating Agents. Cambridge University Press.
Press. Cambridge. England.
Pereira, E., Kirsch, C., Sengupta, R. (2012) BiAgents
Birkedal, L., Debois, S., Hildebrandt, T. (2006) – A Bigraphical Agent Model for Structure-aware
Bigraphical Models of Context-Aware Systems. In: Computation. Cyber-Physical Cloud Computing
Foundations of Software Science and Computation Working Papers, CPCC Berkeley.
Structures, LNCS 3921. Vienna, Austria, 25-31 March
Perrone, G., Debois, S., Hildebrandt, T. (2013) A
2006. Springer-Verlag. 187-201.
verification environment for bigraphs, Journal of
Cherfia, T. A., Belala, F. (2014) A BRS-Based Innovation in Systems and Software Engineering,
Modeling Approach for Context-Aware Systems A Springer-Verlag, 9 (2). 95-104.
Case Study of Smart Car System. IEEE/IFIP
Siewe, F., Cau, A., Zedan, H. (2009) The Calculus of
International Conference on Embedded and
Context-aware Ambients, Journal of Computer and
Ubiquitous Computing (EUC). In press.
System Sciences. 77 (4). 597-620.
Cherfia, T. A., Belala, F. (2014) BigCAS-Tool: A
Wang, J., Xu, D., Lei, Z. (2011) Formalizing the
Bigraphical Environment for Modeling Context-Aware
Structure and Behaviour of Context-aware Systems in
Systems. Submitted to: International Conference on
Bigraphs. In: First ACIS International Symposium on
Advanced Aspects of Software Engineering,
Software and Network Engineering. Seoul, Korea, 19-
ICAASE’14.
20 December 2011. IEEE. 89-94.
Jiang, L., Liu, D., Yang, B (2004) Smart Home
Weiser, M. (2002) The computer for the 21st Century.
Research. In Proc. of the Third International
Pervasive Computing, IEEE, 1 (1). 19-25.
Conference on Machine Learning and Cybernetics.
Vol. 2, 659-663. Xu, D.Z., Xu, D., Lei Z. (2011) Bigraphical Model of
Context-aware in Ubiquitous Computing
King, N. (2003) Smart Home - A Definition. Intertek &
Environments. In: Asia-Pacific Services Computing
DTI. Housing LIN.
Conference. Jeju Island, Korea, 12-15 December
Milner, R. (2008) Bigraphs and their algebra. In: 2011. IEEE. 389-394.
Proceedings of the LIX Colloquium on Emerging
Zimmer, P. (2005) A Calculus for Context-awareness.
Trends in Concurrency Theory. Electronic Notes in
BRICS Report Series RS-05-27. Aarhus, Denmark.
Theoretical Computer Science. 209. 5-19.
21 pages.