Programming Method and Formalization for Activity-Oriented Context-Aware Applications

In many pervasive computing applications, the users´ requirements on environment are highly dependent on specific user activities. We refer to these applications as activity-oriented context-aware (AOCA) applications. In this paper, we propose a programming method which focuses on requirements related to each activity. This method supports lightweight and incremental development of AOCA applications. In order to enhance the reliability of the developed applications especially for safety-critical applications, we further propose an Ambient Calculus based formal model to specify AOCA applications. We describe properties for the verification based on Ambient Logic. Finally, we present a case study to demonstrate the developing process of the proposed method and the usability of the formalization.