@misc{oai:ir.soken.ac.jp:00001502, author = {HOAREAU, Christian and ワロ, クリスチャン and HOAREAU, Christian}, month = {2016-02-17, 2016-02-17}, note = {CONTEXT-AWARE COMPUTING refers to the idea that computing devices can sense
and react to the physical environment where they are deployed. For example,
a context-aware corporate office would intelligently respond to peoples locations and
activities by self-adjusting its lighting and temperature automatically, thus reducing
its energy footprint.
  Context-aware systems model the real world by using increasingly complex and
refined contextual-data representations. As a result, their design and management raise
several challenges. An important and somewhat unexplored one is to guarantee that
context-aware systems correctly capture the intent of their designers once deployed. For
example, we might want to assure that the energy conservation of the aforementioned
corporate office is actually preserved.
  We propose in this thesis a query processing and specification framework that alle-
viates designing and building context-aware systems. It guarantees the management of
contextual information, and can be used for specifying the underlying rules of context-
aware systems. Our approach encourages a high-level of abstraction for retrieving
contextual information in a robust manner, and supports building "provably-correct"
context-aware systems incrementally, by providing modularity and separation of con-
cerns.
  The proposed approach aims at complementing existing context-aware service
wherein contextual information about the physical and computational environment
- information about people, objects, and services - is modeled in a symbolic fashion,
and is independent of any particular sensing technology. In current pervasive com-
puting plateform, contextual information and their underlying models are queried an
ad-hoc manner. Which makes it impossible to guarantee the quality of the results
being returned, and hence the reliability of context-aware services.
  The main idea behind our framework is to apply and adapt the principles of model
checking to query the contextual data structures. Because such query mechanisms have
to be sound, our approach is build upon a logic-based query language. We therefore
ensure that the results of any query (i) do not miss any information that satisfy its
necessary and sufficient conditions and (ii) ,do not contain any information that does
not satisfy the conditions. We describe the implementation of our framework and
discuss its applicability to existing graph-based contextual models., 総研大甲第1287号}, title = {A Model Checking based Framework for Context-Aware Systems}, year = {} }