Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet 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 (engelsk)Inngår i: Pervasive and Mobile Computing, ISSN 1574-1192, E-ISSN 1873-1589, Vol. 9, nr 1, s. 98-117Artikkel i tidsskrift (Fagfellevurdert) 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.

sted, utgiver, år, opplag, sider
2013. Vol. 9, nr 1, s. 98-117
HSV kategori
Forskningsprogram
Distribuerade datorsystem
Identifikatorer
URN: urn:nbn:se:ltu:diva-14632DOI: 10.1016/j.pmcj.2012.03.001ISI: 000314805600007Scopus ID: 2-s2.0-84873196721Lokal ID: e08e100b-39b2-413c-aab1-4d5198dfe8a8OAI: oai:DiVA.org:ltu-14632DiVA, id: diva2:987605
Merknad
Validerad; 2013; 20120327 (andbra)Tilgjengelig fra: 2016-09-29 Laget: 2016-09-29 Sist oppdatert: 2018-07-10bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstScopus

Personposter BETA

Boytsov, AndreyZaslavsky, Arkady

Søk i DiVA

Av forfatter/redaktør
Boytsov, AndreyZaslavsky, Arkady
Av organisasjonen
I samme tidsskrift
Pervasive and Mobile Computing

Søk utenfor DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 64 treff
RefereraExporteraLink to record
Permanent link

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