Formal mirror models: an approach to Just-in-Time reasoning for device ecologies

Pervasive computing calls for new ways of thinking about software and new ways of applying software development techniques. In pervasive computing environments, users will need to interact with collections of devices surrounding them (such as the "system" of smart devices in a user's home), which we metaphorically term device ecologies. A user can interact with these devices with embedded software and hardware, either directly via the device's own interface, or automated through scripts executed by a central coordinator. For the latter, we employ a workflow abstraction for the collective operation of devices, which we call decoflow. While executable formal models are typically used at specification time, we maintain and use such models, calling them mirror models, to record the on-going states of devices, their relationships, and the effects that such devices have on the environment. Users effectively update a mirror model of the devices s/he interacts with. The model can be used to predict the effects of decoflows just before execution. Generalizing from mirror models for device ecologies, we propose the novel paradigm of continually updated mirror models for on-going tracking and reasoning about pervasive computing systems which cohabitates with the user.