Computing at Glasgow University
Paper ID: 9243

Tightly coupled verification of pervasive systems
Calder,M. Gray,P.D. Unsworth,C.

Publication Type: Not Entered
Appeared in: Proceedings of Third International Workshop on Formal Methods in Interactive Systems (FMIS 2009)
Page Numbers :
Publisher: N/A
Year: 2009
ISBN/ISSN: 1862-2122

We consider the problem of verifying context-aware, pervasive, interactive systems when the interaction involves both system configuration and system use. Verification of configurable systems is more tightly coupled to design when the verification process involves reasoning about configurable formal models. The approach is illustrated with a case study: using the model checker SPIN and a SAT solver to reason about a configurable model of an activity monitor from the MATCH homecare infrastructure. Parts of the models are generated automatically from actual log files. }

Keywords: formal models, pervasive systems, model checking

PDF Bibtex entry Endnote XML