Formal verification of a pervasive messaging system

Savas Konur, Michael Fisher, Simon Andrew Dobson, Stephen Knox

Research output: Contribution to journalArticlepeer-review

16 Citations (Scopus)

Abstract

As ubiquitous computing becomes a reality, its applications are increasingly being used in business-critical, mission-critical and even in safety-critical, areas. Such systems must demonstrate an assured level of correctness. One approach to the exhaustive analysis of the behaviour of systems is formal verification, whereby each important requirement is logically assessed against all possible system behaviours. While formal verification is often used in safety analysis, it has rarely been used in the analysis of deployed pervasive applications. Without such formality it is difficult to establish that the system will exhibit the correct behaviours in response to its inputs and environment. In this paper, we show how model-checking techniques can be applied to analyse the probabilistic behaviour of pervasive systems. As a case study we apply this technique to an existing pervasive message-forwarding system, Scatterbox. Scatterbox incorporates many typical characteristics of pervasive systems, such as dependence on sensor reliability and dependence on context. We assess the dynamic temporal behaviour of the system, including the analysis of probabilistic elements, allowing us to verify formal requirements even in the presence of uncertainty in sensors. We also draw some tentative conclusions concerning the use of formal verification for pervasive computing in general.
Original languageEnglish
Pages (from-to)677-694
Number of pages18
JournalFormal Aspects of Computing
Volume26
Issue number4
Early online date28 Mar 2013
DOIs
Publication statusPublished - Apr 2014

Keywords

  • Formal specification
  • Pervasive systems
  • Probabilistic verification

Fingerprint

Dive into the research topics of 'Formal verification of a pervasive messaging system'. Together they form a unique fingerprint.

Cite this