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

来源：软件学报杂志2017年第5期北京时间：

作者：李晅松,陶先平,吕建,宋巍

单位：李晅松，南京理工大学 计算机科学与工程学院, 江苏 南京 210094;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002311,陶先平，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002302,吕建，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002303,宋巍，南京理工大学 计算机科学与工程学院, 江苏 南京 210094;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002304

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

关键词：普适计算;上下文感知;形式规约;运行时验证

基金资助：国家自然科学基金（61373011，61202003，61502225）