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

Specification and Runtime Verification for Activity-Oriented Context-Aware Applications

作　　者：李晅松[1,2] 陶先平[2] 吕建[2] 宋巍[1,2] 

机构地区：[1]南京理工大学计算机科学与工程学院,江苏南京210094 [2]计算机软件新技术国家重点实验室(南京大学),江苏南京210023

出　　处：《软件学报》2017年第5期1167-1182,共16页Journal of Software

基　　金：国家自然科学基金(61373011;61202003;61502225)~~

摘　　要：面向动作的上下文感知(activity-oriented context-aware,简称AOCA)应用组织环境中的资源,为用户动作的顺利进行提供支持.为应对环境和动作相关需求的开放性,这类应用采用轻量级、增量式的开发方法进行开发.相对于在开发阶段描述全局信息的开发方法,AOCA应用的开发可能由不同开发者在不同时间共同参与,这可能会导致较多的不一致等问题,且难以在开发阶段被发现.围绕使用运行时验证手段提高AOCA应用可靠性这一目标展开研究.给出了对于AOCA应用运行状态进行形式化规约、对于系统级和应用级性质进行描述的方法.进一步地设计实现了AOCA应用监控器.最后,通过案例分析以及性能评估证实了该方法的有效性.Activity-Oriented context-aware （AOCA） applications organize environment resources to support the smooth performing of user activities. These applications are developed with a light-weight and incremental method in order to deal with the openness of the environment and requirements related to user activities. In contrast to the methods which attempt to deal with information from an overall level, AOCA applications allow different developers take part in the development in different time. However, this method may lead to more problems such as inconsistency. These problems are difficult to be detected in the development phase. This study focuses on using runtime verification to enhance the reliability of AOCA applications. In this paper, a method is first proposed for specifying AOCA application runtime status and describing system-level and application-level properties. Next, an AOCA application monitor is designed and implemented. Moreover, a case study and a performance evaluation are described to demonstrate the usability of this method.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]