License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FSFMA.2013.61
URN: urn:nbn:de:0030-drops-40892
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4089/
Go to the corresponding OASIcs Volume Portal

Liu, Yan

Formal Modelling and Verification of Pervasive Computing Systems

pdf-format:
9.pdf (0.7 MB)

Abstract

Pervasive computing (PvC) systems are emerging as promising solutions to many practical problems, e.g., elderly care in home. However, such systems have long been developed without sufficient verification. Formal methods, eps. model checking are sound techniques for complex system analysis regarding correctness and reliability requirements. In this work, a formal modelling framework is proposed to model the general the system design (e.g., concurrent communications) and the critical environment inputs (e.g., human behaviours). Correctness requirements are specified in formal logics which are automatically verifiable against a system model. Furthermore, Markov Decision Processes (MDPs) are adopted for modelling probabilistic behaviours of PvC systems. Three problems are analysed which are overall reliability prediction based on component reliabilities, reliability distribution w.r.t., how reliable should the component be to reach an overall reliability requirement and sensitivity analysis w.r.t., how does a component reliability affect the overall reliability. Finally, the usefulness of our approaches are demonstrated on a smart healthcare system with unexpected bugs and system flaws exposed.

BibTeX - Entry

@InProceedings{liu:OASIcs:2013:4089,
  author =	{Yan Liu},
  title =	{{Formal Modelling and Verification of Pervasive Computing Systems}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{61--67},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Christine Choppy and Jun Sun},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4089},
  URN =		{urn:nbn:de:0030-drops-40892},
  doi =		{10.4230/OASIcs.FSFMA.2013.61},
  annote =	{Keywords: System Analysis, Formal Modelling and Verification, Reliability Analysis}
}

Keywords: System Analysis, Formal Modelling and Verification, Reliability Analysis
Collection: 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Issue Date: 2013
Date of publication: 14.07.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI