Correct by Construction Security Approach to Design Fault Tolerant Smart Homes for Disabled People

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 these systems, that is ensuring their safety, is both difficult to design as well as to 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.