Tightly coupled verification of pervasive systems

We consider the problem of verifying context-aware, pervasive, inter- active 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 ap- proach is illustrated with a case study: using the model checker SPIN (Hol03) and a SAT solver (ES03) to reason about a configurable model of an activity monitor from the MATCH homecare infrastructure (MG09). Parts of the models are generated automatically from actual log files.