Pervasive safety application with model checking in smart houses: The INOVUS intelligent oven

Safety is a major challenge in developing assistive software for people with special needs in smart houses. INOVUS is an ongoing project about safety issues of cooking activities. This paper presents the INOVUS project and highlights lacks in current software development processes to meet safety requirements in pervasive computing. In the INOVUS project, we propose an approach to introduce model checking using ALLOY as a new layer to strengthen the design and the understanding of specifications in the development process of safety related applications in smart houses. Finally, we illustrate the model checking process with ALLOY and present the initial results of the INOVUS prototype.