Ensuring safe prevention and reaction in smart home systems dedicated to people becoming disabled

Smart homes dedicated to people with disabilities, specially those with dementia, are critical systems which need to remain safe and adapted to the user. However the control part of such systems - ensuring their safety - is both difficult to design and verify without appropriate tools. Formal techniques have been used to cope with the verification problem, but this paper proposes a new way to specify smart home safety which also eases the design aspect. It enables the use of a correct by construction technique - Discrete Controller Synthesis - to automatically build from constraints a maximally permissive safety controller that can also reconfigure itself as the disabilities of the associated user evolve.