Engineering human flows in smart environments using formal techniques - Full version

While the cost of deploying a smart environment is likely to be high, the benefits of such systems are hard to quantify and predict. The potential for expensive failure is therefore considerable. This paper is concerned with how formal models of smart environments might be used to explore the consequences of the technology on users of the environment before deployment. Alternative models of interaction within smart environments are explored. The first focuses on the individual within the environment and the second provides an exploration of the impact of the designed environment on collective behaviour. It applies a recent approach that provides a quantitative analysis of systems with a very large number of entities with similar behaviour. The paper argues that there are particular properties relating to implicit interaction in immersive systems and to issues of crowd system interaction and discusses how these properties should be analysed. The relationship between these models is discussed and an agenda is established for tool supported methodology. This paper is concerned with an engineering approach to the analysis of human aspects of smart environments.