动作和环境感知应用的形式化技术研究

Activity and environment aware applications are typical scenarios of pervasive/ubiquitous computing. Such applications organize environment resources to support the smoothly performing of user activities. Activity and environment aware applications have some characteristics such as the incremental development process and the open, dynamic runtime environment. These characteristics challenge the reliability of these applications. In order to address this challenge, this research aims at using formal technology for activity and environment aware applications to enhance the reliability of such applications. In this project, the research group will firstly extend existing formal systems based on the characteristics of activity and environment aware applications in order to establish the formal tool for this kind of application. We will then study on the model checking algorithm and runtime verification technology with this formal tool to deal with the efficient verification issue of such applications. Next, we will study on the concept model, development method, and runtime support technology for activity and environment aware applications under the guidance of the formal method so that we can specify and verify such applications in the phases of design, development, and runtime. Finally, a demo of elderly care system will demonstrate the usability of the key technologies. This project will improve the formal method support for the software methodology of activity and environment aware applications. It will also promote software quality of such applications.

动作和环境感知应用是普适计算的典型应用场景，这类应用组织环境中的资源、为用户动作的顺利进行提供支持。动作和环境感知应用具有开发过程增量式、运行环境开放动态等特点，对其可靠性提出了挑战。针对这一挑战，本项目致力于开展动作和环境感知应用的形式化技术研究。项目组拟首先基于动作和环境感知应用特点扩展现有形式系统，建立适合这类应用的形式化工具；然后，拟通过研究该形式化工具相应的模型检验算法和运行时验证技术，解决这类应用的高效验证问题；进一步地，拟通过研究基于形式化方法指导的动作和环境感知应用概念模型、开发方法和运行支撑技术，在设计、开发、运行的各个阶段进行规约和验证；上述关键技术以老人看护为示范应用进行实验验证。本项目的实施，将改进形式化方法对于动作和环境感知应用软件方法学的支持，推动这类应用软件质量的提升。

动作和环境感知应用可以感知用户动作，进一步地感知动作相关的环境信息，并根据感知到的这些信息反馈环境和用户，以保障动作进行。为提升这类应用的软件质量，本项目的研究目标为研究适合这类应用的形式化技术以及形式化方法指导下的应用开发与运行方法体系。我们的研究内容在形式化工具、软件开发支持、运行支撑与验证、实验环境相关传感器技术等方面取得了良好进展。.具体而言，取得的成果包括：1）在形式化工具的理论方面，提出了AL3——三值语义Ambient Logic，支持普适计算应用时空性质的运行时验证；2）在该领域形式化方法的技术实现和应用方面，实现了Ambient Logic的检验器ALChecker并与动作和环境感知应用的可靠性验证结合；进一步地尝试了基于MTL的含有时间约束的性质验证；3）在开发和运行支撑方面，提出了AocML——一种支持面向动作的上下文感知（AOCA）应用模型驱动开发的领域专用语言，并实现了相关的开发和运行支撑工具；4）我们尝试了示范应用环境的部署，包括传感器和智能家居设备等，并在此基础上，进一步进行了手机气压传感器校准相关技术的研究。.这一系列的技术进展和工具实现，推进了提升动作和环境感知应用的可靠性的进度，降低了开发这类应用的难度，完成了本项目预期的目标。