Electronic Communications of the EASST Volume 22 ( 2009 ) Proceedings of the Third International Workshop on Formal Methods for Interactive Systems ( FMIS 2009 ) Tightly coupled verification of pervasive systems
Electronic Communications of the EASST Volume 22 ( 2009 ) Proceedings of the Third International Workshop on Formal Methods for Interactive Systems ( FMIS 2009 ) Tightly coupled verification of pervasive systems
复制标题
EASST 电子通信第 22 卷 (2009) 第三届交互式系统形式方法国际研讨会 (FMIS 2009) 普适系统的紧耦合验证
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Chris Unsworth
中科院分区：
文献类型：
--
作者：
Muffy Calder;P. Gray;Chris Unsworth
当交互既涉及系统配置又涉及系统使用时，我们考虑验证上下文感知的、普遍存在的交互系统的问题。当验证过程涉及对可配置形式模型的推理时，可配置系统的验证与设计更紧密地结合在一起。该方法通过一个案例研究来说明：使用模型检查器SPIN[Hol03]和SAT求解器[ES03]来推理来自匹配家庭护理基础设施[MG09]的活动监视器的可配置模型。部分模型是从实际日志文件自动生成的。
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 [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.