Towards modeling and verification of smart homes

In recent years, the uses of ambient intelligence technologies have been strengthened such that the results promise to revolutionize daily human life by making people´s surroundings flexible and adaptive. A sub branch of this technology is the design of smart home systems. Because these systems are dedicated to be used to improve the quality of life comfort and security while taking into accounts both dimensions of time and space, it is required to use a suitable formal model that is able to handle smart home domain specific nature and which support simulation and verification. This paper proposes a technique that uses reference nets to model and verify a smart home which is sensitive, adaptive and responsive to human person´s presence, needs and preferences.