Designing smart homes dedicated to disabled people using modular Discrete Controller Synthesis

In the domain of smart homes dedicated to disabled people, especially cognitively impaired people, providing an adequate assistance to allow the users to carry out their activities of daily living is the main challenge tackled by many contributions. New assistive technologies based on the concept of Ambient Intelligence have been developed to alleviate the effects of cognitive decline, however, the reliability of such propositions is seldom discussed while the smart home environment — consisting of several electronic or mechanic components — is usually not reliable. Over time, components can fail, threatening to compromise the ability of implemented assistive technologies to maintain their services, thus endangering an already frail user. To deal with the problem of reliability and failure tolerance, redundancy and Quality of Service management systems can be implemented. However, correctly designing such systems is a difficult problem. To address this challenge, this paper presents a formal methodology to model fault tolerant smart homes assistive technologies. The contribution consists in representing a smart home as a controllable reactive program, on which the proposed methodology exploits the modular application of Discrete Controller Synthesis to automatically obtain the various parts of its fault tolerance management system.