Formal Modelling and Verification of Pervasive Computing Systems

Author Yan Liu

Thumbnail PDF


  • Filesize: 0.74 MB
  • 7 pages

Document Identifiers

Author Details

Yan Liu

Cite AsGet BibTex

Yan Liu. Formal Modelling and Verification of Pervasive Computing Systems. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 61-67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


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.
  • System Analysis
  • Formal Modelling and Verification
  • Reliability Analysis


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail