Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Formal verification of context and situation models in pervasive computing
Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.ORCID-id: 0000-0003-1990-5734
2013 (Engelska)Ingår i: Pervasive and Mobile Computing, ISSN 1574-1192, E-ISSN 1873-1589, Vol. 9, nr 1, s. 98-117Artikel i tidskrift (Refereegranskat) 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.

Ort, förlag, år, upplaga, sidor
2013. Vol. 9, nr 1, s. 98-117
Nationell ämneskategori
Medieteknik
Forskningsämne
Distribuerade datorsystem
Identifikatorer
URN: urn:nbn:se:ltu:diva-14632DOI: 10.1016/j.pmcj.2012.03.001ISI: 000314805600007Scopus ID: 2-s2.0-84873196721Lokalt ID: e08e100b-39b2-413c-aab1-4d5198dfe8a8OAI: oai:DiVA.org:ltu-14632DiVA, id: diva2:987605
Anmärkning
Validerad; 2013; 20120327 (andbra)Tillgänglig från: 2016-09-29 Skapad: 2016-09-29 Senast uppdaterad: 2018-07-10Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Personposter BETA

Boytsov, AndreyZaslavsky, Arkady

Sök vidare i DiVA

Av författaren/redaktören
Boytsov, AndreyZaslavsky, Arkady
Av organisationen
Datavetenskap
I samma tidskrift
Pervasive and Mobile Computing
Medieteknik

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 64 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf