2015/11/03 by Muffy Calder, Calder, Muffy, Philip Gray +3
Computer Science · #Advanced Software Engineering Methodologies #Formal Methods in Verification #Petri Nets in System Modeling
paper · doi:10.14279/tuj.eceasst.22.320
openalex publication_date 2024/03/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/01
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.