面向动作的上下文感知应用的规约与运行时验证

• 作者: 吕建 宋巍 李晅松 陶先平
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 普适计算 上下文感知 形式规约 运行时验证
• 年，卷（期）: 2017,（5）
• 所属期刊栏目: 形式化方法与应用专题
• 页码范围: 1167-1182
• 页数: 16页
• 分类号: TP311
• 字数: 11720字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005215

摘要

面向动作的上下文感知(activity-oriented context-aware,简称AOCA)应用组织环境中的资源,为用户动作的顺利进行提供支持.为应对环境和动作相关需求的开放性,这类应用采用轻量级、增量式的开发方法进行开发.相对于在开发阶段描述全局信息的开发方法,AOCA应用的开发可能由不同开发者在不同时间共同参与,这可能会导致较多的不一致等问题,且难以在开发阶段被发现.围绕使用运行时验证手段提高AOCA应用可靠性这一目标展开研究,给出了对于AOCA应用运行状态进行形式化规约、对于系统级和应用级性质进行描述的方法,进一步地设计实现了AOCA应用监控器.最后,通过案例分析以及性能评估证实了该方法的有效性.