Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal verification of context and situation models in pervasive computing
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science.ORCID iD: 0000-0003-1990-5734
2013 (English)In: Pervasive and Mobile Computing, ISSN 1574-1192, E-ISSN 1873-1589, Vol. 9, no 1, p. 98-117Article in journal (Refereed) Published
Abstract [en]

Pervasive computing is a paradigm that focuses on availability of computer resources anytime anywhere for any application and supports non-intrusive integration of computing services into everyday life. Context awareness is the core feature of pervasive computing. High-level context awareness can be enhanced by situation awareness that represents the ability to detect and reason about the real-life situations. In this article we propose, analyze and validate the formal verification method for situation definitions and demonstrate its feasibility and efficiency. Situations are often defined manually by domain experts and are, therefore, susceptible to definition inconsistencies and possible errors, which in turn can cause situation reasoning problems. The proposed method takes as an input properties of situations and dependencies among them as well as situation definitions in terms of low-level context features, and then either formally proves that the definitions do comply with the expected properties, or provides a complete set of counterexamples — context parameters that prove situation inconsistency. Evaluation and complexity analysis of the proposed approach are also presented and discussed. Examples and evaluation results demonstrate that the proposed approach can be used to verify real-life situation definitions, and detect non-obvious errors in situation specifications.

Place, publisher, year, edition, pages
2013. Vol. 9, no 1, p. 98-117
National Category
Media and Communication Technology
Research subject
Mobile and Pervasive Computing
Identifiers
URN: urn:nbn:se:ltu:diva-14632DOI: 10.1016/j.pmcj.2012.03.001ISI: 000314805600007Scopus ID: 2-s2.0-84873196721Local ID: e08e100b-39b2-413c-aab1-4d5198dfe8a8OAI: oai:DiVA.org:ltu-14632DiVA, id: diva2:987605
Note
Validerad; 2013; 20120327 (andbra)Available from: 2016-09-29 Created: 2016-09-29 Last updated: 2018-07-10Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Boytsov, AndreyZaslavsky, Arkady

Search in DiVA

By author/editor
Boytsov, AndreyZaslavsky, Arkady
By organisation
Computer Science
In the same journal
Pervasive and Mobile Computing
Media and Communication Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 62 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf